Metamath Proof Explorer

Theorem climcndslem1

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

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

Proof

Step Hyp Ref Expression
1 climcnds.1 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) e. RR )
2 climcnds.2 
 |-  ( ( ph /\ k e. NN ) -> 0 <_ ( F ` k ) )
3 climcnds.3 
 |-  ( ( ph /\ k e. NN ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )
4 climcnds.4 
 |-  ( ( ph /\ n e. NN0 ) -> ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) )
5 oveq1 
 |-  ( x = 0 -> ( x + 1 ) = ( 0 + 1 ) )
6 0p1e1 
 |-  ( 0 + 1 ) = 1
7 5 6 eqtrdi 
 |-  ( x = 0 -> ( x + 1 ) = 1 )
8 7 oveq2d 
 |-  ( x = 0 -> ( 2 ^ ( x + 1 ) ) = ( 2 ^ 1 ) )
9 2cn 
 |-  2 e. CC
10 exp1 
 |-  ( 2 e. CC -> ( 2 ^ 1 ) = 2 )
11 9 10 ax-mp 
 |-  ( 2 ^ 1 ) = 2
12 df-2 
 |-  2 = ( 1 + 1 )
13 11 12 eqtri 
 |-  ( 2 ^ 1 ) = ( 1 + 1 )
14 8 13 eqtrdi 
 |-  ( x = 0 -> ( 2 ^ ( x + 1 ) ) = ( 1 + 1 ) )
15 14 oveq1d 
 |-  ( x = 0 -> ( ( 2 ^ ( x + 1 ) ) - 1 ) = ( ( 1 + 1 ) - 1 ) )
16 ax-1cn 
 |-  1 e. CC
17 16 16 pncan3oi 
 |-  ( ( 1 + 1 ) - 1 ) = 1
18 15 17 eqtrdi 
 |-  ( x = 0 -> ( ( 2 ^ ( x + 1 ) ) - 1 ) = 1 )
19 18 fveq2d 
 |-  ( x = 0 -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) = ( seq 1 ( + , F ) ` 1 ) )
20 fveq2 
 |-  ( x = 0 -> ( seq 0 ( + , G ) ` x ) = ( seq 0 ( + , G ) ` 0 ) )
21 19 20 breq12d 
 |-  ( x = 0 -> ( ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` x ) <-> ( seq 1 ( + , F ) ` 1 ) <_ ( seq 0 ( + , G ) ` 0 ) ) )
22 21 imbi2d 
 |-  ( x = 0 -> ( ( ph -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` x ) ) <-> ( ph -> ( seq 1 ( + , F ) ` 1 ) <_ ( seq 0 ( + , G ) ` 0 ) ) ) )
23 oveq1 
 |-  ( x = j -> ( x + 1 ) = ( j + 1 ) )
24 23 oveq2d 
 |-  ( x = j -> ( 2 ^ ( x + 1 ) ) = ( 2 ^ ( j + 1 ) ) )
25 24 fvoveq1d 
 |-  ( x = j -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) = ( seq 1 ( + , F ) ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) )
26 fveq2 
 |-  ( x = j -> ( seq 0 ( + , G ) ` x ) = ( seq 0 ( + , G ) ` j ) )
27 25 26 breq12d 
 |-  ( x = j -> ( ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` x ) <-> ( seq 1 ( + , F ) ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` j ) ) )
28 27 imbi2d 
 |-  ( 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 ) ) ) )
29 oveq1 
 |-  ( x = ( j + 1 ) -> ( x + 1 ) = ( ( j + 1 ) + 1 ) )
30 29 oveq2d 
 |-  ( x = ( j + 1 ) -> ( 2 ^ ( x + 1 ) ) = ( 2 ^ ( ( j + 1 ) + 1 ) ) )
31 30 fvoveq1d 
 |-  ( x = ( j + 1 ) -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) = ( seq 1 ( + , F ) ` ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) )
32 fveq2 
 |-  ( x = ( j + 1 ) -> ( seq 0 ( + , G ) ` x ) = ( seq 0 ( + , G ) ` ( j + 1 ) ) )
33 31 32 breq12d 
 |-  ( 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 ) ) ) )
34 33 imbi2d 
 |-  ( 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 ) ) ) ) )
35 oveq1 
 |-  ( x = N -> ( x + 1 ) = ( N + 1 ) )
36 35 oveq2d 
 |-  ( x = N -> ( 2 ^ ( x + 1 ) ) = ( 2 ^ ( N + 1 ) ) )
37 36 fvoveq1d 
 |-  ( x = N -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( x + 1 ) ) - 1 ) ) = ( seq 1 ( + , F ) ` ( ( 2 ^ ( N + 1 ) ) - 1 ) ) )
