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 ffvelcdmda 
 |-  ( ( 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 ffvelcdmda 
 |-  ( ( ( 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 ffvelcdmda 
 |-  ( ( ( ( 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 ffvelcdmda 
 |-  ( ( ( ( ( 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 ffvelcdmda 
 |-  ( ( ( 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 ffvelcdmda 
 |-  ( ( ( ( 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 ffvelcdmda 
 |-  ( ( ( ( ( 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 ffvelcdmda 
 |-  ( ( ( 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 ffvelcdmda 
 |-  ( ( ( 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 ffvelcdmda 
 |-  ( ( ( 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 biimtrrid 
 |-  ( ( 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 biimtrrid 
 |-  ( 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 ) ) )