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

Metamath Proof Explorer

Theorem mbfi1fseqlem6

Description: Lemma for mbfi1fseq . Verify that G converges pointwise to F , and wrap up the existential quantifier. (Contributed by Mario Carneiro, 16-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses mbfi1fseq.1 
|- ( ph -> F e. MblFn )
mbfi1fseq.2 
|- ( ph -> F : RR --> ( 0 [,) +oo ) )
mbfi1fseq.3 
|- J = ( m e. NN , y e. RR |-> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) )
mbfi1fseq.4 
|- G = ( m e. NN |-> ( x e. RR |-> if ( x e. ( -u m [,] m ) , if ( ( m J x ) <_ m , ( m J x ) , m ) , 0 ) ) )
Assertion mbfi1fseqlem6 
|- ( ph -> E. g ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) )

Proof

Step Hyp Ref Expression
1 mbfi1fseq.1 
 |-  ( ph -> F e. MblFn )
2 mbfi1fseq.2 
 |-  ( ph -> F : RR --> ( 0 [,) +oo ) )
3 mbfi1fseq.3 
 |-  J = ( m e. NN , y e. RR |-> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) )
4 mbfi1fseq.4 
 |-  G = ( m e. NN |-> ( x e. RR |-> if ( x e. ( -u m [,] m ) , if ( ( m J x ) <_ m , ( m J x ) , m ) , 0 ) ) )
5 1 2 3 4 mbfi1fseqlem4 
 |-  ( ph -> G : NN --> dom S.1 )
6 1 2 3 4 mbfi1fseqlem5 
 |-  ( ( ph /\ n e. NN ) -> ( 0p oR <_ ( G ` n ) /\ ( G ` n ) oR <_ ( G ` ( n + 1 ) ) ) )
7 6 ralrimiva 
 |-  ( ph -> A. n e. NN ( 0p oR <_ ( G ` n ) /\ ( G ` n ) oR <_ ( G ` ( n + 1 ) ) ) )
8 simpr 
 |-  ( ( ph /\ x e. RR ) -> x e. RR )
9 8 recnd 
 |-  ( ( ph /\ x e. RR ) -> x e. CC )
10 9 abscld 
 |-  ( ( ph /\ x e. RR ) -> ( abs ` x ) e. RR )
11 2 ffvelcdmda 
 |-  ( ( ph /\ x e. RR ) -> ( F ` x ) e. ( 0 [,) +oo ) )
12 elrege0 
 |-  ( ( F ` x ) e. ( 0 [,) +oo ) <-> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
13 11 12 sylib 
 |-  ( ( ph /\ x e. RR ) -> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
14 13 simpld 
 |-  ( ( ph /\ x e. RR ) -> ( F ` x ) e. RR )
15 10 14 readdcld 
 |-  ( ( ph /\ x e. RR ) -> ( ( abs ` x ) + ( F ` x ) ) e. RR )
16 arch 
 |-  ( ( ( abs ` x ) + ( F ` x ) ) e. RR -> E. k e. NN ( ( abs ` x ) + ( F ` x ) ) < k )
17 15 16 syl 
 |-  ( ( ph /\ x e. RR ) -> E. k e. NN ( ( abs ` x ) + ( F ` x ) ) < k )
18 eqid 
 |-  ( ZZ>= ` k ) = ( ZZ>= ` k )
19 nnz 
 |-  ( k e. NN -> k e. ZZ )
20 19 ad2antrl 
 |-  ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) -> k e. ZZ )
21 nnuz 
 |-  NN = ( ZZ>= ` 1 )
22 1zzd 
 |-  ( ( ph /\ x e. RR ) -> 1 e. ZZ )
23 halfcn 
 |-  ( 1 / 2 ) e. CC
24 23 a1i 
 |-  ( ( ph /\ x e. RR ) -> ( 1 / 2 ) e. CC )
25 halfre 
 |-  ( 1 / 2 ) e. RR
26 halfge0 
 |-  0 <_ ( 1 / 2 )
27 absid 
 |-  ( ( ( 1 / 2 ) e. RR /\ 0 <_ ( 1 / 2 ) ) -> ( abs ` ( 1 / 2 ) ) = ( 1 / 2 ) )