38 fveq2 
 |-  ( x = N -> ( seq 0 ( + , G ) ` x ) = ( seq 0 ( + , G ) ` N ) )
39 37 38 breq12d 
 |-  ( 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 
 |-  ( 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 fveq2 
 |-  ( k = 1 -> ( F ` k ) = ( F ` 1 ) )
42 41 eleq1d 
 |-  ( k = 1 -> ( ( F ` k ) e. RR <-> ( F ` 1 ) e. RR ) )
43 1 ralrimiva 
 |-  ( ph -> A. k e. NN ( F ` k ) e. RR )
44 1nn 
 |-  1 e. NN
45 44 a1i 
 |-  ( ph -> 1 e. NN )
46 42 43 45 rspcdva 
 |-  ( ph -> ( F ` 1 ) e. RR )
47 46 leidd 
 |-  ( ph -> ( F ` 1 ) <_ ( F ` 1 ) )
48 46 recnd 
 |-  ( ph -> ( F ` 1 ) e. CC )
49 48 mulid2d 
 |-  ( ph -> ( 1 x. ( F ` 1 ) ) = ( F ` 1 ) )
50 47 49 breqtrrd 
 |-  ( ph -> ( F ` 1 ) <_ ( 1 x. ( F ` 1 ) ) )
51 1z 
 |-  1 e. ZZ
52 eqidd 
 |-  ( ph -> ( F ` 1 ) = ( F ` 1 ) )
53 51 52 seq1i 
 |-  ( ph -> ( seq 1 ( + , F ) ` 1 ) = ( F ` 1 ) )
54 0z 
 |-  0 e. ZZ
55 fveq2 
 |-  ( n = 0 -> ( G ` n ) = ( G ` 0 ) )
56 oveq2 
 |-  ( n = 0 -> ( 2 ^ n ) = ( 2 ^ 0 ) )
57 exp0 
 |-  ( 2 e. CC -> ( 2 ^ 0 ) = 1 )
58 9 57 ax-mp 
 |-  ( 2 ^ 0 ) = 1
59 56 58 eqtrdi 
 |-  ( n = 0 -> ( 2 ^ n ) = 1 )
60 59 fveq2d 
 |-  ( n = 0 -> ( F ` ( 2 ^ n ) ) = ( F ` 1 ) )
61 59 60 oveq12d 
 |-  ( n = 0 -> ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) = ( 1 x. ( F ` 1 ) ) )
62 55 61 eqeq12d 
 |-  ( n = 0 -> ( ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) <-> ( G ` 0 ) = ( 1 x. ( F ` 1 ) ) ) )
63 4 ralrimiva 
 |-  ( ph -> A. n e. NN0 ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) )
64 0nn0 
 |-  0 e. NN0
65 64 a1i 
 |-  ( ph -> 0 e. NN0 )
66 62 63 65 rspcdva 
 |-  ( ph -> ( G ` 0 ) = ( 1 x. ( F ` 1 ) ) )
67 54 66 seq1i 
 |-  ( ph -> ( seq 0 ( + , G ) ` 0 ) = ( 1 x. ( F ` 1 ) ) )
68 50 53 67 3brtr4d 
 |-  ( ph -> ( seq 1 ( + , F ) ` 1 ) <_ ( seq 0 ( + , G ) ` 0 ) )
69 fzfid 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) e. Fin )
70 simpl 
 |-  ( ( ph /\ j e. NN0 ) -> ph )
71 2nn 
 |-  2 e. NN
72 peano2nn0 
 |-  ( j e. NN0 -> ( j + 1 ) e. NN0 )
73 72 adantl 
 |-  ( ( ph /\ j e. NN0 ) -> ( j + 1 ) e. NN0 )
74 nnexpcl 
 |-  ( ( 2 e. NN /\ ( j + 1 ) e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. NN )
75 71 73 74 sylancr 
 |-  ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. NN )
