Metamath Proof Explorer


Theorem mbfi1flimlem

Description: Lemma for mbfi1flim . (Contributed by Mario Carneiro, 5-Sep-2014)

Ref Expression
Hypotheses mbfi1flim.1
|- ( ph -> F e. MblFn )
mbfi1flimlem.2
|- ( ph -> F : RR --> RR )
Assertion mbfi1flimlem
|- ( ph -> E. g ( g : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) )

Proof

Step Hyp Ref Expression
1 mbfi1flim.1
 |-  ( ph -> F e. MblFn )
2 mbfi1flimlem.2
 |-  ( ph -> F : RR --> RR )
3 2 ffvelrnda
 |-  ( ( ph /\ y e. RR ) -> ( F ` y ) e. RR )
4 2 feqmptd
 |-  ( ph -> F = ( y e. RR |-> ( F ` y ) ) )
5 4 1 eqeltrrd
 |-  ( ph -> ( y e. RR |-> ( F ` y ) ) e. MblFn )
6 3 5 mbfpos
 |-  ( ph -> ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) e. MblFn )
7 0re
 |-  0 e. RR
8 ifcl
 |-  ( ( ( F ` y ) e. RR /\ 0 e. RR ) -> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) e. RR )
9 3 7 8 sylancl
 |-  ( ( ph /\ y e. RR ) -> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) e. RR )
10 max1
 |-  ( ( 0 e. RR /\ ( F ` y ) e. RR ) -> 0 <_ if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) )
11 7 3 10 sylancr
 |-  ( ( ph /\ y e. RR ) -> 0 <_ if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) )
12 elrege0
 |-  ( if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) e. ( 0 [,) +oo ) <-> ( if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) e. RR /\ 0 <_ if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) )
13 9 11 12 sylanbrc
 |-  ( ( ph /\ y e. RR ) -> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) e. ( 0 [,) +oo ) )
14 13 fmpttd
 |-  ( ph -> ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) : RR --> ( 0 [,) +oo ) )
15 6 14 mbfi1fseq
 |-  ( ph -> E. f ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) ) )
16 3 renegcld
 |-  ( ( ph /\ y e. RR ) -> -u ( F ` y ) e. RR )
17 3 5 mbfneg
 |-  ( ph -> ( y e. RR |-> -u ( F ` y ) ) e. MblFn )
18 16 17 mbfpos
 |-  ( ph -> ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) e. MblFn )
19 ifcl
 |-  ( ( -u ( F ` y ) e. RR /\ 0 e. RR ) -> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) e. RR )
20 16 7 19 sylancl
 |-  ( ( ph /\ y e. RR ) -> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) e. RR )