28 25 26 27 mp2an 
 |-  ( abs ` ( 1 / 2 ) ) = ( 1 / 2 )
29 halflt1 
 |-  ( 1 / 2 ) < 1
30 28 29 eqbrtri 
 |-  ( abs ` ( 1 / 2 ) ) < 1
31 30 a1i 
 |-  ( ( ph /\ x e. RR ) -> ( abs ` ( 1 / 2 ) ) < 1 )
32 24 31 expcnv 
 |-  ( ( ph /\ x e. RR ) -> ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ~~> 0 )
33 14 recnd 
 |-  ( ( ph /\ x e. RR ) -> ( F ` x ) e. CC )
34 nnex 
 |-  NN e. _V
35 34 mptex 
 |-  ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) e. _V
36 35 a1i 
 |-  ( ( ph /\ x e. RR ) -> ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) e. _V )
37 nnnn0 
 |-  ( j e. NN -> j e. NN0 )
38 37 adantl 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> j e. NN0 )
39 oveq2 
 |-  ( n = j -> ( ( 1 / 2 ) ^ n ) = ( ( 1 / 2 ) ^ j ) )
40 eqid 
 |-  ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) = ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) )
41 ovex 
 |-  ( ( 1 / 2 ) ^ j ) e. _V
42 39 40 41 fvmpt 
 |-  ( j e. NN0 -> ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` j ) = ( ( 1 / 2 ) ^ j ) )
43 38 42 syl 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` j ) = ( ( 1 / 2 ) ^ j ) )
44 expcl 
 |-  ( ( ( 1 / 2 ) e. CC /\ j e. NN0 ) -> ( ( 1 / 2 ) ^ j ) e. CC )
45 23 38 44 sylancr 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( ( 1 / 2 ) ^ j ) e. CC )
46 43 45 eqeltrd 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` j ) e. CC )
47 39 oveq2d 
 |-  ( n = j -> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) = ( ( F ` x ) - ( ( 1 / 2 ) ^ j ) ) )
48 eqid 
 |-  ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) = ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) )
49 ovex 
 |-  ( ( F ` x ) - ( ( 1 / 2 ) ^ j ) ) e. _V
50 47 48 49 fvmpt 
 |-  ( j e. NN -> ( ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) ` j ) = ( ( F ` x ) - ( ( 1 / 2 ) ^ j ) ) )
51 50 adantl 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) ` j ) = ( ( F ` x ) - ( ( 1 / 2 ) ^ j ) ) )
52 43 oveq2d 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( ( F ` x ) - ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` j ) ) = ( ( F ` x ) - ( ( 1 / 2 ) ^ j ) ) )
53 51 52 eqtr4d 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) ` j ) = ( ( F ` x ) - ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` j ) ) )
54 21 22 32 33 36 46 53 climsubc2 
 |-  ( ( ph /\ x e. RR ) -> ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) ~~> ( ( F ` x ) - 0 ) )
55 33 subid1d 
 |-  ( ( ph /\ x e. RR ) -> ( ( F ` x ) - 0 ) = ( F ` x ) )
56 54 55 breqtrd 
 |-  ( ( ph /\ x e. RR ) -> ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) ~~> ( F ` x ) )
57 56 adantr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) -> ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) ~~> ( F ` x ) )
58 34 mptex 
 |-  ( n e. NN |-> ( ( G ` n ) ` x ) ) e. _V
59 58 a1i 
 |-  ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) -> ( n e. NN |-> ( ( G ` n ) ` x ) ) e. _V )
60 simprl 
 |-  ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) -> k e. NN )