76 elfzuz 
 |-  ( k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) -> k e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) )
77 eluznn 
 |-  ( ( ( 2 ^ ( j + 1 ) ) e. NN /\ k e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) -> k e. NN )
78 75 76 77 syl2an 
 |-  ( ( ( ph /\ j e. NN0 ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) -> k e. NN )
79 70 78 1 syl2an2r 
 |-  ( ( ( ph /\ j e. NN0 ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) -> ( F ` k ) e. RR )
80 fveq2 
 |-  ( k = ( 2 ^ ( j + 1 ) ) -> ( F ` k ) = ( F ` ( 2 ^ ( j + 1 ) ) ) )
81 80 eleq1d 
 |-  ( k = ( 2 ^ ( j + 1 ) ) -> ( ( F ` k ) e. RR <-> ( F ` ( 2 ^ ( j + 1 ) ) ) e. RR ) )
82 43 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> A. k e. NN ( F ` k ) e. RR )
83 81 82 75 rspcdva 
 |-  ( ( ph /\ j e. NN0 ) -> ( F ` ( 2 ^ ( j + 1 ) ) ) e. RR )
84 83 adantr 
 |-  ( ( ( ph /\ j e. NN0 ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) -> ( F ` ( 2 ^ ( j + 1 ) ) ) e. RR )
85 simpr 
 |-  ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) -> n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) )
86 simplll 
 |-  ( ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... n ) ) -> ph )
87 75 adantr 
 |-  ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) -> ( 2 ^ ( j + 1 ) ) e. NN )
88 elfzuz 
 |-  ( k e. ( ( 2 ^ ( j + 1 ) ) ... n ) -> k e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) )
89 87 88 77 syl2an 
 |-  ( ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... n ) ) -> k e. NN )
90 86 89 1 syl2anc 
 |-  ( ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... n ) ) -> ( F ` k ) e. RR )
91 simplll 
 |-  ( ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( n - 1 ) ) ) -> ph )
92 elfzuz 
 |-  ( k e. ( ( 2 ^ ( j + 1 ) ) ... ( n - 1 ) ) -> k e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) )
93 87 92 77 syl2an 
 |-  ( ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( n - 1 ) ) ) -> k e. NN )
94 91 93 3 syl2anc 
 |-  ( ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( n - 1 ) ) ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )
95 85 90 94 monoord2 
 |-  ( ( ( ph /\ j e. NN0 ) /\ n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ) -> ( F ` n ) <_ ( F ` ( 2 ^ ( j + 1 ) ) ) )
96 95 ralrimiva 
 |-  ( ( ph /\ j e. NN0 ) -> A. n e. ( ZZ>= ` ( 2 ^ ( j + 1 ) ) ) ( F ` n ) <_ ( F ` ( 2 ^ ( j + 1 ) ) ) )
97 fveq2 
 |-  ( n = k -> ( F ` n ) = ( F ` k ) )
98 97 breq1d 
 |-  ( n = k -> ( ( F ` n ) <_ ( F ` ( 2 ^ ( j + 1 ) ) ) <-> ( F ` k ) <_ ( F ` ( 2 ^ ( j + 1 ) ) ) ) )
99 98 rspccva 
 |-  ( ( 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 ) ) ) )
100 96 76 99 syl2an 
 |-  ( ( ( ph /\ j e. NN0 ) /\ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) -> ( F ` k ) <_ ( F ` ( 2 ^ ( j + 1 ) ) ) )
101 69 79 84 100 fsumle 
 |-  ( ( 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 ) ) ) )
102 fzfid 
 |-  ( ( ph /\ j e. NN0 ) -> ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) e. Fin )
103 hashcl 
 |-  ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) e. Fin -> ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) e. NN0 )
104 102 103 syl 
 |-  ( ( ph /\ j e. NN0 ) -> ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) e. NN0 )
105 104 nn0cnd 
 |-  ( ( ph /\ j e. NN0 ) -> ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) e. CC )
106 75 nnred 
 |-  ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. RR )
107 106 recnd 
 |-  ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. CC )
