Theorem climcndslem1 12584

Description: Lemma for climcnds 12586: 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 6047	. . . . . . . . . . 11 |- ( x = 0 -> ( x + 1 ) = ( 0 + 1 ) )
2		0p1e1 10049	. . . . . . . . . . 11 |- ( 0 + 1 ) = 1
3	1, 2	syl6eq 2452	. . . . . . . . . 10 |- ( x = 0 -> ( x + 1 ) = 1 )
4	3	oveq2d 6056	. . . . . . . . 9 |- ( x = 0 -> ( 2 ^ ( x + 1 ) ) = ( 2 ^ 1 ) )
5		2cn 10026	. . . . . . . . . . 11 |- 2 e. CC
6		exp1 11342	. . . . . . . . . . 11 |- ( 2 e. CC -> ( 2 ^ 1 ) = 2 )
7	5, 6	ax-mp 8	. . . . . . . . . 10 |- ( 2 ^ 1 ) = 2
8		df-2 10014	. . . . . . . . . 10 |- 2 = ( 1 + 1 )
9	7, 8	eqtri 2424	. . . . . . . . 9 |- ( 2 ^ 1 ) = ( 1 + 1 )
10	4, 9	syl6eq 2452	. . . . . . . 8 |- ( x = 0 -> ( 2 ^ ( x + 1 ) ) = ( 1 + 1 ) )
11	10	oveq1d 6055	. . . . . . 7 |- ( x = 0 -> ( ( 2 ^ ( x + 1 ) ) - 1 ) = ( ( 1 + 1 ) - 1 ) )
12		ax-1cn 9004	. . . . . . . 8 |- 1 e. CC
13		pncan 9267	. . . . . . . 8 |- ( ( 1 e. CC /\ 1 e. CC ) -> ( ( 1 + 1 ) - 1 ) = 1 )
14	12, 12, 13	mp2an 654	. . . . . . 7 |- ( ( 1 + 1 ) - 1 ) = 1
15	11, 14	syl6eq 2452	. . . . . 6 |- ( x = 0 -> ( ( 2 ^ ( x + 1 ) ) - 1 ) = 1 )
16	15	fveq2d 5691	. . . . 5 |- ( x = 0 -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) = ( seq 1 ( + , F ) ` 1 ) )
17		fveq2 5687	. . . . 5 |- ( x = 0 -> ( seq 0 ( + , G ) ` x ) = ( seq 0 ( + , G ) ` 0 ) )
18	16, 17	breq12d 4185	. . . 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 308	. . 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 6047	. . . . . . . 8 |- ( x = j -> ( x + 1 ) = ( j + 1 ) )
21	20	oveq2d 6056	. . . . . . 7 |- ( x = j -> ( 2 ^ ( x + 1 ) ) = ( 2 ^ ( j + 1 ) ) )
22	21	oveq1d 6055	. . . . . 6 |- ( x = j -> ( ( 2 ^ ( x + 1 ) ) - 1 ) = ( ( 2 ^ ( j + 1 ) ) - 1 ) )
23	22	fveq2d 5691	. . . . 5 |- ( x = j -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) = ( seq 1 ( + , F ) ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) )
24		fveq2 5687	. . . . 5 |- ( x = j -> ( seq 0 ( + , G ) ` x ) = ( seq 0 ( + , G ) ` j ) )
25	23, 24	breq12d 4185	. . . 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 308	. . 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 6047	. . . . . . . 8 |- ( x = ( j + 1 ) -> ( x + 1 ) = ( ( j + 1 ) + 1 ) )
28	27	oveq2d 6056	. . . . . . 7 |- ( x = ( j + 1 ) -> ( 2 ^ ( x + 1 ) ) = ( 2 ^ ( ( j + 1 ) + 1 ) ) )
29	28	oveq1d 6055	. . . . . 6 |- ( x = ( j + 1 ) -> ( ( 2 ^ ( x + 1 ) ) - 1 ) = ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) )
30	29	fveq2d 5691	. . . . 5 |- ( x = ( j + 1 ) -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) = ( seq 1 ( + , F ) ` ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) )
31		fveq2 5687	. . . . 5 |- ( x = ( j + 1 ) -> ( seq 0 ( + , G ) ` x ) = ( seq 0 ( + , G ) ` ( j + 1 ) ) )
32	30, 31	breq12d 4185	. . . 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 308	. . 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 6047	. . . . . . . 8 |- ( x = N -> ( x + 1 ) = ( N + 1 ) )
35	34	oveq2d 6056	. . . . . . 7 |- ( x = N -> ( 2 ^ ( x + 1 ) ) = ( 2 ^ ( N + 1 ) ) )
36	35	oveq1d 6055	. . . . . 6 |- ( x = N -> ( ( 2 ^ ( x + 1 ) ) - 1 ) = ( ( 2 ^ ( N + 1 ) ) - 1 ) )
37	36	fveq2d 5691	. . . . 5 |- ( x = N -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) = ( seq 1 ( + , F ) ` ( ( 2 ^ ( N + 1 ) ) - 1 ) ) )
38		fveq2 5687	. . . . 5 |- ( x = N -> ( seq 0 ( + , G ) ` x ) = ( seq 0 ( + , G ) ` N ) )
39	37, 38	breq12d 4185	. . . 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 308	. . 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 9967	. . . . . . 7 |- 1 e. NN
42		climcnds.1	. . . . . . . 8 |- ( ( ph /\ k e. NN ) -> ( F ` k ) e. RR )
43	42	ralrimiva 2749	. . . . . . 7 |- ( ph -> A. k e. NN ( F ` k ) e. RR )
44		fveq2 5687	. . . . . . . . 9 |- ( k = 1 -> ( F ` k ) = ( F ` 1 ) )
45	44	eleq1d 2470	. . . . . . . 8 |- ( k = 1 -> ( ( F ` k ) e. RR <-> ( F ` 1 ) e. RR ) )
46	45	rspcv 3008	. . . . . . 7 |- ( 1 e. NN -> ( A. k e. NN ( F ` k ) e. RR -> ( F ` 1 ) e. RR ) )
47	41, 43, 46	mpsyl 61	. . . . . 6 |- ( ph -> ( F ` 1 ) e. RR )
48	47	leidd 9549	. . . . 5 |- ( ph -> ( F ` 1 ) <_ ( F ` 1 ) )
49	47	recnd 9070	. . . . . 6 |- ( ph -> ( F ` 1 ) e. CC )
50	49	mulid2d 9062	. . . . 5 |- ( ph -> ( 1 x. ( F ` 1 ) ) = ( F ` 1 ) )
51	48, 50	breqtrrd 4198	. . . 4 |- ( ph -> ( F ` 1 ) <_ ( 1 x. ( F ` 1 ) ) )
52		1z 10267	. . . . 5 |- 1 e. ZZ
53		eqidd 2405	. . . . 5 |- ( ph -> ( F ` 1 ) = ( F ` 1 ) )
54	52, 53	seq1i 11292	. . . 4 |- ( ph -> ( seq 1 ( + , F ) ` 1 ) = ( F ` 1 ) )
55		0z 10249	. . . . 5 |- 0 e. ZZ
56		0nn0 10192	. . . . . 6 |- 0 e. NN0
57		climcnds.4	. . . . . . 7 |- ( ( ph /\ n e. NN0 ) -> ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) )
58	57	ralrimiva 2749	. . . . . 6 |- ( ph -> A. n e. NN0 ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) )
59		fveq2 5687	. . . . . . . 8 |- ( n = 0 -> ( G ` n ) = ( G ` 0 ) )
60		oveq2 6048	. . . . . . . . . 10 |- ( n = 0 -> ( 2 ^ n ) = ( 2 ^ 0 ) )
61		exp0 11341	. . . . . . . . . . 11 |- ( 2 e. CC -> ( 2 ^ 0 ) = 1 )
62	5, 61	ax-mp 8	. . . . . . . . . 10 |- ( 2 ^ 0 ) = 1
63	60, 62	syl6eq 2452	. . . . . . . . 9 |- ( n = 0 -> ( 2 ^ n ) = 1 )
64	63	fveq2d 5691	. . . . . . . . 9 |- ( n = 0 -> ( F ` ( 2 ^ n ) ) = ( F ` 1 ) )
65	63, 64	oveq12d 6058	. . . . . . . 8 |- ( n = 0 -> ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) = ( 1 x. ( F ` 1 ) ) )
66	59, 65	eqeq12d 2418	. . . . . . 7 |- ( n = 0 -> ( ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) <-> ( G ` 0 ) = ( 1 x. ( F ` 1 ) ) ) )
67	66	rspcv 3008	. . . . . 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 61	. . . . 5 |- ( ph -> ( G ` 0 ) = ( 1 x. ( F ` 1 ) ) )
69	55, 68	seq1i 11292	. . . 4 |- ( ph -> ( seq 0 ( + , G ) ` 0 ) = ( 1 x. ( F ` 1 ) ) )
70	51, 54, 69	3brtr4d 4202	. . 3 |- ( ph -> ( seq 1 ( + , F ) ` 1 ) <_ ( seq 0 ( + , G ) ` 0 ) )
71		fzfid 11267	. . . . . . . . 9 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) e. Fin )
72		simpl 444	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN0 ) -> ph )
73	72	adantr 452	. . . . . . . . . 10 |- ( ( ( ph /\ j e. NN0 ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) -> ph )
74		2nn 10089	. . . . . . . . . . . 12 |- 2 e. NN
75		peano2nn0 10216	. . . . . . . . . . . . 13 |- ( j e. NN0 -> ( j + 1 ) e. NN0 )
76	75	adantl 453	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN0 ) -> ( j + 1 ) e. NN0 )
77		nnexpcl 11349	. . . . . . . . . . . 12 |- ( ( 2 e. NN /\ ( j + 1 ) e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. NN )
78	74, 76, 77	sylancr 645	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. NN )
79		elfzuz 11011	. . . . . . . . . . 11 |- ( k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) -> k e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) )
80		nnuz 10477	. . . . . . . . . . . 12 |- NN = ( ZZ>= ` 1 )
81	80	uztrn2 10459	. . . . . . . . . . 11 |- ( ( ( 2 ^ ( j + 1 ) ) e. NN /\ k e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) -> k e. NN )
82	78, 79, 81	syl2an 464	. . . . . . . . . 10 |- ( ( ( ph /\ j e. NN0 ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) -> k e. NN )
83	73, 82, 42	syl2anc 643	. . . . . . . . 9 |- ( ( ( ph /\ j e. NN0 ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) -> ( F ` k ) e. RR )
84	43	adantr 452	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN0 ) -> A. k e. NN ( F ` k ) e. RR )
85		fveq2 5687	. . . . . . . . . . . . 13 |- ( k = ( 2 ^ ( j + 1 ) ) -> ( F ` k ) = ( F ` ( 2 ^ ( j + 1 ) ) ) )
86	85	eleq1d 2470	. . . . . . . . . . . 12 |- ( k = ( 2 ^ ( j + 1 ) ) -> ( ( F ` k ) e. RR <-> ( F ` ( 2 ^ ( j + 1 ) ) ) e. RR ) )
87	86	rspcv 3008	. . . . . . . . . . 11 |- ( ( 2 ^ ( j + 1 ) ) e. NN -> ( A. k e. NN ( F ` k ) e. RR -> ( F ` ( 2 ^ ( j + 1 ) ) ) e. RR ) )
88	78, 84, 87	sylc 58	. . . . . . . . . 10 |- ( ( ph /\ j e. NN0 ) -> ( F ` ( 2 ^ ( j + 1 ) ) ) e. RR )
89	88	adantr 452	. . . . . . . . 9 |- ( ( ( ph /\ j e. NN0 ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) -> ( F ` ( 2 ^ ( j + 1 ) ) ) e. RR )
90		simpr 448	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) -> n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) )
91		simplll 735	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... n ) ) -> ph )
92	78	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) -> ( 2 ^ ( j + 1 ) ) e. NN )
93		elfzuz 11011	. . . . . . . . . . . . . 14 |- ( k e. ( ( 2 ^ ( j + 1 ) ) ... n ) -> k e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) )
94	92, 93, 81	syl2an 464	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... n ) ) -> k e. NN )
95	91, 94, 42	syl2anc 643	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... n ) ) -> ( F ` k ) e. RR )
96		simplll 735	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( n - 1 ) ) ) -> ph )
97		elfzuz 11011	. . . . . . . . . . . . . 14 |- ( k e. ( ( 2 ^ ( j + 1 ) ) ... ( n - 1 ) ) -> k e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) )
98	92, 97, 81	syl2an 464	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( n - 1 ) ) ) -> k e. NN )
99		climcnds.3	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )
100	96, 98, 99	syl2anc 643	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( n - 1 ) ) ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )
101	90, 95, 100	monoord2 11309	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) -> ( F ` n ) <_ ( F ` ( 2 ^ ( j + 1 ) ) ) )
102	101	ralrimiva 2749	. . . . . . . . . 10 |- ( ( ph /\ j e. NN0 ) -> A. n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ( F ` n ) <_ ( F ` ( 2 ^ ( j + 1 ) ) ) )
103		fveq2 5687	. . . . . . . . . . . 12 |- ( n = k -> ( F ` n ) = ( F ` k ) )
104	103	breq1d 4182	. . . . . . . . . . 11 |- ( n = k -> ( ( F ` n ) <_ ( F ` ( 2 ^ ( j + 1 ) ) ) <-> ( F ` k ) <_ ( F ` ( 2 ^ ( j + 1 ) ) ) ) )
105	104	rspccva 3011	. . . . . . . . . 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 ) ) ) )
106	102, 79, 105	syl2an 464	. . . . . . . . 9 |- ( ( ( ph /\ j e. NN0 ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) -> ( F ` k ) <_ ( F ` ( 2 ^ ( j + 1 ) ) ) )
107	71, 83, 89, 106	fsumle 12533	. . . . . . . 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 ) ) ) )
108		fzfid 11267	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. NN0 ) -> ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) e. Fin )
109		hashcl 11594	. . . . . . . . . . . . 13 |- ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) e. Fin -> ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) e. NN0 )
110	108, 109	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN0 ) -> ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) e. NN0 )
111	110	nn0cnd 10232	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN0 ) -> ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) e. CC )
112	78	nnred 9971	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. RR )
113	112	recnd 9070	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. CC )
114		hashcl 11594	. . . . . . . . . . . . 13 |- ( ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) e. Fin -> ( # ` ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) e. NN0 )
115	71, 114	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN0 ) -> ( # ` ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) e. NN0 )
116	115	nn0cnd 10232	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN0 ) -> ( # ` ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) e. CC )
117		2z 10268	. . . . . . . . . . . . . . . . . . . 20 |- 2 e. ZZ
118		zexpcl 11351	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 2 e. ZZ /\ ( j + 1 ) e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. ZZ )
119	117, 76, 118	sylancr 645	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. ZZ )
120		nn0p1nn 10215	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j e. NN0 -> ( j + 1 ) e. NN )
121	120	adantl 453	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ j e. NN0 ) -> ( j + 1 ) e. NN )
122	121, 80	syl6eleq 2494	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ j e. NN0 ) -> ( j + 1 ) e. ( ZZ>= ` 1 ) )
123		2re 10025	. . . . . . . . . . . . . . . . . . . . . 22 |- 2 e. RR
124		1re 9046	. . . . . . . . . . . . . . . . . . . . . . 23 |- 1 e. RR
125		1lt2 10098	. . . . . . . . . . . . . . . . . . . . . . 23 |- 1 < 2
126	124, 123, 125	ltleii 9152	. . . . . . . . . . . . . . . . . . . . . 22 |- 1 <_ 2
127		leexp2a 11390	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 2 e. RR /\ 1 <_ 2 /\ ( j + 1 ) e. ( ZZ>= ` 1 ) ) -> ( 2 ^ 1 ) <_ ( 2 ^ ( j + 1 ) ) )
128	123, 126, 127	mp3an12 1269	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( j + 1 ) e. ( ZZ>= ` 1 ) -> ( 2 ^ 1 ) <_ ( 2 ^ ( j + 1 ) ) )
129	122, 128	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ 1 ) <_ ( 2 ^ ( j + 1 ) ) )
130	7, 129	syl5eqbrr 4206	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. NN0 ) -> 2 <_ ( 2 ^ ( j + 1 ) ) )
131	117	eluz1i 10451	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2 ^ ( j + 1 ) ) e. ( ZZ>= ` 2 ) <-> ( ( 2 ^ ( j + 1 ) ) e. ZZ /\ 2 <_ ( 2 ^ ( j + 1 ) ) ) )
132	119, 130, 131	sylanbrc 646	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. ( ZZ>= ` 2 ) )
133		uz2m1nn 10506	. . . . . . . . . . . . . . . . . 18 |- ( ( 2 ^ ( j + 1 ) ) e. ( ZZ>= ` 2 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. NN )
134	132, 133	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. NN )
135	134, 80	syl6eleq 2494	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. ( ZZ>= ` 1 ) )
136		peano2zm 10276	. . . . . . . . . . . . . . . . . 18 |- ( ( 2 ^ ( j + 1 ) ) e. ZZ -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. ZZ )
137	119, 136	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. ZZ )
138		peano2nn0 10216	. . . . . . . . . . . . . . . . . . . 20 |- ( ( j + 1 ) e. NN0 -> ( ( j + 1 ) + 1 ) e. NN0 )
139	76, 138	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. NN0 ) -> ( ( j + 1 ) + 1 ) e. NN0 )
140		zexpcl 11351	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2 e. ZZ /\ ( ( j + 1 ) + 1 ) e. NN0 ) -> ( 2 ^ ( ( j + 1 ) + 1 ) ) e. ZZ )
141	117, 139, 140	sylancr 645	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( ( j + 1 ) + 1 ) ) e. ZZ )
142		peano2zm 10276	. . . . . . . . . . . . . . . . . 18 |- ( ( 2 ^ ( ( j + 1 ) + 1 ) ) e. ZZ -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. ZZ )
143	141, 142	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. ZZ )
144	119	zred 10331	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. RR )
145	141	zred 10331	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( ( j + 1 ) + 1 ) ) e. RR )
146	124	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN0 ) -> 1 e. RR )
147	76	nn0zd 10329	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. NN0 ) -> ( j + 1 ) e. ZZ )
148		uzid 10456	. . . . . . . . . . . . . . . . . . . 20 |- ( ( j + 1 ) e. ZZ -> ( j + 1 ) e. ( ZZ>= ` ( j + 1 ) ) )
149	147, 148	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. NN0 ) -> ( j + 1 ) e. ( ZZ>= ` ( j + 1 ) ) )
150		peano2uz 10486	. . . . . . . . . . . . . . . . . . 19 |- ( ( j + 1 ) e. ( ZZ>= ` ( j + 1 ) ) -> ( ( j + 1 ) + 1 ) e. ( ZZ>= ` ( j + 1 ) ) )
151		leexp2a 11390	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 2 e. RR /\ 1 <_ 2 /\ ( ( j + 1 ) + 1 ) e. ( ZZ>= ` ( j + 1 ) ) ) -> ( 2 ^ ( j + 1 ) ) <_ ( 2 ^ ( ( j + 1 ) + 1 ) ) )
152	123, 126, 151	mp3an12 1269	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( j + 1 ) + 1 ) e. ( ZZ>= ` ( j + 1 ) ) -> ( 2 ^ ( j + 1 ) ) <_ ( 2 ^ ( ( j + 1 ) + 1 ) ) )
153	149, 150, 152	3syl 19	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) <_ ( 2 ^ ( ( j + 1 ) + 1 ) ) )
154	144, 145, 146, 153	lesub1dd 9598	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) <_ ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) )
155		eluz2 10450	. . . . . . . . . . . . . . . . 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 ) ) )
156	137, 143, 154, 155	syl3anbrc 1138	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. ( ZZ>= ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) )
157		elfzuzb 11009	. . . . . . . . . . . . . . . 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 ) ) ) )
158	135, 156, 157	sylanbrc 646	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) )
159		fzsplit 11033	. . . . . . . . . . . . . . 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 ) ) ) )
160	158, 159	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 ) ) ) )
161		npcan 9270	. . . . . . . . . . . . . . . . 17 |- ( ( ( 2 ^ ( j + 1 ) ) e. CC /\ 1 e. CC ) -> ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + 1 ) = ( 2 ^ ( j + 1 ) ) )
162	113, 12, 161	sylancl 644	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN0 ) -> ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + 1 ) = ( 2 ^ ( j + 1 ) ) )
163	162	oveq1d 6055	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN0 ) -> ( ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + 1 ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) = ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) )
164	163	uneq2d 3461	. . . . . . . . . . . . . 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 ) ) ) )
165	160, 164	eqtrd 2436	. . . . . . . . . . . . 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 ) ) ) )
166	165	fveq2d 5691	. . . . . . . . . . . 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 ) ) ) ) )
167		expp1 11343	. . . . . . . . . . . . . . . . 17 |- ( ( 2 e. CC /\ ( j + 1 ) e. NN0 ) -> ( 2 ^ ( ( j + 1 ) + 1 ) ) = ( ( 2 ^ ( j + 1 ) ) x. 2 ) )
168	5, 76, 167	sylancr 645	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( ( j + 1 ) + 1 ) ) = ( ( 2 ^ ( j + 1 ) ) x. 2 ) )
169	113	times2d 10167	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) x. 2 ) = ( ( 2 ^ ( j + 1 ) ) + ( 2 ^ ( j + 1 ) ) ) )
170	168, 169	eqtrd 2436	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( ( j + 1 ) + 1 ) ) = ( ( 2 ^ ( j + 1 ) ) + ( 2 ^ ( j + 1 ) ) ) )
171	170	oveq1d 6055	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) = ( ( ( 2 ^ ( j + 1 ) ) + ( 2 ^ ( j + 1 ) ) ) - 1 ) )
172	12	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN0 ) -> 1 e. CC )
173	113, 113, 172	addsubd 9388	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN0 ) -> ( ( ( 2 ^ ( j + 1 ) ) + ( 2 ^ ( j + 1 ) ) ) - 1 ) = ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + ( 2 ^ ( j + 1 ) ) ) )
174	171, 173	eqtrd 2436	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) = ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + ( 2 ^ ( j + 1 ) ) ) )
175		uztrn 10458	. . . . . . . . . . . . . . . . 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 ) )
176	156, 135, 175	syl2anc 643	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. ( ZZ>= ` 1 ) )
177	176, 80	syl6eleqr 2495	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. NN )
178	177	nnnn0d 10230	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. NN0 )
179		hashfz1 11585	. . . . . . . . . . . . . 14 |- ( ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. NN0 -> ( # ` ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) = ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) )
180	178, 179	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. NN0 ) -> ( # ` ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) = ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) )
181	134	nnnn0d 10230	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. NN0 )
182		hashfz1 11585	. . . . . . . . . . . . . . 15 |- ( ( ( 2 ^ ( j + 1 ) ) - 1 ) e. NN0 -> ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) = ( ( 2 ^ ( j + 1 ) ) - 1 ) )
183	181, 182	syl 16	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN0 ) -> ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) = ( ( 2 ^ ( j + 1 ) ) - 1 ) )
184	183	oveq1d 6055	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. NN0 ) -> ( ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) + ( 2 ^ ( j + 1 ) ) ) = ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + ( 2 ^ ( j + 1 ) ) ) )
185	174, 180, 184	3eqtr4d 2446	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN0 ) -> ( # ` ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) = ( ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) + ( 2 ^ ( j + 1 ) ) ) )
186	112	ltm1d 9899	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) < ( 2 ^ ( j + 1 ) ) )
187		fzdisj 11034	. . . . . . . . . . . . . 14 |- ( ( ( 2 ^ ( j + 1 ) ) - 1 ) < ( 2 ^ ( j + 1 ) ) -> ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) i^i ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) = (/) )
188	186, 187	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. NN0 ) -> ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) i^i ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) = (/) )
189		hashun 11611	. . . . . . . . . . . . 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 ) ) ) ) )
190	108, 71, 188, 189	syl3anc 1184	. . . . . . . . . . . 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 ) ) ) ) )
191	166, 185, 190	3eqtr3d 2444	. . . . . . . . . . 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 ) ) ) ) )
192	111, 113, 116, 191	addcanad 9227	. . . . . . . . . 10 |- ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) = ( # ` ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) )
193	192	oveq1d 6055	. . . . . . . . 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 ) ) ) ) )
194	58	adantr 452	. . . . . . . . . 10 |- ( ( ph /\ j e. NN0 ) -> A. n e. NN0 ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) )
195		fveq2 5687	. . . . . . . . . . . 12 |- ( n = ( j + 1 ) -> ( G ` n ) = ( G ` ( j + 1 ) ) )
196		oveq2 6048	. . . . . . . . . . . . 13 |- ( n = ( j + 1 ) -> ( 2 ^ n ) = ( 2 ^ ( j + 1 ) ) )
197	196	fveq2d 5691	. . . . . . . . . . . . 13 |- ( n = ( j + 1 ) -> ( F ` ( 2 ^ n ) ) = ( F ` ( 2 ^ ( j + 1 ) ) ) )
198	196, 197	oveq12d 6058	. . . . . . . . . . . 12 |- ( n = ( j + 1 ) -> ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) = ( ( 2 ^ ( j + 1 ) ) x. ( F ` ( 2 ^ ( j + 1 ) ) ) ) )
199	195, 198	eqeq12d 2418	. . . . . . . . . . 11 |- ( n = ( j + 1 ) -> ( ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) <-> ( G ` ( j + 1 ) ) = ( ( 2 ^ ( j + 1 ) ) x. ( F ` ( 2 ^ ( j + 1 ) ) ) ) ) )
200	199	rspcv 3008	. . . . . . . . . 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 ) ) ) ) ) )
201	76, 194, 200	sylc 58	. . . . . . . . 9 |- ( ( ph /\ j e. NN0 ) -> ( G ` ( j + 1 ) ) = ( ( 2 ^ ( j + 1 ) ) x. ( F ` ( 2 ^ ( j + 1 ) ) ) ) )
202	88	recnd 9070	. . . . . . . . . 10 |- ( ( ph /\ j e. NN0 ) -> ( F ` ( 2 ^ ( j + 1 ) ) ) e. CC )
203		fsumconst 12528	. . . . . . . . . 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 ) ) ) ) )
204	71, 202, 203	syl2anc 643	. . . . . . . . 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 ) ) ) ) )
205	193, 201, 204	3eqtr4d 2446	. . . . . . . 8 |- ( ( ph /\ j e. NN0 ) -> ( G ` ( j + 1 ) ) = sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` ( 2 ^ ( j + 1 ) ) ) )
206	107, 205	breqtrrd 4198	. . . . . . 7 |- ( ( ph /\ j e. NN0 ) -> sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` k ) <_ ( G ` ( j + 1 ) ) )
207		elfznn 11036	. . . . . . . . . 10 |- ( k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) -> k e. NN )
208	72, 207, 42	syl2an 464	. . . . . . . . 9 |- ( ( ( ph /\ j e. NN0 ) /\ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) -> ( F ` k ) e. RR )
209	108, 208	fsumrecl 12483	. . . . . . . 8 |- ( ( ph /\ j e. NN0 ) -> sum_ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ( F ` k ) e. RR )
210	71, 83	fsumrecl 12483	. . . . . . . 8 |- ( ( ph /\ j e. NN0 ) -> sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` k ) e. RR )
211		nn0uz 10476	. . . . . . . . . 10 |- NN0 = ( ZZ>= ` 0 )
212	55	a1i 11	. . . . . . . . . 10 |- ( ph -> 0 e. ZZ )
213		simpr 448	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. NN0 ) -> n e. NN0 )
214		nnexpcl 11349	. . . . . . . . . . . . . 14 |- ( ( 2 e. NN /\ n e. NN0 ) -> ( 2 ^ n ) e. NN )
215	74, 213, 214	sylancr 645	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN0 ) -> ( 2 ^ n ) e. NN )
216	215	nnred 9971	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN0 ) -> ( 2 ^ n ) e. RR )
217	43	adantr 452	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN0 ) -> A. k e. NN ( F ` k ) e. RR )
218		fveq2 5687	. . . . . . . . . . . . . . 15 |- ( k = ( 2 ^ n ) -> ( F ` k ) = ( F ` ( 2 ^ n ) ) )
219	218	eleq1d 2470	. . . . . . . . . . . . . 14 |- ( k = ( 2 ^ n ) -> ( ( F ` k ) e. RR <-> ( F ` ( 2 ^ n ) ) e. RR ) )
220	219	rspcv 3008	. . . . . . . . . . . . 13 |- ( ( 2 ^ n ) e. NN -> ( A. k e. NN ( F ` k ) e. RR -> ( F ` ( 2 ^ n ) ) e. RR ) )
221	215, 217, 220	sylc 58	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN0 ) -> ( F ` ( 2 ^ n ) ) e. RR )
222	216, 221	remulcld 9072	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN0 ) -> ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) e. RR )
223	57, 222	eqeltrd 2478	. . . . . . . . . 10 |- ( ( ph /\ n e. NN0 ) -> ( G ` n ) e. RR )
224	211, 212, 223	serfre 11307	. . . . . . . . 9 |- ( ph -> seq 0 ( + , G ) : NN0 --> RR )
225	224	ffvelrnda 5829	. . . . . . . 8 |- ( ( ph /\ j e. NN0 ) -> ( seq 0 ( + , G ) ` j ) e. RR )
226	144, 88	remulcld 9072	. . . . . . . . 9 |- ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) x. ( F ` ( 2 ^ ( j + 1 ) ) ) ) e. RR )
227	201, 226	eqeltrd 2478	. . . . . . . 8 |- ( ( ph /\ j e. NN0 ) -> ( G ` ( j + 1 ) ) e. RR )
228		le2add 9466	. . . . . . . 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 ) ) ) ) )
229	209, 210, 225, 227, 228	syl22anc 1185	. . . . . . 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 ) ) ) ) )
230	206, 229	mpan2d 656	. . . . . 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 ) ) ) ) )
231		eqidd 2405	. . . . . . . . 9 |- ( ( ( ph /\ j e. NN0 ) /\ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) -> ( F ` k ) = ( F ` k ) )
232	42	recnd 9070	. . . . . . . . . 10 |- ( ( ph /\ k e. NN ) -> ( F ` k ) e. CC )
233	72, 207, 232	syl2an 464	. . . . . . . . 9 |- ( ( ( ph /\ j e. NN0 ) /\ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) -> ( F ` k ) e. CC )
234	231, 135, 233	fsumser 12479	. . . . . . . 8 |- ( ( ph /\ j e. NN0 ) -> sum_ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ( F ` k ) = ( seq 1 ( + , F ) ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) )
235	234	eqcomd 2409	. . . . . . 7 |- ( ( ph /\ j e. NN0 ) -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) = sum_ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ( F ` k ) )
236	235	breq1d 4182	. . . . . 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 ) ) )
237		eqidd 2405	. . . . . . . . 9 |- ( ( ( ph /\ j e. NN0 ) /\ k e. ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) -> ( F ` k ) = ( F ` k ) )
238		elfznn 11036	. . . . . . . . . 10 |- ( k e. ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) -> k e. NN )
239	72, 238, 232	syl2an 464	. . . . . . . . 9 |- ( ( ( ph /\ j e. NN0 ) /\ k e. ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) -> ( F ` k ) e. CC )
240	237, 176, 239	fsumser 12479	. . . . . . . 8 |- ( ( ph /\ j e. NN0 ) -> sum_ k e. ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` k ) = ( seq 1 ( + , F ) ` ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) )
241		fzfid 11267	. . . . . . . . 9 |- ( ( ph /\ j e. NN0 ) -> ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) e. Fin )
242	188, 165, 241, 239	fsumsplit 12488	. . . . . . . 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 ) ) )
243	240, 242	eqtr3d 2438	. . . . . . 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 ) ) )
244		simpr 448	. . . . . . . . 9 |- ( ( ph /\ j e. NN0 ) -> j e. NN0 )
245	244, 211	syl6eleq 2494	. . . . . . . 8 |- ( ( ph /\ j e. NN0 ) -> j e. ( ZZ>= ` 0 ) )
246		seqp1 11293	. . . . . . . 8 |- ( j e. ( ZZ>= ` 0 ) -> ( seq 0 ( + , G ) ` ( j + 1 ) ) = ( ( seq 0 ( + , G ) ` j ) + ( G ` ( j + 1 ) ) ) )
247	245, 246	syl 16	. . . . . . 7 |- ( ( ph /\ j e. NN0 ) -> ( seq 0 ( + , G ) ` ( j + 1 ) ) = ( ( seq 0 ( + , G ) ` j ) + ( G ` ( j + 1 ) ) ) )
248	243, 247	breq12d 4185	. . . . . 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 ) ) ) ) )
249	230, 236, 248	3imtr4d 260	. . . . 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 ) ) ) )
250	249	expcom 425	. . . 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 ) ) ) ) )
251	250	a2d 24	. . 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 ) ) ) ) )
252	19, 26, 33, 40, 70, 251	nn0ind 10322	. 2 |- ( N e. NN0 -> ( ph -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( N + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` N ) ) )
253	252	impcom 420	1 |- ( ( ph /\ N e. NN0 ) -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( N + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` N ) )

Syntax hints:   -> wi 4   /\ wa 359   = wceq 1649   e. wcel 1721   A.wral 2666   u. cun 3278   i^i cin 3279   (/)c0 3588   class class class wbr 4172   ` cfv 5413  (class class class)co 6040   Fincfn 7068   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947   + caddc 8949   x. cmul 8951   < clt 9076   <_ cle 9077   - cmin 9247   NNcn 9956   2c2 10005   NN0cn0 10177   ZZcz 10238   ZZ>=cuz 10444   ...cfz 10999   seq cseq 11278   ^cexp 11337   #chash 11573   sum_csu 12434

This theorem is referenced by:  climcnds  12586

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-sup 7404  df-oi 7435  df-card 7782  df-cda 8004  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-n0 10178  df-z 10239  df-uz 10445  df-rp 10569  df-ico 10878  df-fz 11000  df-fzo 11091  df-seq 11279  df-exp 11338  df-hash 11574  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-clim 12237  df-sum 12435