Metamath Proof Explorer

Theorem climcndslem2

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

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