108 hashcl 
 |-  ( ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) e. Fin -> ( # ` ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) e. NN0 )
109 69 108 syl 
 |-  ( ( ph /\ j e. NN0 ) -> ( # ` ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) e. NN0 )
110 109 nn0cnd 
 |-  ( ( ph /\ j e. NN0 ) -> ( # ` ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) e. CC )
111 2z 
 |-  2 e. ZZ
112 zexpcl 
 |-  ( ( 2 e. ZZ /\ ( j + 1 ) e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. ZZ )
113 111 73 112 sylancr 
 |-  ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. ZZ )
114 2re 
 |-  2 e. RR
115 1le2 
 |-  1 <_ 2
116 nn0p1nn 
 |-  ( j e. NN0 -> ( j + 1 ) e. NN )
117 116 adantl 
 |-  ( ( ph /\ j e. NN0 ) -> ( j + 1 ) e. NN )
118 nnuz 
 |-  NN = ( ZZ>= ` 1 )
119 117 118 eleqtrdi 
 |-  ( ( ph /\ j e. NN0 ) -> ( j + 1 ) e. ( ZZ>= ` 1 ) )
120 leexp2a 
 |-  ( ( 2 e. RR /\ 1 <_ 2 /\ ( j + 1 ) e. ( ZZ>= ` 1 ) ) -> ( 2 ^ 1 ) <_ ( 2 ^ ( j + 1 ) ) )
121 114 115 119 120 mp3an12i 
 |-  ( ( ph /\ j e. NN0 ) -> ( 2 ^ 1 ) <_ ( 2 ^ ( j + 1 ) ) )
122 11 121 eqbrtrrid 
 |-  ( ( ph /\ j e. NN0 ) -> 2 <_ ( 2 ^ ( j + 1 ) ) )
123 111 eluz1i 
 |-  ( ( 2 ^ ( j + 1 ) ) e. ( ZZ>= ` 2 ) <-> ( ( 2 ^ ( j + 1 ) ) e. ZZ /\ 2 <_ ( 2 ^ ( j + 1 ) ) ) )
124 113 122 123 sylanbrc 
 |-  ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. ( ZZ>= ` 2 ) )
125 uz2m1nn 
 |-  ( ( 2 ^ ( j + 1 ) ) e. ( ZZ>= ` 2 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. NN )
126 124 125 syl 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. NN )
127 126 118 eleqtrdi 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. ( ZZ>= ` 1 ) )
128 peano2zm 
 |-  ( ( 2 ^ ( j + 1 ) ) e. ZZ -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. ZZ )
129 113 128 syl 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. ZZ )
130 peano2nn0 
 |-  ( ( j + 1 ) e. NN0 -> ( ( j + 1 ) + 1 ) e. NN0 )
131 73 130 syl 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( j + 1 ) + 1 ) e. NN0 )
132 zexpcl 
 |-  ( ( 2 e. ZZ /\ ( ( j + 1 ) + 1 ) e. NN0 ) -> ( 2 ^ ( ( j + 1 ) + 1 ) ) e. ZZ )
133 111 131 132 sylancr 
 |-  ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( ( j + 1 ) + 1 ) ) e. ZZ )
134 peano2zm 
 |-  ( ( 2 ^ ( ( j + 1 ) + 1 ) ) e. ZZ -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. ZZ )
135 133 134 syl 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. ZZ )
136 113 zred 
 |-  ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. RR )
137 133 zred 
 |-  ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( ( j + 1 ) + 1 ) ) e. RR )
138 1red 
 |-  ( ( ph /\ j e. NN0 ) -> 1 e. RR )
139 73 nn0zd 
 |-  ( ( ph /\ j e. NN0 ) -> ( j + 1 ) e. ZZ )
140 uzid 
 |-  ( ( j + 1 ) e. ZZ -> ( j + 1 ) e. ( ZZ>= ` ( j + 1 ) ) )
141 peano2uz 
 |-  ( ( j + 1 ) e. ( ZZ>= ` ( j + 1 ) ) -> ( ( j + 1 ) + 1 ) e. ( ZZ>= ` ( j + 1 ) ) )
142 leexp2a 
 |-  ( ( 2 e. RR /\ 1 <_ 2 /\ ( ( j + 1 ) + 1 ) e. ( ZZ>= ` ( j + 1 ) ) ) -> ( 2 ^ ( j + 1 ) ) <_ ( 2 ^ ( ( j + 1 ) + 1 ) ) )
143 114 115 142 mp3an12 
 |-  ( ( ( j + 1 ) + 1 ) e. ( ZZ>= ` ( j + 1 ) ) -> ( 2 ^ ( j + 1 ) ) <_ ( 2 ^ ( ( j + 1 ) + 1 ) ) )
144 139 140 141 143 4syl 
 |-  ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) <_ ( 2 ^ ( ( j + 1 ) + 1 ) ) )
145 136 137 138 144 lesub1dd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) <_ ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) )
146 eluz2 
 |-  ( ( ( 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 ) ) )