21 max1
 |-  ( ( 0 e. RR /\ -u ( F ` y ) e. RR ) -> 0 <_ if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) )
22 7 16 21 sylancr
 |-  ( ( ph /\ y e. RR ) -> 0 <_ if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) )
23 elrege0
 |-  ( if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) e. ( 0 [,) +oo ) <-> ( if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) e. RR /\ 0 <_ if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) )
24 20 22 23 sylanbrc
 |-  ( ( ph /\ y e. RR ) -> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) e. ( 0 [,) +oo ) )
25 24 fmpttd
 |-  ( ph -> ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) : RR --> ( 0 [,) +oo ) )
26 18 25 mbfi1fseq
 |-  ( ph -> E. h ( h : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( h ` n ) /\ ( h ` n ) oR <_ ( h ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) )
27 exdistrv
 |-  ( E. f E. h ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) ) /\ ( h : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( h ` n ) /\ ( h ` n ) oR <_ ( h ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) ) <-> ( E. f ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) ) /\ E. h ( h : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( h ` n ) /\ ( h ` n ) oR <_ ( h ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) ) )
28 3simpb
 |-  ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) ) -> ( f : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) ) )
29 3simpb
 |-  ( ( h : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( h ` n ) /\ ( h ` n ) oR <_ ( h ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) -> ( h : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) )
30 28 29 anim12i
 |-  ( ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) ) /\ ( h : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( h ` n ) /\ ( h ` n ) oR <_ ( h ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) ) -> ( ( f : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) ) /\ ( h : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) ) )
31 an4
 |-  ( ( ( f : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) ) /\ ( h : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) ) <-> ( ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) /\ ( A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) /\ A. x e. RR ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) ) )
32 30 31 sylib
 |-  ( ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) ) /\ ( h : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( h ` n ) /\ ( h ` n ) oR <_ ( h ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) ) -> ( ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) /\ ( A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) /\ A. x e. RR ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) ) )
33 r19.26
 |-  ( A. x e. RR ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) <-> ( A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) /\ A. x e. RR ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) )
34 i1fsub
 |-  ( ( x e. dom S.1 /\ y e. dom S.1 ) -> ( x oF - y ) e. dom S.1 )
35 34 adantl
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ ( x e. dom S.1 /\ y e. dom S.1 ) ) -> ( x oF - y ) e. dom S.1 )
36 simprl
 |-  ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) -> f : NN --> dom S.1 )
37 simprr
 |-  ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) -> h : NN --> dom S.1 )
38 nnex
 |-  NN e. _V
39 38 a1i
 |-  ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) -> NN e. _V )
40 inidm
 |-  ( NN i^i NN ) = NN
41 35 36 37 39 39 40 off
 |-  ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) -> ( f oF oF - h ) : NN --> dom S.1 )
42 fveq2
 |-  ( y = x -> ( F ` y ) = ( F ` x ) )
43 42 breq2d
 |-  ( y = x -> ( 0 <_ ( F ` y ) <-> 0 <_ ( F ` x ) ) )
44 43 42 ifbieq1d
 |-  ( y = x -> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) = if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) )
45 eqid
 |-  ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) = ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) )
46 fvex
 |-  ( F ` x ) e. _V
47 c0ex
 |-  0 e. _V
48 46 47 ifex
 |-  if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) e. _V
49 44 45 48 fvmpt
 |-  ( x e. RR -> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) = if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) )
50 49 breq2d
 |-  ( x e. RR -> ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) <-> ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) )
51 42 negeqd
 |-  ( y = x -> -u ( F ` y ) = -u ( F ` x ) )
52 51 breq2d
 |-  ( y = x -> ( 0 <_ -u ( F ` y ) <-> 0 <_ -u ( F ` x ) ) )
53 52 51 ifbieq1d
 |-  ( y = x -> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) = if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) )
54 eqid
 |-  ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) = ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) )
55 negex
 |-  -u ( F ` x ) e. _V
56 55 47 ifex
 |-  if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) e. _V
57 53 54 56 fvmpt
 |-  ( x e. RR -> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) = if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) )
58 57 breq2d
 |-  ( x e. RR -> ( ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) <-> ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) )
59 50 58 anbi12d
 |-  ( x e. RR -> ( ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) <-> ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) )
60 59 adantl
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) -> ( ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) <-> ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) )
61 nnuz
 |-  NN = ( ZZ>= ` 1 )
62 1zzd
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) /\ ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) -> 1 e. ZZ )
63 simprl
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) /\ ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) -> ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) )
64 38 mptex
 |-  ( n e. NN |-> ( ( ( f oF oF - h ) ` n ) ` x ) ) e. _V
65 64 a1i
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) /\ ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) -> ( n e. NN |-> ( ( ( f oF oF - h ) ` n ) ` x ) ) e. _V )
66 simprr
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) /\ ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) -> ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) )
67 36 ffvelrnda
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ n e. NN ) -> ( f ` n ) e. dom S.1 )
68 i1ff
 |-  ( ( f ` n ) e. dom S.1 -> ( f ` n ) : RR --> RR )
69 67 68 syl
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ n e. NN ) -> ( f ` n ) : RR --> RR )
70 69 ffvelrnda
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ n e. NN ) /\ x e. RR ) -> ( ( f ` n ) ` x ) e. RR )
71 70 an32s
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) /\ n e. NN ) -> ( ( f ` n ) ` x ) e. RR )
72 71 recnd
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) /\ n e. NN ) -> ( ( f ` n ) ` x ) e. CC )
73 72 fmpttd
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) -> ( n e. NN |-> ( ( f ` n ) ` x ) ) : NN --> CC )
74 73 adantr
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) /\ ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) -> ( n e. NN |-> ( ( f ` n ) ` x ) ) : NN --> CC )
75 74 ffvelrnda
 |-  ( ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) /\ ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ` k ) e. CC )
76 37 ffvelrnda
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ n e. NN ) -> ( h ` n ) e. dom S.1 )
77 i1ff
 |-  ( ( h ` n ) e. dom S.1 -> ( h ` n ) : RR --> RR )
