Theorem climcndslem1 13297

Description: Lemma for climcnds 13299: bound the original series by the condensed series. (Contributed by Mario Carneiro, 18-Jul-2014.)

Hypotheses

Ref	Expression
climcnds.1	|- ( ( ph /\ k e. NN ) -> ( F ` k ) e. RR )
climcnds.2	|- ( ( ph /\ k e. NN ) -> 0 <_ ( F ` k ) )
climcnds.3	|- ( ( ph /\ k e. NN ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )
climcnds.4	|- ( ( ph /\ n e. NN0 ) -> ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) )

Assertion

Ref	Expression
climcndslem1	|- ( ( ph /\ N e. NN0 ) -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( N + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` N ) )

Distinct variable groups:   k, n, F   k, G, n   ph, k, n

Allowed substitution hints:   N( k, n)

Proof of Theorem climcndslem1

Dummy variables j x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 6089	. . . . . . . . . . 11 |- ( x = 0 -> ( x + 1 ) = ( 0 + 1 ) )
2		0p1e1 10423	. . . . . . . . . . 11 |- ( 0 + 1 ) = 1
3	1, 2	syl6eq 2483	. . . . . . . . . 10 |- ( x = 0 -> ( x + 1 ) = 1 )
4	3	oveq2d 6098	. . . . . . . . 9 |- ( x = 0 -> ( 2 ^ ( x + 1 ) ) = ( 2 ^ 1 ) )
5		2cn 10382	. . . . . . . . . . 11 |- 2 e. CC
6		exp1 11857	. . . . . . . . . . 11 |- ( 2 e. CC -> ( 2 ^ 1 ) = 2 )
7	5, 6	ax-mp 5	. . . . . . . . . 10 |- ( 2 ^ 1 ) = 2
8		df-2 10370	. . . . . . . . . 10 |- 2 = ( 1 + 1 )
9	7, 8	eqtri 2455	. . . . . . . . 9 |- ( 2 ^ 1 ) = ( 1 + 1 )
10	4, 9	syl6eq 2483	. . . . . . . 8 |- ( x = 0 -> ( 2 ^ ( x + 1 ) ) = ( 1 + 1 ) )
11	10	oveq1d 6097	. . . . . . 7 |- ( x = 0 -> ( ( 2 ^ ( x + 1 ) ) - 1 ) = ( ( 1 + 1 ) - 1 ) )
12		ax-1cn 9330	. . . . . . . 8 |- 1 e. CC
13		pncan 9606	. . . . . . . 8 |- ( ( 1 e. CC /\ 1 e. CC ) -> ( ( 1 + 1 ) - 1 ) = 1 )
14	12, 12, 13	mp2an 667	. . . . . . 7 |- ( ( 1 + 1 ) - 1 ) = 1
15	11, 14	syl6eq 2483	. . . . . 6 |- ( x = 0 -> ( ( 2 ^ ( x + 1 ) ) - 1 ) = 1 )
16	15	fveq2d 5685	. . . . 5 |- ( x = 0 -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) = ( seq 1 ( + , F ) ` 1 ) )
17		fveq2 5681	. . . . 5 |- ( x = 0 -> ( seq 0 ( + , G ) ` x ) = ( seq 0 ( + , G ) ` 0 ) )
18	16, 17	breq12d 4295	. . . 4 |- ( x = 0 -> ( ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` x ) <-> ( seq 1 ( + , F ) ` 1 ) <_ ( seq 0 ( + , G ) ` 0 ) ) )
19	18	imbi2d 316	. . 3 |- ( x = 0 -> ( ( ph -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` x ) ) <-> ( ph -> ( seq 1 ( + , F ) ` 1 ) <_ ( seq 0 ( + , G ) ` 0 ) ) ) )
20		oveq1 6089	. . . . . . . 8 |- ( x = j -> ( x + 1 ) = ( j + 1 ) )
21	20	oveq2d 6098	. . . . . . 7 |- ( x = j -> ( 2 ^ ( x + 1 ) ) = ( 2 ^ ( j + 1 ) ) )
22	21	oveq1d 6097	. . . . . 6 |- ( x = j -> ( ( 2 ^ ( x + 1 ) ) - 1 ) = ( ( 2 ^ ( j + 1 ) ) - 1 ) )
23	22	fveq2d 5685	. . . . 5 |- ( x = j -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) = ( seq 1 ( + , F ) ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) )
24		fveq2 5681	. . . . 5 |- ( x = j -> ( seq 0 ( + , G ) ` x ) = ( seq 0 ( + , G ) ` j ) )
25	23, 24	breq12d 4295	. . . 4 |- ( x = j -> ( ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` x ) <-> ( seq 1 ( + , F ) ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` j ) ) )
26	25	imbi2d 316	. . 3 |- ( x = j -> ( ( ph -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` x ) ) <-> ( ph -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` j ) ) ) )
27		oveq1 6089	. . . . . . . 8 |- ( x = ( j + 1 ) -> ( x + 1 ) = ( ( j + 1 ) + 1 ) )
28	27	oveq2d 6098	. . . . . . 7 |- ( x = ( j + 1 ) -> ( 2 ^ ( x + 1 ) ) = ( 2 ^ ( ( j + 1 ) + 1 ) ) )
29	28	oveq1d 6097	. . . . . 6 |- ( x = ( j + 1 ) -> ( ( 2 ^ ( x + 1 ) ) - 1 ) = ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) )
30	29	fveq2d 5685	. . . . 5 |- ( x = ( j + 1 ) -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) = ( seq 1 ( + , F ) ` ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) )
31		fveq2 5681	. . . . 5 |- ( x = ( j + 1 ) -> ( seq 0 ( + , G ) ` x ) = ( seq 0 ( + , G ) ` ( j + 1 ) ) )
32	30, 31	breq12d 4295	. . . 4 |- ( x = ( j + 1 ) -> ( ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` x ) <-> ( seq 1 ( + , F ) ` ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` ( j + 1 ) ) ) )
33	32	imbi2d 316	. . 3 |- ( x = ( j + 1 ) -> ( ( ph -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` x ) ) <-> ( ph -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` ( j + 1 ) ) ) ) )
34		oveq1 6089	. . . . . . . 8 |- ( x = N -> ( x + 1 ) = ( N + 1 ) )
35	34	oveq2d 6098	. . . . . . 7 |- ( x = N -> ( 2 ^ ( x + 1 ) ) = ( 2 ^ ( N + 1 ) ) )
36	35	oveq1d 6097	. . . . . 6 |- ( x = N -> ( ( 2 ^ ( x + 1 ) ) - 1 ) = ( ( 2 ^ ( N + 1 ) ) - 1 ) )
37	36	fveq2d 5685	. . . . 5 |- ( x = N -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) = ( seq 1 ( + , F ) ` ( ( 2 ^ ( N + 1 ) ) - 1 ) ) )
38		fveq2 5681	. . . . 5 |- ( x = N -> ( seq 0 ( + , G ) ` x ) = ( seq 0 ( + , G ) ` N ) )
39	37, 38	breq12d 4295	. . . 4 |- ( x = N -> ( ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` x ) <-> ( seq 1 ( + , F ) ` ( ( 2 ^ ( N + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` N ) ) )
40	39	imbi2d 316	. . 3 |- ( x = N -> ( ( ph -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` x ) ) <-> ( ph -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( N + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` N ) ) ) )
41		1nn 10323	. . . . . . 7 |- 1 e. NN
42		climcnds.1	. . . . . . . 8 |- ( ( ph /\ k e. NN ) -> ( F ` k ) e. RR )
43	42	ralrimiva 2791	. . . . . . 7 |- ( ph -> A. k e. NN ( F ` k ) e. RR )
44		fveq2 5681	. . . . . . . . 9 |- ( k = 1 -> ( F ` k ) = ( F ` 1 ) )
45	44	eleq1d 2501	. . . . . . . 8 |- ( k = 1 -> ( ( F ` k ) e. RR <-> ( F ` 1 ) e. RR ) )
46	45	rspcv 3060	. . . . . . 7 |- ( 1 e. NN -> ( A. k e. NN ( F ` k ) e. RR -> ( F ` 1 ) e. RR ) )
47	41, 43, 46	mpsyl 63	. . . . . 6 |- ( ph -> ( F ` 1 ) e. RR )
48	47	leidd 9896	. . . . 5 |- ( ph -> ( F ` 1 ) <_ ( F ` 1 ) )
49	47	recnd 9402	. . . . . 6 |- ( ph -> ( F ` 1 ) e. CC )
50	49	mulid2d 9394	. . . . 5 |- ( ph -> ( 1 x. ( F ` 1 ) ) = ( F ` 1 ) )
51	48, 50	breqtrrd 4308	. . . 4 |- ( ph -> ( F ` 1 ) <_ ( 1 x. ( F ` 1 ) ) )
52		1z 10666	. . . . 5 |- 1 e. ZZ
53		eqidd 2436	. . . . 5 |- ( ph -> ( F ` 1 ) = ( F ` 1 ) )
54	52, 53	seq1i 11806	. . . 4 |- ( ph -> ( seq 1 ( + , F ) ` 1 ) = ( F ` 1 ) )
55		0z 10647	. . . . 5 |- 0 e. ZZ
56		0nn0 10584	. . . . . 6 |- 0 e. NN0
57		climcnds.4	. . . . . . 7 |- ( ( ph /\ n e. NN0 ) -> ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) )
58	57	ralrimiva 2791	. . . . . 6 |- ( ph -> A. n e. NN0 ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) )
59		fveq2 5681	. . . . . . . 8 |- ( n = 0 -> ( G ` n ) = ( G ` 0 ) )
60		oveq2 6090	. . . . . . . . . 10 |- ( n = 0 -> ( 2 ^ n ) = ( 2 ^ 0 ) )
61		exp0 11855	. . . . . . . . . . 11 |- ( 2 e. CC -> ( 2 ^ 0 ) = 1 )
62	5, 61	ax-mp 5	. . . . . . . . . 10 |- ( 2 ^ 0 ) = 1
63	60, 62	syl6eq 2483	. . . . . . . . 9 |- ( n = 0 -> ( 2 ^ n ) = 1 )
64	63	fveq2d 5685	. . . . . . . . 9 |- ( n = 0 -> ( F ` ( 2 ^ n ) ) = ( F ` 1 ) )
65	63, 64	oveq12d 6100	. . . . . . . 8 |- ( n = 0 -> ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) = ( 1 x. ( F ` 1 ) ) )
66	59, 65	eqeq12d 2449	. . . . . . 7 |- ( n = 0 -> ( ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) <-> ( G ` 0 ) = ( 1 x. ( F ` 1 ) ) ) )
67	66	rspcv 3060	. . . . . 6 |- ( 0 e. NN0 -> ( A. n e. NN0 ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) -> ( G ` 0 ) = ( 1 x. ( F ` 1 ) ) ) )
68	56, 58, 67	mpsyl 63	. . . . 5 |- ( ph -> ( G ` 0 ) = ( 1 x. ( F ` 1 ) ) )
69	55, 68	seq1i 11806	. . . 4 |- ( ph -> ( seq 0 ( + , G ) ` 0 ) = ( 1 x. ( F ` 1 ) ) )
70	51, 54, 69	3brtr4d 4312	. . 3 |- ( ph -> ( seq 1 ( + , F ) ` 1 ) <_ ( seq 0 ( + , G ) ` 0 ) )
71		fzfid 11781	. . . . . . . . 9 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) e. Fin )
72		simpl 454	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN0 ) -> ph )
73	72	adantr 462	. . . . . . . . . 10 |- ( ( ( ph /\ j e. NN0 ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) -> ph )
74		2nn 10469	. . . . . . . . . . . 12 |- 2 e. NN
75		peano2nn0 10610	. . . . . . . . . . . . 13 |- ( j e. NN0 -> ( j + 1 ) e. NN0 )
76	75	adantl 463	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN0 ) -> ( j + 1 ) e. NN0 )
77		nnexpcl 11864	. . . . . . . . . . . 12 |- ( ( 2 e. NN /\ ( j + 1 ) e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. NN )
78	74, 76, 77	sylancr 658	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. NN )
79		elfzuz 11438	. . . . . . . . . . 11 |- ( k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) -> k e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) )
80		eluznn 10915	. . . . . . . . . . 11 |- ( ( ( 2 ^ ( j + 1 ) ) e. NN /\ k e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) -> k e. NN )
81	78, 79, 80	syl2an 474	. . . . . . . . . 10 |- ( ( ( ph /\ j e. NN0 ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) -> k e. NN )
82	73, 81, 42	syl2anc 656	. . . . . . . . 9 |- ( ( ( ph /\ j e. NN0 ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) -> ( F ` k ) e. RR )
83	43	adantr 462	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN0 ) -> A. k e. NN ( F ` k ) e. RR )
84		fveq2 5681	. . . . . . . . . . . . 13 |- ( k = ( 2 ^ ( j + 1 ) ) -> ( F ` k ) = ( F ` ( 2 ^ ( j + 1 ) ) ) )
85	84	eleq1d 2501	. . . . . . . . . . . 12 |- ( k = ( 2 ^ ( j + 1 ) ) -> ( ( F ` k ) e. RR <-> ( F ` ( 2 ^ ( j + 1 ) ) ) e. RR ) )
86	85	rspcv 3060	. . . . . . . . . . 11 |- ( ( 2 ^ ( j + 1 ) ) e. NN -> ( A. k e. NN ( F ` k ) e. RR -> ( F ` ( 2 ^ ( j + 1 ) ) ) e. RR ) )
87	78, 83, 86	sylc 60	. . . . . . . . . 10 |- ( ( ph /\ j e. NN0 ) -> ( F ` ( 2 ^ ( j + 1 ) ) ) e. RR )
88	87	adantr 462	. . . . . . . . 9 |- ( ( ( ph /\ j e. NN0 ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) -> ( F ` ( 2 ^ ( j + 1 ) ) ) e. RR )
89		simpr 458	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) -> n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) )
90		simplll 752	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... n ) ) -> ph )
91	78	adantr 462	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) -> ( 2 ^ ( j + 1 ) ) e. NN )
92		elfzuz 11438	. . . . . . . . . . . . . 14 |- ( k e. ( ( 2 ^ ( j + 1 ) ) ... n ) -> k e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) )
93	91, 92, 80	syl2an 474	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... n ) ) -> k e. NN )
94	90, 93, 42	syl2anc 656	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... n ) ) -> ( F ` k ) e. RR )
95		simplll 752	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( n - 1 ) ) ) -> ph )
96		elfzuz 11438	. . . . . . . . . . . . . 14 |- ( k e. ( ( 2 ^ ( j + 1 ) ) ... ( n - 1 ) ) -> k e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) )
97	91, 96, 80	syl2an 474	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( n - 1 ) ) ) -> k e. NN )
98		climcnds.3	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )
99	95, 97, 98	syl2anc 656	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( n - 1 ) ) ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )
100	89, 94, 99	monoord2 11823	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) -> ( F ` n ) <_ ( F ` ( 2 ^ ( j + 1 ) ) ) )
101	100	ralrimiva 2791	. . . . . . . . . 10 |- ( ( ph /\ j e. NN0 ) -> A. n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ( F ` n ) <_ ( F ` ( 2 ^ ( j + 1 ) ) ) )
102		fveq2 5681	. . . . . . . . . . . 12 |- ( n = k -> ( F ` n ) = ( F ` k ) )
103	102	breq1d 4292	. . . . . . . . . . 11 |- ( n = k -> ( ( F ` n ) <_ ( F ` ( 2 ^ ( j + 1 ) ) ) <-> ( F ` k ) <_ ( F ` ( 2 ^ ( j + 1 ) ) ) ) )
104	103	rspccva 3063	. . . . . . . . . 10 |- ( ( A. n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ( F ` n ) <_ ( F ` ( 2 ^ ( j + 1 ) ) ) /\ k e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) -> ( F ` k ) <_ ( F ` ( 2 ^ ( j + 1 ) ) ) )
105	101, 79, 104	syl2an 474	. . . . . . . . 9 |- ( ( ( ph /\ j e. NN0 ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) -> ( F ` k ) <_ ( F ` ( 2 ^ ( j + 1 ) ) ) )
106	71, 82, 88, 105	fsumle 13247	. . . . . . . 8 |- ( ( ph /\ j e. NN0 ) -> sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` k ) <_ sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` ( 2 ^ ( j + 1 ) ) ) )
107		fzfid 11781	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. NN0 ) -> ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) e. Fin )
108		hashcl 12112	. . . . . . . . . . . . 13 |- ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) e. Fin -> ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) e. NN0 )
109	107, 108	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN0 ) -> ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) e. NN0 )
110	109	nn0cnd 10628	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN0 ) -> ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) e. CC )
111	78	nnred 10327	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. RR )
112	111	recnd 9402	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. CC )
113		hashcl 12112	. . . . . . . . . . . . 13 |- ( ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) e. Fin -> ( # ` ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) e. NN0 )
114	71, 113	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN0 ) -> ( # ` ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) e. NN0 )
115	114	nn0cnd 10628	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN0 ) -> ( # ` ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) e. CC )
116		2z 10668	. . . . . . . . . . . . . . . . . . . 20 |- 2 e. ZZ
117		zexpcl 11866	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 2 e. ZZ /\ ( j + 1 ) e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. ZZ )
118	116, 76, 117	sylancr 658	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. ZZ )
119		nn0p1nn 10609	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j e. NN0 -> ( j + 1 ) e. NN )
120	119	adantl 463	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ j e. NN0 ) -> ( j + 1 ) e. NN )
121		nnuz 10886	. . . . . . . . . . . . . . . . . . . . . 22 |- NN = ( ZZ>= ` 1 )
122	120, 121	syl6eleq 2525	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ j e. NN0 ) -> ( j + 1 ) e. ( ZZ>= ` 1 ) )
123		2re 10381	. . . . . . . . . . . . . . . . . . . . . 22 |- 2 e. RR
124		1le2 10525	. . . . . . . . . . . . . . . . . . . . . 22 |- 1 <_ 2
125		leexp2a 11905	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 2 e. RR /\ 1 <_ 2 /\ ( j + 1 ) e. ( ZZ>= ` 1 ) ) -> ( 2 ^ 1 ) <_ ( 2 ^ ( j + 1 ) ) )
126	123, 124, 125	mp3an12 1299	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( j + 1 ) e. ( ZZ>= ` 1 ) -> ( 2 ^ 1 ) <_ ( 2 ^ ( j + 1 ) ) )
127	122, 126	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ 1 ) <_ ( 2 ^ ( j + 1 ) ) )
128	7, 127	syl5eqbrr 4316	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. NN0 ) -> 2 <_ ( 2 ^ ( j + 1 ) ) )
129	116	eluz1i 10858	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2 ^ ( j + 1 ) ) e. ( ZZ>= ` 2 ) <-> ( ( 2 ^ ( j + 1 ) ) e. ZZ /\ 2 <_ ( 2 ^ ( j + 1 ) ) ) )
130	118, 128, 129	sylanbrc 659	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. ( ZZ>= ` 2 ) )
131		uz2m1nn 10919	. . . . . . . . . . . . . . . . . 18 |- ( ( 2 ^ ( j + 1 ) ) e. ( ZZ>= ` 2 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. NN )
132	130, 131	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. NN )
133	132, 121	syl6eleq 2525	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. ( ZZ>= ` 1 ) )
134		peano2zm 10678	. . . . . . . . . . . . . . . . . 18 |- ( ( 2 ^ ( j + 1 ) ) e. ZZ -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. ZZ )
135	118, 134	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. ZZ )
136		peano2nn0 10610	. . . . . . . . . . . . . . . . . . . 20 |- ( ( j + 1 ) e. NN0 -> ( ( j + 1 ) + 1 ) e. NN0 )
137	76, 136	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. NN0 ) -> ( ( j + 1 ) + 1 ) e. NN0 )
138		zexpcl 11866	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2 e. ZZ /\ ( ( j + 1 ) + 1 ) e. NN0 ) -> ( 2 ^ ( ( j + 1 ) + 1 ) ) e. ZZ )
139	116, 137, 138	sylancr 658	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( ( j + 1 ) + 1 ) ) e. ZZ )
140		peano2zm 10678	. . . . . . . . . . . . . . . . . 18 |- ( ( 2 ^ ( ( j + 1 ) + 1 ) ) e. ZZ -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. ZZ )
141	139, 140	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. ZZ )
142	118	zred 10737	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. RR )
143	139	zred 10737	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( ( j + 1 ) + 1 ) ) e. RR )
144		1red 9391	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN0 ) -> 1 e. RR )
145	76	nn0zd 10735	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. NN0 ) -> ( j + 1 ) e. ZZ )
146		uzid 10865	. . . . . . . . . . . . . . . . . . 19 |- ( ( j + 1 ) e. ZZ -> ( j + 1 ) e. ( ZZ>= ` ( j + 1 ) ) )
147		peano2uz 10898	. . . . . . . . . . . . . . . . . . 19 |- ( ( j + 1 ) e. ( ZZ>= ` ( j + 1 ) ) -> ( ( j + 1 ) + 1 ) e. ( ZZ>= ` ( j + 1 ) ) )
148		leexp2a 11905	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 2 e. RR /\ 1 <_ 2 /\ ( ( j + 1 ) + 1 ) e. ( ZZ>= ` ( j + 1 ) ) ) -> ( 2 ^ ( j + 1 ) ) <_ ( 2 ^ ( ( j + 1 ) + 1 ) ) )
149	123, 124, 148	mp3an12 1299	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( j + 1 ) + 1 ) e. ( ZZ>= ` ( j + 1 ) ) -> ( 2 ^ ( j + 1 ) ) <_ ( 2 ^ ( ( j + 1 ) + 1 ) ) )
150	145, 146, 147, 149	4syl 21	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) <_ ( 2 ^ ( ( j + 1 ) + 1 ) ) )
151	142, 143, 144, 150	lesub1dd 9945	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) <_ ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) )
152		eluz2 10857	. . . . . . . . . . . . . . . . 17 |- ( ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. ( ZZ>= ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) <-> ( ( ( 2 ^ ( j + 1 ) ) - 1 ) e. ZZ /\ ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. ZZ /\ ( ( 2 ^ ( j + 1 ) ) - 1 ) <_ ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) )
153	135, 141, 151, 152	syl3anbrc 1167	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. ( ZZ>= ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) )
154		elfzuzb 11436	. . . . . . . . . . . . . . . 16 |- ( ( ( 2 ^ ( j + 1 ) ) - 1 ) e. ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) <-> ( ( ( 2 ^ ( j + 1 ) ) - 1 ) e. ( ZZ>= ` 1 ) /\ ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. ( ZZ>= ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) )
155	133, 153, 154	sylanbrc 659	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) )
156		fzsplit 11464	. . . . . . . . . . . . . . 15 |- ( ( ( 2 ^ ( j + 1 ) ) - 1 ) e. ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) -> ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) = ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) u. ( ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + 1 ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) )
157	155, 156	syl 16	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN0 ) -> ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) = ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) u. ( ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + 1 ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) )
158		npcan 9609	. . . . . . . . . . . . . . . . 17 |- ( ( ( 2 ^ ( j + 1 ) ) e. CC /\ 1 e. CC ) -> ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + 1 ) = ( 2 ^ ( j + 1 ) ) )
159	112, 12, 158	sylancl 657	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN0 ) -> ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + 1 ) = ( 2 ^ ( j + 1 ) ) )
160	159	oveq1d 6097	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN0 ) -> ( ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + 1 ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) = ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) )
161	160	uneq2d 3500	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN0 ) -> ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) u. ( ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + 1 ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) = ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) u. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) )
162	157, 161	eqtrd 2467	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. NN0 ) -> ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) = ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) u. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) )
163	162	fveq2d 5685	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN0 ) -> ( # ` ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) = ( # ` ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) u. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) ) )
164		expp1 11858	. . . . . . . . . . . . . . . . 17 |- ( ( 2 e. CC /\ ( j + 1 ) e. NN0 ) -> ( 2 ^ ( ( j + 1 ) + 1 ) ) = ( ( 2 ^ ( j + 1 ) ) x. 2 ) )
165	5, 76, 164	sylancr 658	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( ( j + 1 ) + 1 ) ) = ( ( 2 ^ ( j + 1 ) ) x. 2 ) )
166	112	times2d 10558	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) x. 2 ) = ( ( 2 ^ ( j + 1 ) ) + ( 2 ^ ( j + 1 ) ) ) )
167	165, 166	eqtrd 2467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( ( j + 1 ) + 1 ) ) = ( ( 2 ^ ( j + 1 ) ) + ( 2 ^ ( j + 1 ) ) ) )
168	167	oveq1d 6097	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) = ( ( ( 2 ^ ( j + 1 ) ) + ( 2 ^ ( j + 1 ) ) ) - 1 ) )
169	12	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN0 ) -> 1 e. CC )
170	112, 112, 169	addsubd 9730	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN0 ) -> ( ( ( 2 ^ ( j + 1 ) ) + ( 2 ^ ( j + 1 ) ) ) - 1 ) = ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + ( 2 ^ ( j + 1 ) ) ) )
171	168, 170	eqtrd 2467	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) = ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + ( 2 ^ ( j + 1 ) ) ) )
172		uztrn 10867	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. ( ZZ>= ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) /\ ( ( 2 ^ ( j + 1 ) ) - 1 ) e. ( ZZ>= ` 1 ) ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. ( ZZ>= ` 1 ) )
173	153, 133, 172	syl2anc 656	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. ( ZZ>= ` 1 ) )
174	173, 121	syl6eleqr 2526	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. NN )
175	174	nnnn0d 10626	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. NN0 )
176		hashfz1 12103	. . . . . . . . . . . . . 14 |- ( ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. NN0 -> ( # ` ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) = ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) )
177	175, 176	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. NN0 ) -> ( # ` ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) = ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) )
178	132	nnnn0d 10626	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. NN0 )
179		hashfz1 12103	. . . . . . . . . . . . . . 15 |- ( ( ( 2 ^ ( j + 1 ) ) - 1 ) e. NN0 -> ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) = ( ( 2 ^ ( j + 1 ) ) - 1 ) )
180	178, 179	syl 16	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN0 ) -> ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) = ( ( 2 ^ ( j + 1 ) ) - 1 ) )
181	180	oveq1d 6097	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. NN0 ) -> ( ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) + ( 2 ^ ( j + 1 ) ) ) = ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + ( 2 ^ ( j + 1 ) ) ) )
182	171, 177, 181	3eqtr4d 2477	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN0 ) -> ( # ` ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) = ( ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) + ( 2 ^ ( j + 1 ) ) ) )
183	111	ltm1d 10255	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) < ( 2 ^ ( j + 1 ) ) )
184		fzdisj 11465	. . . . . . . . . . . . . 14 |- ( ( ( 2 ^ ( j + 1 ) ) - 1 ) < ( 2 ^ ( j + 1 ) ) -> ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) i^i ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) = (/) )
185	183, 184	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. NN0 ) -> ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) i^i ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) = (/) )
186		hashun 12131	. . . . . . . . . . . . 13 |- ( ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) e. Fin /\ ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) e. Fin /\ ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) i^i ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) = (/) ) -> ( # ` ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) u. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) ) = ( ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) + ( # ` ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) ) )
187	107, 71, 185, 186	syl3anc 1213	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN0 ) -> ( # ` ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) u. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) ) = ( ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) + ( # ` ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) ) )
188	163, 182, 187	3eqtr3d 2475	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN0 ) -> ( ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) + ( 2 ^ ( j + 1 ) ) ) = ( ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) + ( # ` ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) ) )
189	110, 112, 115, 188	addcanad 9564	. . . . . . . . . 10 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) = ( # ` ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) )
190	189	oveq1d 6097	. . . . . . . . 9 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) x. ( F ` ( 2 ^ ( j + 1 ) ) ) ) = ( ( # ` ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) x. ( F ` ( 2 ^ ( j + 1 ) ) ) ) )
191	58	adantr 462	. . . . . . . . . 10 |- ( ( ph /\ j e. NN0 ) -> A. n e. NN0 ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) )
192		fveq2 5681	. . . . . . . . . . . 12 |- ( n = ( j + 1 ) -> ( G ` n ) = ( G ` ( j + 1 ) ) )
193		oveq2 6090	. . . . . . . . . . . . 13 |- ( n = ( j + 1 ) -> ( 2 ^ n ) = ( 2 ^ ( j + 1 ) ) )
194	193	fveq2d 5685	. . . . . . . . . . . . 13 |- ( n = ( j + 1 ) -> ( F ` ( 2 ^ n ) ) = ( F ` ( 2 ^ ( j + 1 ) ) ) )
195	193, 194	oveq12d 6100	. . . . . . . . . . . 12 |- ( n = ( j + 1 ) -> ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) = ( ( 2 ^ ( j + 1 ) ) x. ( F ` ( 2 ^ ( j + 1 ) ) ) ) )
196	192, 195	eqeq12d 2449	. . . . . . . . . . 11 |- ( n = ( j + 1 ) -> ( ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) <-> ( G ` ( j + 1 ) ) = ( ( 2 ^ ( j + 1 ) ) x. ( F ` ( 2 ^ ( j + 1 ) ) ) ) ) )
197	196	rspcv 3060	. . . . . . . . . 10 |- ( ( j + 1 ) e. NN0 -> ( A. n e. NN0 ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) -> ( G ` ( j + 1 ) ) = ( ( 2 ^ ( j + 1 ) ) x. ( F ` ( 2 ^ ( j + 1 ) ) ) ) ) )
198	76, 191, 197	sylc 60	. . . . . . . . 9 |- ( ( ph /\ j e. NN0 ) -> ( G ` ( j + 1 ) ) = ( ( 2 ^ ( j + 1 ) ) x. ( F ` ( 2 ^ ( j + 1 ) ) ) ) )
199	87	recnd 9402	. . . . . . . . . 10 |- ( ( ph /\ j e. NN0 ) -> ( F ` ( 2 ^ ( j + 1 ) ) ) e. CC )
200		fsumconst 13242	. . . . . . . . . 10 |- ( ( ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) e. Fin /\ ( F ` ( 2 ^ ( j + 1 ) ) ) e. CC ) -> sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` ( 2 ^ ( j + 1 ) ) ) = ( ( # ` ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) x. ( F ` ( 2 ^ ( j + 1 ) ) ) ) )
201	71, 199, 200	syl2anc 656	. . . . . . . . 9 |- ( ( ph /\ j e. NN0 ) -> sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` ( 2 ^ ( j + 1 ) ) ) = ( ( # ` ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) x. ( F ` ( 2 ^ ( j + 1 ) ) ) ) )
202	190, 198, 201	3eqtr4d 2477	. . . . . . . 8 |- ( ( ph /\ j e. NN0 ) -> ( G ` ( j + 1 ) ) = sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` ( 2 ^ ( j + 1 ) ) ) )
203	106, 202	breqtrrd 4308	. . . . . . 7 |- ( ( ph /\ j e. NN0 ) -> sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` k ) <_ ( G ` ( j + 1 ) ) )
204		elfznn 11467	. . . . . . . . . 10 |- ( k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) -> k e. NN )
205	72, 204, 42	syl2an 474	. . . . . . . . 9 |- ( ( ( ph /\ j e. NN0 ) /\ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) -> ( F ` k ) e. RR )
206	107, 205	fsumrecl 13197	. . . . . . . 8 |- ( ( ph /\ j e. NN0 ) -> sum_ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ( F ` k ) e. RR )
207	71, 82	fsumrecl 13197	. . . . . . . 8 |- ( ( ph /\ j e. NN0 ) -> sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` k ) e. RR )
208		nn0uz 10885	. . . . . . . . . 10 |- NN0 = ( ZZ>= ` 0 )
209		0zd 10648	. . . . . . . . . 10 |- ( ph -> 0 e. ZZ )
210		simpr 458	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. NN0 ) -> n e. NN0 )
211		nnexpcl 11864	. . . . . . . . . . . . . 14 |- ( ( 2 e. NN /\ n e. NN0 ) -> ( 2 ^ n ) e. NN )
212	74, 210, 211	sylancr 658	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN0 ) -> ( 2 ^ n ) e. NN )
213	212	nnred 10327	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN0 ) -> ( 2 ^ n ) e. RR )
214	43	adantr 462	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN0 ) -> A. k e. NN ( F ` k ) e. RR )
215		fveq2 5681	. . . . . . . . . . . . . . 15 |- ( k = ( 2 ^ n ) -> ( F ` k ) = ( F ` ( 2 ^ n ) ) )
216	215	eleq1d 2501	. . . . . . . . . . . . . 14 |- ( k = ( 2 ^ n ) -> ( ( F ` k ) e. RR <-> ( F ` ( 2 ^ n ) ) e. RR ) )
217	216	rspcv 3060	. . . . . . . . . . . . 13 |- ( ( 2 ^ n ) e. NN -> ( A. k e. NN ( F ` k ) e. RR -> ( F ` ( 2 ^ n ) ) e. RR ) )
218	212, 214, 217	sylc 60	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN0 ) -> ( F ` ( 2 ^ n ) ) e. RR )
219	213, 218	remulcld 9404	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN0 ) -> ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) e. RR )
220	57, 219	eqeltrd 2509	. . . . . . . . . 10 |- ( ( ph /\ n e. NN0 ) -> ( G ` n ) e. RR )
221	208, 209, 220	serfre 11821	. . . . . . . . 9 |- ( ph -> seq 0 ( + , G ) : NN0 --> RR )
222	221	ffvelrnda 5833	. . . . . . . 8 |- ( ( ph /\ j e. NN0 ) -> ( seq 0 ( + , G ) ` j ) e. RR )
223	142, 87	remulcld 9404	. . . . . . . . 9 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) x. ( F ` ( 2 ^ ( j + 1 ) ) ) ) e. RR )
224	198, 223	eqeltrd 2509	. . . . . . . 8 |- ( ( ph /\ j e. NN0 ) -> ( G ` ( j + 1 ) ) e. RR )
225		le2add 9811	. . . . . . . 8 |- ( ( ( sum_ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ( F ` k ) e. RR /\ sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` k ) e. RR ) /\ ( ( seq 0 ( + , G ) ` j ) e. RR /\ ( G ` ( j + 1 ) ) e. RR ) ) -> ( ( sum_ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ( F ` k ) <_ ( seq 0 ( + , G ) ` j ) /\ sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` k ) <_ ( G ` ( j + 1 ) ) ) -> ( sum_ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ( F ` k ) + sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` k ) ) <_ ( ( seq 0 ( + , G ) ` j ) + ( G ` ( j + 1 ) ) ) ) )
226	206, 207, 222, 224, 225	syl22anc 1214	. . . . . . 7 |- ( ( ph /\ j e. NN0 ) -> ( ( sum_ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ( F ` k ) <_ ( seq 0 ( + , G ) ` j ) /\ sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` k ) <_ ( G ` ( j + 1 ) ) ) -> ( sum_ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ( F ` k ) + sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` k ) ) <_ ( ( seq 0 ( + , G ) ` j ) + ( G ` ( j + 1 ) ) ) ) )
227	203, 226	mpan2d 669	. . . . . 6 |- ( ( ph /\ j e. NN0 ) -> ( sum_ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ( F ` k ) <_ ( seq 0 ( + , G ) ` j ) -> ( sum_ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ( F ` k ) + sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` k ) ) <_ ( ( seq 0 ( + , G ) ` j ) + ( G ` ( j + 1 ) ) ) ) )
228		eqidd 2436	. . . . . . . . 9 |- ( ( ( ph /\ j e. NN0 ) /\ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) -> ( F ` k ) = ( F ` k ) )
229	42	recnd 9402	. . . . . . . . . 10 |- ( ( ph /\ k e. NN ) -> ( F ` k ) e. CC )
230	72, 204, 229	syl2an 474	. . . . . . . . 9 |- ( ( ( ph /\ j e. NN0 ) /\ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) -> ( F ` k ) e. CC )
231	228, 133, 230	fsumser 13193	. . . . . . . 8 |- ( ( ph /\ j e. NN0 ) -> sum_ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ( F ` k ) = ( seq 1 ( + , F ) ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) )
232	231	eqcomd 2440	. . . . . . 7 |- ( ( ph /\ j e. NN0 ) -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) = sum_ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ( F ` k ) )
233	232	breq1d 4292	. . . . . 6 |- ( ( ph /\ j e. NN0 ) -> ( ( seq 1 ( + , F ) ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` j ) <-> sum_ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ( F ` k ) <_ ( seq 0 ( + , G ) ` j ) ) )
234		eqidd 2436	. . . . . . . . 9 |- ( ( ( ph /\ j e. NN0 ) /\ k e. ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) -> ( F ` k ) = ( F ` k ) )
235		elfznn 11467	. . . . . . . . . 10 |- ( k e. ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) -> k e. NN )
236	72, 235, 229	syl2an 474	. . . . . . . . 9 |- ( ( ( ph /\ j e. NN0 ) /\ k e. ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) -> ( F ` k ) e. CC )
237	234, 173, 236	fsumser 13193	. . . . . . . 8 |- ( ( ph /\ j e. NN0 ) -> sum_ k e. ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` k ) = ( seq 1 ( + , F ) ` ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) )
238		fzfid 11781	. . . . . . . . 9 |- ( ( ph /\ j e. NN0 ) -> ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) e. Fin )
239	185, 162, 238, 236	fsumsplit 13202	. . . . . . . 8 |- ( ( ph /\ j e. NN0 ) -> sum_ k e. ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` k ) = ( sum_ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ( F ` k ) + sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` k ) ) )
240	237, 239	eqtr3d 2469	. . . . . . 7 |- ( ( ph /\ j e. NN0 ) -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) = ( sum_ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ( F ` k ) + sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` k ) ) )
241		simpr 458	. . . . . . . . 9 |- ( ( ph /\ j e. NN0 ) -> j e. NN0 )
242	241, 208	syl6eleq 2525	. . . . . . . 8 |- ( ( ph /\ j e. NN0 ) -> j e. ( ZZ>= ` 0 ) )
243		seqp1 11807	. . . . . . . 8 |- ( j e. ( ZZ>= ` 0 ) -> ( seq 0 ( + , G ) ` ( j + 1 ) ) = ( ( seq 0 ( + , G ) ` j ) + ( G ` ( j + 1 ) ) ) )
244	242, 243	syl 16	. . . . . . 7 |- ( ( ph /\ j e. NN0 ) -> ( seq 0 ( + , G ) ` ( j + 1 ) ) = ( ( seq 0 ( + , G ) ` j ) + ( G ` ( j + 1 ) ) ) )
245	240, 244	breq12d 4295	. . . . . 6 |- ( ( ph /\ j e. NN0 ) -> ( ( seq 1 ( + , F ) ` ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` ( j + 1 ) ) <-> ( sum_ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ( F ` k ) + sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` k ) ) <_ ( ( seq 0 ( + , G ) ` j ) + ( G ` ( j + 1 ) ) ) ) )
246	227, 233, 245	3imtr4d 268	. . . . 5 |- ( ( ph /\ j e. NN0 ) -> ( ( seq 1 ( + , F ) ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` j ) -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` ( j + 1 ) ) ) )
247	246	expcom 435	. . . 4 |- ( j e. NN0 -> ( ph -> ( ( seq 1 ( + , F ) ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` j ) -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` ( j + 1 ) ) ) ) )
248	247	a2d 26	. . 3 |- ( j e. NN0 -> ( ( ph -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` j ) ) -> ( ph -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` ( j + 1 ) ) ) ) )
249	19, 26, 33, 40, 70, 248	nn0ind 10728	. 2 |- ( N e. NN0 -> ( ph -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( N + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` N ) ) )
250	249	impcom 430	1 |- ( ( ph /\ N e. NN0 ) -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( N + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` N ) )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1364   e. wcel 1757   A.wral 2707   u. cun 3316   i^i cin 3317   (/)c0 3627   class class class wbr 4282   ` cfv 5408  (class class class)co 6082   Fincfn 7300   CCcc 9270   RRcr 9271   0cc0 9272   1c1 9273   + caddc 9275   x. cmul 9277   < clt 9408   <_ cle 9409   - cmin 9585   NNcn 10312   2c2 10361   NN0cn0 10569   ZZcz 10636   ZZ>=cuz 10851   ...cfz 11426   seqcseq 11792   ^cexp 11851   #chash 12089   sum_csu 13149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-rep 4393  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363  ax-inf2 7837  ax-cnex 9328  ax-resscn 9329  ax-1cn 9330  ax-icn 9331  ax-addcl 9332  ax-addrcl 9333  ax-mulcl 9334  ax-mulrcl 9335  ax-mulcom 9336  ax-addass 9337  ax-mulass 9338  ax-distr 9339  ax-i2m1 9340  ax-1ne0 9341  ax-1rid 9342  ax-rnegex 9343  ax-rrecex 9344  ax-cnre 9345  ax-pre-lttri 9346  ax-pre-lttrn 9347  ax-pre-ltadd 9348  ax-pre-mulgt0 9349  ax-pre-sup 9350

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-fal 1370  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-pss 3334  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-tp 3872  df-op 3874  df-uni 4082  df-int 4119  df-iun 4163  df-br 4283  df-opab 4341  df-mpt 4342  df-tr 4376  df-eprel 4621  df-id 4625  df-po 4630  df-so 4631  df-fr 4668  df-se 4669  df-we 4670  df-ord 4711  df-on 4712  df-lim 4713  df-suc 4714  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-isom 5417  df-riota 6041  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-om 6468  df-1st 6568  df-2nd 6569  df-recs 6820  df-rdg 6854  df-1o 6910  df-oadd 6914  df-er 7091  df-en 7301  df-dom 7302  df-sdom 7303  df-fin 7304  df-sup 7681  df-oi 7714  df-card 8099  df-cda 8327  df-pnf 9410  df-mnf 9411  df-xr 9412  df-ltxr 9413  df-le 9414  df-sub 9587  df-neg 9588  df-div 9984  df-nn 10313  df-2 10370  df-3 10371  df-n0 10570  df-z 10637  df-uz 10852  df-rp 10982  df-ico 11296  df-fz 11427  df-fzo 11535  df-seq 11793  df-exp 11852  df-hash 12090  df-cj 12574  df-re 12575  df-im 12576  df-sqr 12710  df-abs 12711  df-clim 12952  df-sum 13150

This theorem is referenced by:  climcnds  13299