This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem climcnds

Description: The Cauchy condensation test. If a ( k ) is a decreasing sequence of nonnegative terms, then sum_ k e. NN a ( k ) converges iff sum_ n e. NN0 2 ^ n x. a ( 2 ^ n ) converges. (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 climcnds 
|- ( ph -> ( seq 1 ( + , F ) e. dom ~~> <-> seq 0 ( + , G ) e. dom ~~> ) )

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 nnuz 
 |-  NN = ( ZZ>= ` 1 )
6 1zzd 
 |-  ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) -> 1 e. ZZ )
7 1zzd 
 |-  ( ph -> 1 e. ZZ )
8 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
9 2nn 
 |-  2 e. NN
10 simpr 
 |-  ( ( ph /\ n e. NN0 ) -> n e. NN0 )
11 nnexpcl 
 |-  ( ( 2 e. NN /\ n e. NN0 ) -> ( 2 ^ n ) e. NN )
12 9 10 11 sylancr 
 |-  ( ( ph /\ n e. NN0 ) -> ( 2 ^ n ) e. NN )
13 12 nnred 
 |-  ( ( ph /\ n e. NN0 ) -> ( 2 ^ n ) e. RR )
14 fveq2 
 |-  ( k = ( 2 ^ n ) -> ( F ` k ) = ( F ` ( 2 ^ n ) ) )
15 14 eleq1d 
 |-  ( k = ( 2 ^ n ) -> ( ( F ` k ) e. RR <-> ( F ` ( 2 ^ n ) ) e. RR ) )
16 1 ralrimiva 
 |-  ( ph -> A. k e. NN ( F ` k ) e. RR )
17 16 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> A. k e. NN ( F ` k ) e. RR )
18 15 17 12 rspcdva 
 |-  ( ( ph /\ n e. NN0 ) -> ( F ` ( 2 ^ n ) ) e. RR )
19 13 18 remulcld 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) e. RR )
20 4 19 eqeltrd 
 |-  ( ( ph /\ n e. NN0 ) -> ( G ` n ) e. RR )
21 8 20 sylan2 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) e. RR )
22 5 7 21 serfre 
 |-  ( ph -> seq 1 ( + , G ) : NN --> RR )
23 22 adantr 
 |-  ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) -> seq 1 ( + , G ) : NN --> RR )
24 simpr 
 |-  ( ( ph /\ j e. NN ) -> j e. NN )
25 24 5 eleqtrdi 
 |-  ( ( ph /\ j e. NN ) -> j e. ( ZZ>= ` 1 ) )
26 nnz 
 |-  ( j e. NN -> j e. ZZ )
27 26 adantl 
 |-  ( ( ph /\ j e. NN ) -> j e. ZZ )
28 uzid 
 |-  ( j e. ZZ -> j e. ( ZZ>= ` j ) )
29 peano2uz 
 |-  ( j e. ( ZZ>= ` j ) -> ( j + 1 ) e. ( ZZ>= ` j ) )
30 27 28 29 3syl 
 |-  ( ( ph /\ j e. NN ) -> ( j + 1 ) e. ( ZZ>= ` j ) )
31 simpl 
 |-  ( ( ph /\ j e. NN ) -> ph )
32 elfznn 
 |-  ( n e. ( 1 ... ( j + 1 ) ) -> n e. NN )