78 76 77 syl
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ n e. NN ) -> ( h ` n ) : RR --> RR )
79 78 ffvelrnda
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ n e. NN ) /\ x e. RR ) -> ( ( h ` n ) ` x ) e. RR )
80 79 an32s
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) /\ n e. NN ) -> ( ( h ` n ) ` x ) e. RR )
81 80 recnd
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) /\ n e. NN ) -> ( ( h ` n ) ` x ) e. CC )
82 81 fmpttd
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) -> ( n e. NN |-> ( ( h ` n ) ` x ) ) : NN --> CC )
83 82 adantr
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) /\ ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) -> ( n e. NN |-> ( ( h ` n ) ` x ) ) : NN --> CC )
84 83 ffvelrnda
 |-  ( ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) /\ ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( h ` n ) ` x ) ) ` k ) e. CC )
85 36 ffnd
 |-  ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) -> f Fn NN )
86 37 ffnd
 |-  ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) -> h Fn NN )
87 eqidd
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ k e. NN ) -> ( f ` k ) = ( f ` k ) )
88 eqidd
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ k e. NN ) -> ( h ` k ) = ( h ` k ) )
89 85 86 39 39 40 87 88 ofval
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ k e. NN ) -> ( ( f oF oF - h ) ` k ) = ( ( f ` k ) oF - ( h ` k ) ) )
90 89 fveq1d
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ k e. NN ) -> ( ( ( f oF oF - h ) ` k ) ` x ) = ( ( ( f ` k ) oF - ( h ` k ) ) ` x ) )
91 90 adantr
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ k e. NN ) /\ x e. RR ) -> ( ( ( f oF oF - h ) ` k ) ` x ) = ( ( ( f ` k ) oF - ( h ` k ) ) ` x ) )
92 36 ffvelrnda
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ k e. NN ) -> ( f ` k ) e. dom S.1 )
93 i1ff
 |-  ( ( f ` k ) e. dom S.1 -> ( f ` k ) : RR --> RR )
94 ffn
 |-  ( ( f ` k ) : RR --> RR -> ( f ` k ) Fn RR )
95 92 93 94 3syl
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ k e. NN ) -> ( f ` k ) Fn RR )
96 37 ffvelrnda
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ k e. NN ) -> ( h ` k ) e. dom S.1 )
97 i1ff
 |-  ( ( h ` k ) e. dom S.1 -> ( h ` k ) : RR --> RR )
98 ffn
 |-  ( ( h ` k ) : RR --> RR -> ( h ` k ) Fn RR )