147 129 135 145 146 syl3anbrc 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. ( ZZ>= ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) )
148 elfzuzb 
 |-  ( ( ( 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 ) ) ) )
149 127 147 148 sylanbrc 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) )
150 fzsplit 
 |-  ( ( ( 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 ) ) ) )
151 149 150 syl 
 |-  ( ( 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 ) ) ) )
152 npcan 
 |-  ( ( ( 2 ^ ( j + 1 ) ) e. CC /\ 1 e. CC ) -> ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + 1 ) = ( 2 ^ ( j + 1 ) ) )
153 107 16 152 sylancl 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + 1 ) = ( 2 ^ ( j + 1 ) ) )
154 153 oveq1d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + 1 ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) = ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) )
155 154 uneq2d 
 |-  ( ( 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 ) ) ) )
156 151 155 eqtrd 
 |-  ( ( ph /\ j e. NN0 ) -> ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) = ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) u. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) )
157 156 fveq2d 
 |-  ( ( ph /\ j e. NN0 ) -> ( # ` ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) = ( # ` ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) u. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) ) )
158 expp1 
 |-  ( ( 2 e. CC /\ ( j + 1 ) e. NN0 ) -> ( 2 ^ ( ( j + 1 ) + 1 ) ) = ( ( 2 ^ ( j + 1 ) ) x. 2 ) )
159 9 73 158 sylancr 
 |-  ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( ( j + 1 ) + 1 ) ) = ( ( 2 ^ ( j + 1 ) ) x. 2 ) )
160 107 times2d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) x. 2 ) = ( ( 2 ^ ( j + 1 ) ) + ( 2 ^ ( j + 1 ) ) ) )
161 159 160 eqtrd 
 |-  ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( ( j + 1 ) + 1 ) ) = ( ( 2 ^ ( j + 1 ) ) + ( 2 ^ ( j + 1 ) ) ) )
162 161 oveq1d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) = ( ( ( 2 ^ ( j + 1 ) ) + ( 2 ^ ( j + 1 ) ) ) - 1 ) )
163 1cnd 
 |-  ( ( ph /\ j e. NN0 ) -> 1 e. CC )
164 107 107 163 addsubd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ( 2 ^ ( j + 1 ) ) + ( 2 ^ ( j + 1 ) ) ) - 1 ) = ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + ( 2 ^ ( j + 1 ) ) ) )
165 162 164 eqtrd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) = ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + ( 2 ^ ( j + 1 ) ) ) )
166 uztrn 
 |-  ( ( ( ( 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 ) )
167 147 127 166 syl2anc 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. ( ZZ>= ` 1 ) )
168 167 118 eleqtrrdi 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. NN )
169 168 nnnn0d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. NN0 )
170 hashfz1 
 |-  ( ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) e. NN0 -> ( # ` ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) = ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) )
171 169 170 syl 
 |-  ( ( ph /\ j e. NN0 ) -> ( # ` ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) = ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) )
172 126 nnnn0d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. NN0 )
173 hashfz1 
 |-  ( ( ( 2 ^ ( j + 1 ) ) - 1 ) e. NN0 -> ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) = ( ( 2 ^ ( j + 1 ) ) - 1 ) )
174 172 173 syl 
 |-  ( ( ph /\ j e. NN0 ) -> ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) = ( ( 2 ^ ( j + 1 ) ) - 1 ) )
175 174 oveq1d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) + ( 2 ^ ( j + 1 ) ) ) = ( ( ( 2 ^ ( j + 1 ) ) - 1 ) + ( 2 ^ ( j + 1 ) ) ) )
176 165 171 175 3eqtr4d 
 |-  ( ( ph /\ j e. NN0 ) -> ( # ` ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) = ( ( # ` ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) + ( 2 ^ ( j + 1 ) ) ) )
177 106 ltm1d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) < ( 2 ^ ( j + 1 ) ) )
178 fzdisj 
 |-  ( ( ( 2 ^ ( j + 1 ) ) - 1 ) < ( 2 ^ ( j + 1 ) ) -> ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) i^i ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) = (/) )