61 eluznn 
 |-  ( ( k e. NN /\ j e. ( ZZ>= ` k ) ) -> j e. NN )
62 60 61 sylan 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> j e. NN )
63 62 50 syl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) ` j ) = ( ( F ` x ) - ( ( 1 / 2 ) ^ j ) ) )
64 14 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( F ` x ) e. RR )
65 62 37 syl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> j e. NN0 )
66 reexpcl 
 |-  ( ( ( 1 / 2 ) e. RR /\ j e. NN0 ) -> ( ( 1 / 2 ) ^ j ) e. RR )
67 25 65 66 sylancr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( 1 / 2 ) ^ j ) e. RR )
68 64 67 resubcld 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( F ` x ) - ( ( 1 / 2 ) ^ j ) ) e. RR )
69 63 68 eqeltrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) ` j ) e. RR )
70 fveq2 
 |-  ( n = j -> ( G ` n ) = ( G ` j ) )
71 70 fveq1d 
 |-  ( n = j -> ( ( G ` n ) ` x ) = ( ( G ` j ) ` x ) )
72 eqid 
 |-  ( n e. NN |-> ( ( G ` n ) ` x ) ) = ( n e. NN |-> ( ( G ` n ) ` x ) )
73 fvex 
 |-  ( ( G ` j ) ` x ) e. _V
74 71 72 73 fvmpt 
 |-  ( j e. NN -> ( ( n e. NN |-> ( ( G ` n ) ` x ) ) ` j ) = ( ( G ` j ) ` x ) )
75 62 74 syl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( n e. NN |-> ( ( G ` n ) ` x ) ) ` j ) = ( ( G ` j ) ` x ) )
76 5 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> G : NN --> dom S.1 )
77 76 62 ffvelcdmd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( G ` j ) e. dom S.1 )
78 i1ff 
 |-  ( ( G ` j ) e. dom S.1 -> ( G ` j ) : RR --> RR )
79 77 78 syl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( G ` j ) : RR --> RR )
80 8 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> x e. RR )
81 79 80 ffvelcdmd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( G ` j ) ` x ) e. RR )
82 75 81 eqeltrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( n e. NN |-> ( ( G ` n ) ` x ) ) ` j ) e. RR )
83 33 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( F ` x ) e. CC )
84 2nn 
 |-  2 e. NN
85 nnexpcl 
 |-  ( ( 2 e. NN /\ j e. NN0 ) -> ( 2 ^ j ) e. NN )
86 84 65 85 sylancr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( 2 ^ j ) e. NN )
87 86 nnred 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( 2 ^ j ) e. RR )
88 87 recnd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( 2 ^ j ) e. CC )
89 86 nnne0d 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( 2 ^ j ) =/= 0 )
90 83 88 89 divcan4d 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( ( F ` x ) x. ( 2 ^ j ) ) / ( 2 ^ j ) ) = ( F ` x ) )
91 90 eqcomd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( F ` x ) = ( ( ( F ` x ) x. ( 2 ^ j ) ) / ( 2 ^ j ) ) )
92 2cnd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> 2 e. CC )
93 2ne0 
 |-  2 =/= 0