33 31 32 21 syl2an 
 |-  ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... ( j + 1 ) ) ) -> ( G ` n ) e. RR )
34 simpll 
 |-  ( ( ( ph /\ j e. NN ) /\ n e. ( ( j + 1 ) ... ( j + 1 ) ) ) -> ph )
35 elfz1eq 
 |-  ( n e. ( ( j + 1 ) ... ( j + 1 ) ) -> n = ( j + 1 ) )
36 35 adantl 
 |-  ( ( ( ph /\ j e. NN ) /\ n e. ( ( j + 1 ) ... ( j + 1 ) ) ) -> n = ( j + 1 ) )
37 nnnn0 
 |-  ( j e. NN -> j e. NN0 )
38 peano2nn0 
 |-  ( j e. NN0 -> ( j + 1 ) e. NN0 )
39 37 38 syl 
 |-  ( j e. NN -> ( j + 1 ) e. NN0 )
40 39 ad2antlr 
 |-  ( ( ( ph /\ j e. NN ) /\ n e. ( ( j + 1 ) ... ( j + 1 ) ) ) -> ( j + 1 ) e. NN0 )
41 36 40 eqeltrd 
 |-  ( ( ( ph /\ j e. NN ) /\ n e. ( ( j + 1 ) ... ( j + 1 ) ) ) -> n e. NN0 )
42 12 nnnn0d 
 |-  ( ( ph /\ n e. NN0 ) -> ( 2 ^ n ) e. NN0 )
43 42 nn0ge0d 
 |-  ( ( ph /\ n e. NN0 ) -> 0 <_ ( 2 ^ n ) )
44 14 breq2d 
 |-  ( k = ( 2 ^ n ) -> ( 0 <_ ( F ` k ) <-> 0 <_ ( F ` ( 2 ^ n ) ) ) )
45 2 ralrimiva 
 |-  ( ph -> A. k e. NN 0 <_ ( F ` k ) )
46 45 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> A. k e. NN 0 <_ ( F ` k ) )
47 44 46 12 rspcdva 
 |-  ( ( ph /\ n e. NN0 ) -> 0 <_ ( F ` ( 2 ^ n ) ) )
48 13 18 43 47 mulge0d 
 |-  ( ( ph /\ n e. NN0 ) -> 0 <_ ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) )
49 48 4 breqtrrd 
 |-  ( ( ph /\ n e. NN0 ) -> 0 <_ ( G ` n ) )
50 34 41 49 syl2anc 
 |-  ( ( ( ph /\ j e. NN ) /\ n e. ( ( j + 1 ) ... ( j + 1 ) ) ) -> 0 <_ ( G ` n ) )
51 25 30 33 50 sermono 
 |-  ( ( ph /\ j e. NN ) -> ( seq 1 ( + , G ) ` j ) <_ ( seq 1 ( + , G ) ` ( j + 1 ) ) )
52 51 adantlr 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> ( seq 1 ( + , G ) ` j ) <_ ( seq 1 ( + , G ) ` ( j + 1 ) ) )
53 2re 
 |-  2 e. RR
54 eqidd 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ k e. NN ) -> ( F ` k ) = ( F ` k ) )
55 1 adantlr 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ k e. NN ) -> ( F ` k ) e. RR )
56 simpr 
 |-  ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) -> seq 1 ( + , F ) e. dom ~~> )
57 5 6 54 55 56 isumrecl 
 |-  ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) -> sum_ k e. NN ( F ` k ) e. RR )
58 remulcl 
 |-  ( ( 2 e. RR /\ sum_ k e. NN ( F ` k ) e. RR ) -> ( 2 x. sum_ k e. NN ( F ` k ) ) e. RR )
59 53 57 58 sylancr 
 |-  ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) -> ( 2 x. sum_ k e. NN ( F ` k ) ) e. RR )
60 23 ffvelcdmda 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> ( seq 1 ( + , G ) ` j ) e. RR )
61 5 7 1 serfre 
 |-  ( ph -> seq 1 ( + , F ) : NN --> RR )
62 61 ad2antrr 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> seq 1 ( + , F ) : NN --> RR )
63 37 adantl 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> j e. NN0 )
64 nnexpcl 
 |-  ( ( 2 e. NN /\ j e. NN0 ) -> ( 2 ^ j ) e. NN )