99 96 97 98 3syl
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ k e. NN ) -> ( h ` k ) Fn RR )
100 reex
 |-  RR e. _V
101 100 a1i
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ k e. NN ) -> RR e. _V )
102 inidm
 |-  ( RR i^i RR ) = RR
103 eqidd
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ k e. NN ) /\ x e. RR ) -> ( ( f ` k ) ` x ) = ( ( f ` k ) ` x ) )
104 eqidd
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ k e. NN ) /\ x e. RR ) -> ( ( h ` k ) ` x ) = ( ( h ` k ) ` x ) )
105 95 99 101 101 102 103 104 ofval
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ k e. NN ) /\ x e. RR ) -> ( ( ( f ` k ) oF - ( h ` k ) ) ` x ) = ( ( ( f ` k ) ` x ) - ( ( h ` k ) ` x ) ) )
106 91 105 eqtrd
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ k e. NN ) /\ x e. RR ) -> ( ( ( f oF oF - h ) ` k ) ` x ) = ( ( ( f ` k ) ` x ) - ( ( h ` k ) ` x ) ) )
107 106 an32s
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) /\ k e. NN ) -> ( ( ( f oF oF - h ) ` k ) ` x ) = ( ( ( f ` k ) ` x ) - ( ( h ` k ) ` x ) ) )
108 fveq2
 |-  ( n = k -> ( ( f oF oF - h ) ` n ) = ( ( f oF oF - h ) ` k ) )
109 108 fveq1d
 |-  ( n = k -> ( ( ( f oF oF - h ) ` n ) ` x ) = ( ( ( f oF oF - h ) ` k ) ` x ) )
110 eqid
 |-  ( n e. NN |-> ( ( ( f oF oF - h ) ` n ) ` x ) ) = ( n e. NN |-> ( ( ( f oF oF - h ) ` n ) ` x ) )
111 fvex
 |-  ( ( ( f oF oF - h ) ` k ) ` x ) e. _V
112 109 110 111 fvmpt
 |-  ( k e. NN -> ( ( n e. NN |-> ( ( ( f oF oF - h ) ` n ) ` x ) ) ` k ) = ( ( ( f oF oF - h ) ` k ) ` x ) )
113 112 adantl
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( ( f oF oF - h ) ` n ) ` x ) ) ` k ) = ( ( ( f oF oF - h ) ` k ) ` x ) )
114 fveq2
 |-  ( n = k -> ( f ` n ) = ( f ` k ) )
115 114 fveq1d
 |-  ( n = k -> ( ( f ` n ) ` x ) = ( ( f ` k ) ` x ) )
116 eqid
 |-  ( n e. NN |-> ( ( f ` n ) ` x ) ) = ( n e. NN |-> ( ( f ` n ) ` x ) )
117 fvex
 |-  ( ( f ` k ) ` x ) e. _V
118 115 116 117 fvmpt
 |-  ( k e. NN -> ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ` k ) = ( ( f ` k ) ` x ) )
119 fveq2
 |-  ( n = k -> ( h ` n ) = ( h ` k ) )
120 119 fveq1d
 |-  ( n = k -> ( ( h ` n ) ` x ) = ( ( h ` k ) ` x ) )
121 eqid
 |-  ( n e. NN |-> ( ( h ` n ) ` x ) ) = ( n e. NN |-> ( ( h ` n ) ` x ) )
122 fvex
 |-  ( ( h ` k ) ` x ) e. _V
123 120 121 122 fvmpt
 |-  ( k e. NN -> ( ( n e. NN |-> ( ( h ` n ) ` x ) ) ` k ) = ( ( h ` k ) ` x ) )
124 118 123 oveq12d
 |-  ( k e. NN -> ( ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ` k ) - ( ( n e. NN |-> ( ( h ` n ) ` x ) ) ` k ) ) = ( ( ( f ` k ) ` x ) - ( ( h ` k ) ` x ) ) )
125 124 adantl
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) /\ k e. NN ) -> ( ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ` k ) - ( ( n e. NN |-> ( ( h ` n ) ` x ) ) ` k ) ) = ( ( ( f ` k ) ` x ) - ( ( h ` k ) ` x ) ) )
126 107 113 125 3eqtr4d
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( ( f oF oF - h ) ` n ) ` x ) ) ` k ) = ( ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ` k ) - ( ( n e. NN |-> ( ( h ` n ) ` x ) ) ` k ) ) )
127 126 adantlr
 |-  ( ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) /\ ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( ( f oF oF - h ) ` n ) ` x ) ) ` k ) = ( ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ` k ) - ( ( n e. NN |-> ( ( h ` n ) ` x ) ) ` k ) ) )
128 61 62 63 65 66 75 84 127 climsub
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) /\ ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) -> ( n e. NN |-> ( ( ( f oF oF - h ) ` n ) ` x ) ) ~~> ( if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) - if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) )
129 2 adantr
 |-  ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) -> F : RR --> RR )
130 129 ffvelrnda
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) -> ( F ` x ) e. RR )
131 max0sub
 |-  ( ( F ` x ) e. RR -> ( if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) - if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) = ( F ` x ) )
132 130 131 syl
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) -> ( if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) - if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) = ( F ` x ) )
133 132 adantr
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) /\ ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) -> ( if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) - if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) = ( F ` x ) )
134 128 133 breqtrd
 |-  ( ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) /\ ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) -> ( n e. NN |-> ( ( ( f oF oF - h ) ` n ) ` x ) ) ~~> ( F ` x ) )