94 93 a1i 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> 2 =/= 0 )
95 eluzelz 
 |-  ( j e. ( ZZ>= ` k ) -> j e. ZZ )
96 95 adantl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> j e. ZZ )
97 92 94 96 exprecd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( 1 / 2 ) ^ j ) = ( 1 / ( 2 ^ j ) ) )
98 91 97 oveq12d 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( F ` x ) - ( ( 1 / 2 ) ^ j ) ) = ( ( ( ( F ` x ) x. ( 2 ^ j ) ) / ( 2 ^ j ) ) - ( 1 / ( 2 ^ j ) ) ) )
99 64 87 remulcld 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( F ` x ) x. ( 2 ^ j ) ) e. RR )
100 99 recnd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( F ` x ) x. ( 2 ^ j ) ) e. CC )
101 1cnd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> 1 e. CC )
102 100 101 88 89 divsubdird 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) / ( 2 ^ j ) ) = ( ( ( ( F ` x ) x. ( 2 ^ j ) ) / ( 2 ^ j ) ) - ( 1 / ( 2 ^ j ) ) ) )
103 98 102 eqtr4d 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( F ` x ) - ( ( 1 / 2 ) ^ j ) ) = ( ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) / ( 2 ^ j ) ) )
104 fllep1 
 |-  ( ( ( F ` x ) x. ( 2 ^ j ) ) e. RR -> ( ( F ` x ) x. ( 2 ^ j ) ) <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) + 1 ) )
105 99 104 syl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( F ` x ) x. ( 2 ^ j ) ) <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) + 1 ) )
106 1red 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> 1 e. RR )
107 reflcl 
 |-  ( ( ( F ` x ) x. ( 2 ^ j ) ) e. RR -> ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) e. RR )
108 99 107 syl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) e. RR )
109 99 106 108 lesubaddd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) <-> ( ( F ` x ) x. ( 2 ^ j ) ) <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) + 1 ) ) )
110 105 109 mpbird 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) )
111 peano2rem 
 |-  ( ( ( F ` x ) x. ( 2 ^ j ) ) e. RR -> ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) e. RR )
112 99 111 syl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) e. RR )
113 86 nngt0d 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> 0 < ( 2 ^ j ) )
114 lediv1 
 |-  ( ( ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) e. RR /\ ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) e. RR /\ ( ( 2 ^ j ) e. RR /\ 0 < ( 2 ^ j ) ) ) -> ( ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) <-> ( ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) / ( 2 ^ j ) ) <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) )
115 112 108 87 113 114 syl112anc 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) <-> ( ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) / ( 2 ^ j ) ) <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) )
116 110 115 mpbid 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) / ( 2 ^ j ) ) <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) )
117 103 116 eqbrtrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( F ` x ) - ( ( 1 / 2 ) ^ j ) ) <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) )
118 1 2 3 4 mbfi1fseqlem2 
 |-  ( j e. NN -> ( G ` j ) = ( x e. RR |-> if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) ) )
119 62 118 syl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( G ` j ) = ( x e. RR |-> if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) ) )
120 119 fveq1d 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( G ` j ) ` x ) = ( ( x e. RR |-> if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) ) ` x ) )
121 ovex 
 |-  ( j J x ) e. _V
122 vex 
 |-  j e. _V
123 121 122 ifex 
 |-  if ( ( j J x ) <_ j , ( j J x ) , j ) e. _V
124 c0ex 
 |-  0 e. _V
125 123 124 ifex 
 |-  if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) e. _V
126 eqid 
 |-  ( x e. RR |-> if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) ) = ( x e. RR |-> if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) )
127 126 fvmpt2 
 |-  ( ( x e. RR /\ if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) e. _V ) -> ( ( x e. RR |-> if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) ) ` x ) = if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) )