65 9 63 64 sylancr 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> ( 2 ^ j ) e. NN )
66 62 65 ffvelcdmd 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> ( seq 1 ( + , F ) ` ( 2 ^ j ) ) e. RR )
67 remulcl 
 |-  ( ( 2 e. RR /\ ( seq 1 ( + , F ) ` ( 2 ^ j ) ) e. RR ) -> ( 2 x. ( seq 1 ( + , F ) ` ( 2 ^ j ) ) ) e. RR )
68 53 66 67 sylancr 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> ( 2 x. ( seq 1 ( + , F ) ` ( 2 ^ j ) ) ) e. RR )
69 59 adantr 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> ( 2 x. sum_ k e. NN ( F ` k ) ) e. RR )
70 1 2 3 4 climcndslem2 
 |-  ( ( ph /\ j e. NN ) -> ( seq 1 ( + , G ) ` j ) <_ ( 2 x. ( seq 1 ( + , F ) ` ( 2 ^ j ) ) ) )
71 70 adantlr 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> ( seq 1 ( + , G ) ` j ) <_ ( 2 x. ( seq 1 ( + , F ) ` ( 2 ^ j ) ) ) )
72 eqidd 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) /\ k e. ( 1 ... ( 2 ^ j ) ) ) -> ( F ` k ) = ( F ` k ) )
73 65 5 eleqtrdi 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> ( 2 ^ j ) e. ( ZZ>= ` 1 ) )
74 simpll 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> ph )
75 elfznn 
 |-  ( k e. ( 1 ... ( 2 ^ j ) ) -> k e. NN )
76 1 recnd 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) e. CC )
77 74 75 76 syl2an 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) /\ k e. ( 1 ... ( 2 ^ j ) ) ) -> ( F ` k ) e. CC )
78 72 73 77 fsumser 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> sum_ k e. ( 1 ... ( 2 ^ j ) ) ( F ` k ) = ( seq 1 ( + , F ) ` ( 2 ^ j ) ) )
79 1zzd 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> 1 e. ZZ )
80 fzfid 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> ( 1 ... ( 2 ^ j ) ) e. Fin )
81 75 ssriv 
 |-  ( 1 ... ( 2 ^ j ) ) C_ NN
82 81 a1i 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> ( 1 ... ( 2 ^ j ) ) C_ NN )
83 eqidd 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) /\ k e. NN ) -> ( F ` k ) = ( F ` k ) )
84 1 ad4ant14 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) /\ k e. NN ) -> ( F ` k ) e. RR )
85 2 ad4ant14 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) /\ k e. NN ) -> 0 <_ ( F ` k ) )
86 simplr 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> seq 1 ( + , F ) e. dom ~~> )
87 5 79 80 82 83 84 85 86 isumless 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> sum_ k e. ( 1 ... ( 2 ^ j ) ) ( F ` k ) <_ sum_ k e. NN ( F ` k ) )
88 78 87 eqbrtrrd 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> ( seq 1 ( + , F ) ` ( 2 ^ j ) ) <_ sum_ k e. NN ( F ` k ) )
89 57 adantr 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> sum_ k e. NN ( F ` k ) e. RR )
90 2rp 
 |-  2 e. RR+
91 90 a1i 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> 2 e. RR+ )
92 66 89 91 lemul2d 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> ( ( seq 1 ( + , F ) ` ( 2 ^ j ) ) <_ sum_ k e. NN ( F ` k ) <-> ( 2 x. ( seq 1 ( + , F ) ` ( 2 ^ j ) ) ) <_ ( 2 x. sum_ k e. NN ( F ` k ) ) ) )
93 88 92 mpbid 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> ( 2 x. ( seq 1 ( + , F ) ` ( 2 ^ j ) ) ) <_ ( 2 x. sum_ k e. NN ( F ` k ) ) )
94 60 68 69 71 93 letrd 
 |-  ( ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> ( seq 1 ( + , G ) ` j ) <_ ( 2 x. sum_ k e. NN ( F ` k ) ) )
95 94 ralrimiva 
 |-  ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) -> A. j e. NN ( seq 1 ( + , G ) ` j ) <_ ( 2 x. sum_ k e. NN ( F ` k ) ) )