135 134 ex
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) -> ( ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) -> ( n e. NN |-> ( ( ( f oF oF - h ) ` n ) ` x ) ) ~~> ( F ` x ) ) )
136 60 135 sylbid
 |-  ( ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) /\ x e. RR ) -> ( ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) -> ( n e. NN |-> ( ( ( f oF oF - h ) ` n ) ` x ) ) ~~> ( F ` x ) ) )
137 136 ralimdva
 |-  ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) -> ( A. x e. RR ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) -> A. x e. RR ( n e. NN |-> ( ( ( f oF oF - h ) ` n ) ` x ) ) ~~> ( F ` x ) ) )
138 ovex
 |-  ( f oF oF - h ) e. _V
139 feq1
 |-  ( g = ( f oF oF - h ) -> ( g : NN --> dom S.1 <-> ( f oF oF - h ) : NN --> dom S.1 ) )
140 fveq1
 |-  ( g = ( f oF oF - h ) -> ( g ` n ) = ( ( f oF oF - h ) ` n ) )
141 140 fveq1d
 |-  ( g = ( f oF oF - h ) -> ( ( g ` n ) ` x ) = ( ( ( f oF oF - h ) ` n ) ` x ) )
142 141 mpteq2dv
 |-  ( g = ( f oF oF - h ) -> ( n e. NN |-> ( ( g ` n ) ` x ) ) = ( n e. NN |-> ( ( ( f oF oF - h ) ` n ) ` x ) ) )
143 142 breq1d
 |-  ( g = ( f oF oF - h ) -> ( ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) <-> ( n e. NN |-> ( ( ( f oF oF - h ) ` n ) ` x ) ) ~~> ( F ` x ) ) )
144 143 ralbidv
 |-  ( g = ( f oF oF - h ) -> ( A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) <-> A. x e. RR ( n e. NN |-> ( ( ( f oF oF - h ) ` n ) ` x ) ) ~~> ( F ` x ) ) )
145 139 144 anbi12d
 |-  ( g = ( f oF oF - h ) -> ( ( g : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) <-> ( ( f oF oF - h ) : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( ( f oF oF - h ) ` n ) ` x ) ) ~~> ( F ` x ) ) ) )
146 138 145 spcev
 |-  ( ( ( f oF oF - h ) : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( ( f oF oF - h ) ` n ) ` x ) ) ~~> ( F ` x ) ) -> E. g ( g : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) )
147 41 137 146 syl6an
 |-  ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) -> ( A. x e. RR ( ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) /\ ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) -> E. g ( g : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) ) )
148 33 147 syl5bir
 |-  ( ( ph /\ ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) ) -> ( ( A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) /\ A. x e. RR ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) -> E. g ( g : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) ) )
149 148 expimpd
 |-  ( ph -> ( ( ( f : NN --> dom S.1 /\ h : NN --> dom S.1 ) /\ ( A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) /\ A. x e. RR ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) ) -> E. g ( g : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) ) )
150 32 149 syl5
 |-  ( ph -> ( ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) ) /\ ( h : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( h ` n ) /\ ( h ` n ) oR <_ ( h ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) ) -> E. g ( g : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) ) )
151 150 exlimdvv
 |-  ( ph -> ( E. f E. h ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) ) /\ ( h : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( h ` n ) /\ ( h ` n ) oR <_ ( h ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) ) -> E. g ( g : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) ) )
152 27 151 syl5bir
 |-  ( ph -> ( ( E. f ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ ( F ` y ) , ( F ` y ) , 0 ) ) ` x ) ) /\ E. h ( h : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( h ` n ) /\ ( h ` n ) oR <_ ( h ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( h ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( 0 <_ -u ( F ` y ) , -u ( F ` y ) , 0 ) ) ` x ) ) ) -> E. g ( g : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) ) )
153 15 26 152 mp2and
 |-  ( ph -> E. g ( g : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) )