179 177 178 syl 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) i^i ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) = (/) )
180 hashun 
 |-  ( ( ( 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 ) ) ) ) )
181 102 69 179 180 syl3anc 
 |-  ( ( 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 ) ) ) ) )
182 157 176 181 3eqtr3d 
 |-  ( ( 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 ) ) ) ) )
183 105 107 110 182 addcanad 
 |-  ( ( ph /\ j e. NN0 ) -> ( 2 ^ ( j + 1 ) ) = ( # ` ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) )
184 183 oveq1d 
 |-  ( ( 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 ) ) ) ) )
185 fveq2 
 |-  ( n = ( j + 1 ) -> ( G ` n ) = ( G ` ( j + 1 ) ) )
186 oveq2 
 |-  ( n = ( j + 1 ) -> ( 2 ^ n ) = ( 2 ^ ( j + 1 ) ) )
187 186 fveq2d 
 |-  ( n = ( j + 1 ) -> ( F ` ( 2 ^ n ) ) = ( F ` ( 2 ^ ( j + 1 ) ) ) )
188 186 187 oveq12d 
 |-  ( n = ( j + 1 ) -> ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) = ( ( 2 ^ ( j + 1 ) ) x. ( F ` ( 2 ^ ( j + 1 ) ) ) ) )
189 185 188 eqeq12d 
 |-  ( n = ( j + 1 ) -> ( ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) <-> ( G ` ( j + 1 ) ) = ( ( 2 ^ ( j + 1 ) ) x. ( F ` ( 2 ^ ( j + 1 ) ) ) ) ) )
190 63 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> A. n e. NN0 ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) )
191 189 190 73 rspcdva 
 |-  ( ( ph /\ j e. NN0 ) -> ( G ` ( j + 1 ) ) = ( ( 2 ^ ( j + 1 ) ) x. ( F ` ( 2 ^ ( j + 1 ) ) ) ) )
192 83 recnd 
 |-  ( ( ph /\ j e. NN0 ) -> ( F ` ( 2 ^ ( j + 1 ) ) ) e. CC )
193 fsumconst 
 |-  ( ( ( ( 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 ) ) ) ) )
194 69 192 193 syl2anc 
 |-  ( ( 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 ) ) ) ) )
195 184 191 194 3eqtr4d 
 |-  ( ( ph /\ j e. NN0 ) -> ( G ` ( j + 1 ) ) = sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` ( 2 ^ ( j + 1 ) ) ) )
196 101 195 breqtrrd 
 |-  ( ( ph /\ j e. NN0 ) -> sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` k ) <_ ( G ` ( j + 1 ) ) )
197 elfznn 
 |-  ( k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) -> k e. NN )
198 70 197 1 syl2an 
 |-  ( ( ( ph /\ j e. NN0 ) /\ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) -> ( F ` k ) e. RR )
199 102 198 fsumrecl 
 |-  ( ( ph /\ j e. NN0 ) -> sum_ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ( F ` k ) e. RR )
200 69 79 fsumrecl 
 |-  ( ( ph /\ j e. NN0 ) -> sum_ k e. ( ( 2 ^ ( j + 1 ) ) ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` k ) e. RR )
201 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
202 0zd 
 |-  ( ph -> 0 e. ZZ )
203 simpr 
 |-  ( ( ph /\ n e. NN0 ) -> n e. NN0 )
204 nnexpcl 
 |-  ( ( 2 e. NN /\ n e. NN0 ) -> ( 2 ^ n ) e. NN )
205 71 203 204 sylancr 
 |-  ( ( ph /\ n e. NN0 ) -> ( 2 ^ n ) e. NN )
206 205 nnred 
 |-  ( ( ph /\ n e. NN0 ) -> ( 2 ^ n ) e. RR )
207 fveq2 
 |-  ( k = ( 2 ^ n ) -> ( F ` k ) = ( F ` ( 2 ^ n ) ) )
208 207 eleq1d 
 |-  ( k = ( 2 ^ n ) -> ( ( F ` k ) e. RR <-> ( F ` ( 2 ^ n ) ) e. RR ) )
209 43 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> A. k e. NN ( F ` k ) e. RR )
210 208 209 205 rspcdva 
 |-  ( ( ph /\ n e. NN0 ) -> ( F ` ( 2 ^ n ) ) e. RR )
211 206 210 remulcld 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) e. RR )
212 4 211 eqeltrd 
 |-  ( ( ph /\ n e. NN0 ) -> ( G ` n ) e. RR )