96 brralrspcev 
 |-  ( ( ( 2 x. sum_ k e. NN ( F ` k ) ) e. RR /\ A. j e. NN ( seq 1 ( + , G ) ` j ) <_ ( 2 x. sum_ k e. NN ( F ` k ) ) ) -> E. x e. RR A. j e. NN ( seq 1 ( + , G ) ` j ) <_ x )
97 59 95 96 syl2anc 
 |-  ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) -> E. x e. RR A. j e. NN ( seq 1 ( + , G ) ` j ) <_ x )
98 5 6 23 52 97 climsup 
 |-  ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) -> seq 1 ( + , G ) ~~> sup ( ran seq 1 ( + , G ) , RR , < ) )
99 climrel 
 |-  Rel ~~>
100 99 releldmi 
 |-  ( seq 1 ( + , G ) ~~> sup ( ran seq 1 ( + , G ) , RR , < ) -> seq 1 ( + , G ) e. dom ~~> )
101 98 100 syl 
 |-  ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) -> seq 1 ( + , G ) e. dom ~~> )
102 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
103 1nn0 
 |-  1 e. NN0
104 103 a1i 
 |-  ( ph -> 1 e. NN0 )
105 20 recnd 
 |-  ( ( ph /\ n e. NN0 ) -> ( G ` n ) e. CC )
106 102 104 105 iserex 
 |-  ( ph -> ( seq 0 ( + , G ) e. dom ~~> <-> seq 1 ( + , G ) e. dom ~~> ) )
107 106 biimpar 
 |-  ( ( ph /\ seq 1 ( + , G ) e. dom ~~> ) -> seq 0 ( + , G ) e. dom ~~> )
108 101 107 syldan 
 |-  ( ( ph /\ seq 1 ( + , F ) e. dom ~~> ) -> seq 0 ( + , G ) e. dom ~~> )
109 1zzd 
 |-  ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) -> 1 e. ZZ )
110 61 adantr 
 |-  ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) -> seq 1 ( + , F ) : NN --> RR )
111 elfznn 
 |-  ( k e. ( 1 ... ( j + 1 ) ) -> k e. NN )
112 31 111 1 syl2an 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. ( 1 ... ( j + 1 ) ) ) -> ( F ` k ) e. RR )
113 simpll 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. ( ( j + 1 ) ... ( j + 1 ) ) ) -> ph )
114 peano2nn 
 |-  ( j e. NN -> ( j + 1 ) e. NN )
115 114 adantl 
 |-  ( ( ph /\ j e. NN ) -> ( j + 1 ) e. NN )
116 elfz1eq 
 |-  ( k e. ( ( j + 1 ) ... ( j + 1 ) ) -> k = ( j + 1 ) )
117 eleq1 
 |-  ( k = ( j + 1 ) -> ( k e. NN <-> ( j + 1 ) e. NN ) )
118 117 biimparc 
 |-  ( ( ( j + 1 ) e. NN /\ k = ( j + 1 ) ) -> k e. NN )
119 115 116 118 syl2an 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. ( ( j + 1 ) ... ( j + 1 ) ) ) -> k e. NN )
120 113 119 2 syl2anc 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. ( ( j + 1 ) ... ( j + 1 ) ) ) -> 0 <_ ( F ` k ) )
121 25 30 112 120 sermono 
 |-  ( ( ph /\ j e. NN ) -> ( seq 1 ( + , F ) ` j ) <_ ( seq 1 ( + , F ) ` ( j + 1 ) ) )
122 121 adantlr 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( seq 1 ( + , F ) ` j ) <_ ( seq 1 ( + , F ) ` ( j + 1 ) ) )
123 0zd 
 |-  ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) -> 0 e. ZZ )
124 eqidd 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ n e. NN0 ) -> ( G ` n ) = ( G ` n ) )
125 20 adantlr 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ n e. NN0 ) -> ( G ` n ) e. RR )
126 simpr 
 |-  ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) -> seq 0 ( + , G ) e. dom ~~> )
127 102 123 124 125 126 isumrecl 
 |-  ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) -> sum_ n e. NN0 ( G ` n ) e. RR )