128 80 125 127 sylancl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( x e. RR |-> if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) ) ` x ) = if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) )
129 75 120 128 3eqtrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( n e. NN |-> ( ( G ` n ) ` x ) ) ` j ) = if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) )
130 10 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( abs ` x ) e. RR )
131 15 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( abs ` x ) + ( F ` x ) ) e. RR )
132 62 nnred 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> j e. RR )
133 11 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( F ` x ) e. ( 0 [,) +oo ) )
134 133 12 sylib 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
135 134 simprd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> 0 <_ ( F ` x ) )
136 130 64 addge01d 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( 0 <_ ( F ` x ) <-> ( abs ` x ) <_ ( ( abs ` x ) + ( F ` x ) ) ) )
137 135 136 mpbid 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( abs ` x ) <_ ( ( abs ` x ) + ( F ` x ) ) )
138 60 adantr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> k e. NN )
139 138 nnred 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> k e. RR )
140 simplrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( abs ` x ) + ( F ` x ) ) < k )
141 131 139 140 ltled 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( abs ` x ) + ( F ` x ) ) <_ k )
142 eluzle 
 |-  ( j e. ( ZZ>= ` k ) -> k <_ j )
143 142 adantl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> k <_ j )
144 131 139 132 141 143 letrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( abs ` x ) + ( F ` x ) ) <_ j )
145 130 131 132 137 144 letrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( abs ` x ) <_ j )
146 80 132 absled 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( abs ` x ) <_ j <-> ( -u j <_ x /\ x <_ j ) ) )
147 145 146 mpbid 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( -u j <_ x /\ x <_ j ) )
148 147 simpld 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> -u j <_ x )
149 147 simprd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> x <_ j )
150 132 renegcld 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> -u j e. RR )
151 elicc2 
 |-  ( ( -u j e. RR /\ j e. RR ) -> ( x e. ( -u j [,] j ) <-> ( x e. RR /\ -u j <_ x /\ x <_ j ) ) )
152 150 132 151 syl2anc 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( x e. ( -u j [,] j ) <-> ( x e. RR /\ -u j <_ x /\ x <_ j ) ) )
153 80 148 149 152 mpbir3and 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> x e. ( -u j [,] j ) )
154 153 iftrued 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) = if ( ( j J x ) <_ j , ( j J x ) , j ) )
155 simpr 
 |-  ( ( m = j /\ y = x ) -> y = x )
156 155 fveq2d 
 |-  ( ( m = j /\ y = x ) -> ( F ` y ) = ( F ` x ) )
157 simpl 
 |-  ( ( m = j /\ y = x ) -> m = j )
158 157 oveq2d 
 |-  ( ( m = j /\ y = x ) -> ( 2 ^ m ) = ( 2 ^ j ) )
159 156 158 oveq12d 
 |-  ( ( m = j /\ y = x ) -> ( ( F ` y ) x. ( 2 ^ m ) ) = ( ( F ` x ) x. ( 2 ^ j ) ) )
160 159 fveq2d 
 |-  ( ( m = j /\ y = x ) -> ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) = ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) )
161 160 158 oveq12d 
 |-  ( ( m = j /\ y = x ) -> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) )
162 ovex 
 |-  ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) e. _V
163 161 3 162 ovmpoa 
 |-  ( ( j e. NN /\ x e. RR ) -> ( j J x ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) )
164 62 80 163 syl2anc 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( j J x ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) )
165 108 86 nndivred 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) e. RR )
166 flle 
 |-  ( ( ( F ` x ) x. ( 2 ^ j ) ) e. RR -> ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) <_ ( ( F ` x ) x. ( 2 ^ j ) ) )
167 99 166 syl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) <_ ( ( F ` x ) x. ( 2 ^ j ) ) )
168 ledivmul2 
 |-  ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) e. RR /\ ( F ` x ) e. RR /\ ( ( 2 ^ j ) e. RR /\ 0 < ( 2 ^ j ) ) ) -> ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) <_ ( F ` x ) <-> ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) <_ ( ( F ` x ) x. ( 2 ^ j ) ) ) )
169 108 64 87 113 168 syl112anc 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) <_ ( F ` x ) <-> ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) <_ ( ( F ` x ) x. ( 2 ^ j ) ) ) )
170 167 169 mpbird 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) <_ ( F ` x ) )
171 9 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> x e. CC )
172 171 absge0d 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> 0 <_ ( abs ` x ) )
173 64 130 addge02d 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( 0 <_ ( abs ` x ) <-> ( F ` x ) <_ ( ( abs ` x ) + ( F ` x ) ) ) )
174 172 173 mpbid 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( F ` x ) <_ ( ( abs ` x ) + ( F ` x ) ) )
175 64 131 132 174 144 letrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( F ` x ) <_ j )
176 165 64 132 170 175 letrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) <_ j )
177 164 176 eqbrtrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( j J x ) <_ j )
178 177 iftrued 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> if ( ( j J x ) <_ j , ( j J x ) , j ) = ( j J x ) )
179 178 164 eqtrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> if ( ( j J x ) <_ j , ( j J x ) , j ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) )
180 129 154 179 3eqtrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( n e. NN |-> ( ( G ` n ) ` x ) ) ` j ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) )
181 117 63 180 3brtr4d 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) ` j ) <_ ( ( n e. NN |-> ( ( G ` n ) ` x ) ) ` j ) )
182 180 170 eqbrtrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( n e. NN |-> ( ( G ` n ) ` x ) ) ` j ) <_ ( F ` x ) )
183 18 20 57 59 69 82 181 182 climsqz 
 |-  ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) -> ( n e. NN |-> ( ( G ` n ) ` x ) ) ~~> ( F ` x ) )
184 17 183 rexlimddv 
 |-  ( ( ph /\ x e. RR ) -> ( n e. NN |-> ( ( G ` n ) ` x ) ) ~~> ( F ` x ) )