213 201 202 212 serfre 
 |-  ( ph -> seq 0 ( + , G ) : NN0 --> RR )
214 213 ffvelrnda 
 |-  ( ( ph /\ j e. NN0 ) -> ( seq 0 ( + , G ) ` j ) e. RR )
215 136 83 remulcld 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 2 ^ ( j + 1 ) ) x. ( F ` ( 2 ^ ( j + 1 ) ) ) ) e. RR )
216 191 215 eqeltrd 
 |-  ( ( ph /\ j e. NN0 ) -> ( G ` ( j + 1 ) ) e. RR )
217 le2add 
 |-  ( ( ( 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 ) ) ) ) )
218 199 200 214 216 217 syl22anc 
 |-  ( ( 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 ) ) ) ) )
219 196 218 mpan2d 
 |-  ( ( 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 ) ) ) ) )
220 eqidd 
 |-  ( ( ( ph /\ j e. NN0 ) /\ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) -> ( F ` k ) = ( F ` k ) )
221 1 recnd 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) e. CC )
222 70 197 221 syl2an 
 |-  ( ( ( ph /\ j e. NN0 ) /\ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) -> ( F ` k ) e. CC )
223 220 127 222 fsumser 
 |-  ( ( ph /\ j e. NN0 ) -> sum_ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ( F ` k ) = ( seq 1 ( + , F ) ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) )
224 223 eqcomd 
 |-  ( ( ph /\ j e. NN0 ) -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) = sum_ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ( F ` k ) )
225 224 breq1d 
 |-  ( ( 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 ) ) )
226 eqidd 
 |-  ( ( ( ph /\ j e. NN0 ) /\ k e. ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) -> ( F ` k ) = ( F ` k ) )
227 elfznn 
 |-  ( k e. ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) -> k e. NN )
228 70 227 221 syl2an 
 |-  ( ( ( ph /\ j e. NN0 ) /\ k e. ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ) -> ( F ` k ) e. CC )
229 226 167 228 fsumser 
 |-  ( ( ph /\ j e. NN0 ) -> sum_ k e. ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) ( F ` k ) = ( seq 1 ( + , F ) ` ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) )
230 fzfid 
 |-  ( ( ph /\ j e. NN0 ) -> ( 1 ... ( ( 2 ^ ( ( j + 1 ) + 1 ) ) - 1 ) ) e. Fin )
231 179 156 230 228 fsumsplit 
 |-  ( ( 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 ) ) )
232 229 231 eqtr3d 
 |-  ( ( 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 ) ) )
233 simpr 
 |-  ( ( ph /\ j e. NN0 ) -> j e. NN0 )
234 233 201 eleqtrdi 
 |-  ( ( ph /\ j e. NN0 ) -> j e. ( ZZ>= ` 0 ) )
235 seqp1 
 |-  ( j e. ( ZZ>= ` 0 ) -> ( seq 0 ( + , G ) ` ( j + 1 ) ) = ( ( seq 0 ( + , G ) ` j ) + ( G ` ( j + 1 ) ) ) )
236 234 235 syl 
 |-  ( ( ph /\ j e. NN0 ) -> ( seq 0 ( + , G ) ` ( j + 1 ) ) = ( ( seq 0 ( + , G ) ` j ) + ( G ` ( j + 1 ) ) ) )
237 232 236 breq12d 
 |-  ( ( 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 ) ) ) ) )
238 219 225 237 3imtr4d 
 |-  ( ( 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 ) ) ) )
239 238 expcom 
 |-  ( 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 ) ) ) ) )
240 239 a2d 
 |-  ( 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 ) ) ) ) )
241 22 28 34 40 68 240 nn0ind 
 |-  ( N e. NN0 -> ( ph -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( N + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` N ) ) )
242 241 impcom 
 |-  ( ( ph /\ N e. NN0 ) -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( N + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` N ) )