128 110 ffvelcdmda 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( seq 1 ( + , F ) ` j ) e. RR )
129 0zd 
 |-  ( ph -> 0 e. ZZ )
130 102 129 20 serfre 
 |-  ( ph -> seq 0 ( + , G ) : NN0 --> RR )
131 130 adantr 
 |-  ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) -> seq 0 ( + , G ) : NN0 --> RR )
132 ffvelcdm 
 |-  ( ( seq 0 ( + , G ) : NN0 --> RR /\ j e. NN0 ) -> ( seq 0 ( + , G ) ` j ) e. RR )
133 131 37 132 syl2an 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( seq 0 ( + , G ) ` j ) e. RR )
134 127 adantr 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> sum_ n e. NN0 ( G ` n ) e. RR )
135 110 adantr 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> seq 1 ( + , F ) : NN --> RR )
136 simpr 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> j e. NN )
137 26 adantl 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> j e. ZZ )
138 39 adantl 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( j + 1 ) e. NN0 )
139 138 nn0red 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( j + 1 ) e. RR )
140 nnexpcl 
 |-  ( ( 2 e. NN /\ ( j + 1 ) e. NN0 ) -> ( 2 ^ ( j + 1 ) ) e. NN )
141 9 138 140 sylancr 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( 2 ^ ( j + 1 ) ) e. NN )
142 141 nnred 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( 2 ^ ( j + 1 ) ) e. RR )
143 2z 
 |-  2 e. ZZ
144 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
145 143 144 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
146 bernneq3 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ ( j + 1 ) e. NN0 ) -> ( j + 1 ) < ( 2 ^ ( j + 1 ) ) )
147 145 138 146 sylancr 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( j + 1 ) < ( 2 ^ ( j + 1 ) ) )
148 139 142 147 ltled 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( j + 1 ) <_ ( 2 ^ ( j + 1 ) ) )
149 137 peano2zd 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( j + 1 ) e. ZZ )
150 141 nnzd 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( 2 ^ ( j + 1 ) ) e. ZZ )
151 eluz 
 |-  ( ( ( j + 1 ) e. ZZ /\ ( 2 ^ ( j + 1 ) ) e. ZZ ) -> ( ( 2 ^ ( j + 1 ) ) e. ( ZZ>= ` ( j + 1 ) ) <-> ( j + 1 ) <_ ( 2 ^ ( j + 1 ) ) ) )
152 149 150 151 syl2anc 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( ( 2 ^ ( j + 1 ) ) e. ( ZZ>= ` ( j + 1 ) ) <-> ( j + 1 ) <_ ( 2 ^ ( j + 1 ) ) ) )
153 148 152 mpbird 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( 2 ^ ( j + 1 ) ) e. ( ZZ>= ` ( j + 1 ) ) )
154 eluzp1m1 
 |-  ( ( j e. ZZ /\ ( 2 ^ ( j + 1 ) ) e. ( ZZ>= ` ( j + 1 ) ) ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. ( ZZ>= ` j ) )
155 137 153 154 syl2anc 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. ( ZZ>= ` j ) )
156 eluznn 
 |-  ( ( j e. NN /\ ( ( 2 ^ ( j + 1 ) ) - 1 ) e. ( ZZ>= ` j ) ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. NN )
157 136 155 156 syl2anc 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( ( 2 ^ ( j + 1 ) ) - 1 ) e. NN )
158 135 157 ffvelcdmd 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) e. RR )
159 25 adantlr 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> j e. ( ZZ>= ` 1 ) )
160 simpll 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ph )
161 elfznn 
 |-  ( k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) -> k e. NN )
162 160 161 1 syl2an 
 |-  ( ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) /\ k e. ( 1 ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) -> ( F ` k ) e. RR )
163 114 adantl 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( j + 1 ) e. NN )
164 elfzuz 
 |-  ( k e. ( ( j + 1 ) ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) -> k e. ( ZZ>= ` ( j + 1 ) ) )
165 eluznn 
 |-  ( ( ( j + 1 ) e. NN /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> k e. NN )
166 163 164 165 syl2an 
 |-  ( ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) /\ k e. ( ( j + 1 ) ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) -> k e. NN )