185 184 ralrimiva 
 |-  ( ph -> A. x e. RR ( n e. NN |-> ( ( G ` n ) ` x ) ) ~~> ( F ` x ) )
186 34 mptex 
 |-  ( m e. NN |-> ( x e. RR |-> if ( x e. ( -u m [,] m ) , if ( ( m J x ) <_ m , ( m J x ) , m ) , 0 ) ) ) e. _V
187 4 186 eqeltri 
 |-  G e. _V
188 feq1 
 |-  ( g = G -> ( g : NN --> dom S.1 <-> G : NN --> dom S.1 ) )
189 fveq1 
 |-  ( g = G -> ( g ` n ) = ( G ` n ) )
190 189 breq2d 
 |-  ( g = G -> ( 0p oR <_ ( g ` n ) <-> 0p oR <_ ( G ` n ) ) )
191 fveq1 
 |-  ( g = G -> ( g ` ( n + 1 ) ) = ( G ` ( n + 1 ) ) )
192 189 191 breq12d 
 |-  ( g = G -> ( ( g ` n ) oR <_ ( g ` ( n + 1 ) ) <-> ( G ` n ) oR <_ ( G ` ( n + 1 ) ) ) )
193 190 192 anbi12d 
 |-  ( g = G -> ( ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) <-> ( 0p oR <_ ( G ` n ) /\ ( G ` n ) oR <_ ( G ` ( n + 1 ) ) ) ) )
194 193 ralbidv 
 |-  ( g = G -> ( A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) <-> A. n e. NN ( 0p oR <_ ( G ` n ) /\ ( G ` n ) oR <_ ( G ` ( n + 1 ) ) ) ) )
195 189 fveq1d 
 |-  ( g = G -> ( ( g ` n ) ` x ) = ( ( G ` n ) ` x ) )
196 195 mpteq2dv 
 |-  ( g = G -> ( n e. NN |-> ( ( g ` n ) ` x ) ) = ( n e. NN |-> ( ( G ` n ) ` x ) ) )
197 196 breq1d 
 |-  ( g = G -> ( ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) <-> ( n e. NN |-> ( ( G ` n ) ` x ) ) ~~> ( F ` x ) ) )
198 197 ralbidv 
 |-  ( g = G -> ( A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) <-> A. x e. RR ( n e. NN |-> ( ( G ` n ) ` x ) ) ~~> ( F ` x ) ) )
199 188 194 198 3anbi123d 
 |-  ( g = G -> ( ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) <-> ( G : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( G ` n ) /\ ( G ` n ) oR <_ ( G ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( G ` n ) ` x ) ) ~~> ( F ` x ) ) ) )
200 187 199 spcev 
 |-  ( ( G : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( G ` n ) /\ ( G ` n ) oR <_ ( G ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( G ` n ) ` x ) ) ~~> ( F ` x ) ) -> E. g ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) )
201 5 7 185 200 syl3anc 
 |-  ( ph -> E. g ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) )