167 160 166 2 syl2an2r 
 |-  ( ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) /\ k e. ( ( j + 1 ) ... ( ( 2 ^ ( j + 1 ) ) - 1 ) ) ) -> 0 <_ ( F ` k ) )
168 159 155 162 167 sermono 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( seq 1 ( + , F ) ` j ) <_ ( seq 1 ( + , F ) ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) )
169 37 adantl 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> j e. NN0 )
170 1 2 3 4 climcndslem1 
 |-  ( ( ph /\ j e. NN0 ) -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` j ) )
171 160 169 170 syl2anc 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( j + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` j ) )
172 128 158 133 168 171 letrd 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( seq 1 ( + , F ) ` j ) <_ ( seq 0 ( + , G ) ` j ) )
173 eqidd 
 |-  ( ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) /\ n e. ( 0 ... j ) ) -> ( G ` n ) = ( G ` n ) )
174 169 102 eleqtrdi 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> j e. ( ZZ>= ` 0 ) )
175 elfznn0 
 |-  ( n e. ( 0 ... j ) -> n e. NN0 )
176 160 175 105 syl2an 
 |-  ( ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) /\ n e. ( 0 ... j ) ) -> ( G ` n ) e. CC )
177 173 174 176 fsumser 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> sum_ n e. ( 0 ... j ) ( G ` n ) = ( seq 0 ( + , G ) ` j ) )
178 0zd 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> 0 e. ZZ )
179 fzfid 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( 0 ... j ) e. Fin )
180 175 ssriv 
 |-  ( 0 ... j ) C_ NN0
181 180 a1i 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( 0 ... j ) C_ NN0 )
182 eqidd 
 |-  ( ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) /\ n e. NN0 ) -> ( G ` n ) = ( G ` n ) )
183 20 ad4ant14 
 |-  ( ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) /\ n e. NN0 ) -> ( G ` n ) e. RR )
184 49 ad4ant14 
 |-  ( ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) /\ n e. NN0 ) -> 0 <_ ( G ` n ) )
185 simplr 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> seq 0 ( + , G ) e. dom ~~> )
186 102 178 179 181 182 183 184 185 isumless 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> sum_ n e. ( 0 ... j ) ( G ` n ) <_ sum_ n e. NN0 ( G ` n ) )
187 177 186 eqbrtrrd 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( seq 0 ( + , G ) ` j ) <_ sum_ n e. NN0 ( G ` n ) )
188 128 133 134 172 187 letrd 
 |-  ( ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) /\ j e. NN ) -> ( seq 1 ( + , F ) ` j ) <_ sum_ n e. NN0 ( G ` n ) )
189 188 ralrimiva 
 |-  ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) -> A. j e. NN ( seq 1 ( + , F ) ` j ) <_ sum_ n e. NN0 ( G ` n ) )
190 brralrspcev 
 |-  ( ( sum_ n e. NN0 ( G ` n ) e. RR /\ A. j e. NN ( seq 1 ( + , F ) ` j ) <_ sum_ n e. NN0 ( G ` n ) ) -> E. x e. RR A. j e. NN ( seq 1 ( + , F ) ` j ) <_ x )
191 127 189 190 syl2anc 
 |-  ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) -> E. x e. RR A. j e. NN ( seq 1 ( + , F ) ` j ) <_ x )
192 5 109 110 122 191 climsup 
 |-  ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) -> seq 1 ( + , F ) ~~> sup ( ran seq 1 ( + , F ) , RR , < ) )
193 99 releldmi 
 |-  ( seq 1 ( + , F ) ~~> sup ( ran seq 1 ( + , F ) , RR , < ) -> seq 1 ( + , F ) e. dom ~~> )
194 192 193 syl 
 |-  ( ( ph /\ seq 0 ( + , G ) e. dom ~~> ) -> seq 1 ( + , F ) e. dom ~~> )
195 108 194 impbida 
 |-  ( ph -> ( seq 1 ( + , F ) e. dom ~~> <-> seq 0 ( + , G ) e. dom ~~> ) )