Metamath Proof Explorer

Theorem pntlem3

Description: Lemma for pnt . Equation 10.6.35 in Shapiro, p. 436. (Contributed by Mario Carneiro, 8-Apr-2016) (Proof shortened by AV, 27-Sep-2020)

Ref Expression
Hypotheses pntlem3.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
pntlem3.a 
|- ( ph -> A e. RR+ )
pntlem3.A 
|- ( ph -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )
pntlem3.1 
|- T = { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t }
pntlem3.2 
|- ( ph -> C e. RR+ )
pntlem3.3 
|- ( ( ph /\ u e. T ) -> ( u - ( C x. ( u ^ 3 ) ) ) e. T )
Assertion pntlem3 
|- ( ph -> ( x e. RR+ |-> ( ( psi ` x ) / x ) ) ~~>r 1 )

Proof

Step Hyp Ref Expression
1 pntlem3.r 
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2 pntlem3.a 
 |-  ( ph -> A e. RR+ )
3 pntlem3.A 
 |-  ( ph -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )
4 pntlem3.1 
 |-  T = { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t }
5 pntlem3.2 
 |-  ( ph -> C e. RR+ )
6 pntlem3.3 
 |-  ( ( ph /\ u e. T ) -> ( u - ( C x. ( u ^ 3 ) ) ) e. T )
7 rpssre 
 |-  RR+ C_ RR
8 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
9 8 subcn 
 |-  - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
10 9 a1i 
 |-  ( ( ph /\ 0 < inf ( T , RR , < ) ) -> - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
11 ssid 
 |-  CC C_ CC
12 cncfmptid 
 |-  ( ( CC C_ CC /\ CC C_ CC ) -> ( p e. CC |-> p ) e. ( CC -cn-> CC ) )
13 11 11 12 mp2an 
 |-  ( p e. CC |-> p ) e. ( CC -cn-> CC )
14 13 a1i 
 |-  ( ( ph /\ 0 < inf ( T , RR , < ) ) -> ( p e. CC |-> p ) e. ( CC -cn-> CC ) )
15 5 adantr 
 |-  ( ( ph /\ 0 < inf ( T , RR , < ) ) -> C e. RR+ )
16 15 rpcnd 
 |-  ( ( ph /\ 0 < inf ( T , RR , < ) ) -> C e. CC )
17 11 a1i 
 |-  ( ( ph /\ 0 < inf ( T , RR , < ) ) -> CC C_ CC )
18 cncfmptc 
 |-  ( ( C e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( p e. CC |-> C ) e. ( CC -cn-> CC ) )
19 16 17 17 18 syl3anc 
 |-  ( ( ph /\ 0 < inf ( T , RR , < ) ) -> ( p e. CC |-> C ) e. ( CC -cn-> CC ) )
20 3nn0 
 |-  3 e. NN0
21 8 expcn 
 |-  ( 3 e. NN0 -> ( p e. CC |-> ( p ^ 3 ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
22 20 21 mp1i 
 |-  ( ( ph /\ 0 < inf ( T , RR , < ) ) -> ( p e. CC |-> ( p ^ 3 ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
23 8 cncfcn1 
 |-  ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) )
24 22 23 eleqtrrdi 
 |-  ( ( ph /\ 0 < inf ( T , RR , < ) ) -> ( p e. CC |-> ( p ^ 3 ) ) e. ( CC -cn-> CC ) )
25 19 24 mulcncf 
 |-  ( ( ph /\ 0 < inf ( T , RR , < ) ) -> ( p e. CC |-> ( C x. ( p ^ 3 ) ) ) e. ( CC -cn-> CC ) )
26 8 10 14 25 cncfmpt2f 
 |-  ( ( ph /\ 0 < inf ( T , RR , < ) ) -> ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) e. ( CC -cn-> CC ) )
27 4 ssrab3 
 |-  T C_ ( 0 [,] A )
28 0re 
 |-  0 e. RR
29 2 rpred 
 |-  ( ph -> A e. RR )
30 iccssre 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 [,] A ) C_ RR )
31 28 29 30 sylancr 
 |-  ( ph -> ( 0 [,] A ) C_ RR )
32 27 31 sstrid 
 |-  ( ph -> T C_ RR )
33 0xr 
 |-  0 e. RR*
34 2 rpxrd 
 |-  ( ph -> A e. RR* )
35 2 rpge0d 
 |-  ( ph -> 0 <_ A )
36 ubicc2 
 |-  ( ( 0 e. RR* /\ A e. RR* /\ 0 <_ A ) -> A e. ( 0 [,] A ) )
37 33 34 35 36 mp3an2i 
 |-  ( ph -> A e. ( 0 [,] A ) )
38 1rp 
 |-  1 e. RR+
39 fveq2 
 |-  ( x = z -> ( R ` x ) = ( R ` z ) )
40 id 
 |-  ( x = z -> x = z )
41 39 40 oveq12d 
 |-  ( x = z -> ( ( R ` x ) / x ) = ( ( R ` z ) / z ) )
42 41 fveq2d 
 |-  ( x = z -> ( abs ` ( ( R ` x ) / x ) ) = ( abs ` ( ( R ` z ) / z ) ) )
43 42 breq1d 
 |-  ( x = z -> ( ( abs ` ( ( R ` x ) / x ) ) <_ A <-> ( abs ` ( ( R ` z ) / z ) ) <_ A ) )
44 3 adantr 
 |-  ( ( ph /\ z e. ( 1 [,) +oo ) ) -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )
45 1re 
 |-  1 e. RR
46 elicopnf 
 |-  ( 1 e. RR -> ( z e. ( 1 [,) +oo ) <-> ( z e. RR /\ 1 <_ z ) ) )
47 45 46 mp1i 
 |-  ( ph -> ( z e. ( 1 [,) +oo ) <-> ( z e. RR /\ 1 <_ z ) ) )
48 47 simprbda 
 |-  ( ( ph /\ z e. ( 1 [,) +oo ) ) -> z e. RR )
49 0red 
 |-  ( ( ph /\ z e. ( 1 [,) +oo ) ) -> 0 e. RR )
50 45 a1i 
 |-  ( ( ph /\ z e. ( 1 [,) +oo ) ) -> 1 e. RR )
51 0lt1 
 |-  0 < 1
52 51 a1i 
 |-  ( ( ph /\ z e. ( 1 [,) +oo ) ) -> 0 < 1 )
53 47 simplbda 
 |-  ( ( ph /\ z e. ( 1 [,) +oo ) ) -> 1 <_ z )
54 49 50 48 52 53 ltletrd 
 |-  ( ( ph /\ z e. ( 1 [,) +oo ) ) -> 0 < z )
55 48 54 elrpd 
 |-  ( ( ph /\ z e. ( 1 [,) +oo ) ) -> z e. RR+ )
56 43 44 55 rspcdva 
 |-  ( ( ph /\ z e. ( 1 [,) +oo ) ) -> ( abs ` ( ( R ` z ) / z ) ) <_ A )
57 56 ralrimiva 
 |-  ( ph -> A. z e. ( 1 [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ A )
58 oveq1 
 |-  ( y = 1 -> ( y [,) +oo ) = ( 1 [,) +oo ) )
59 58 raleqdv 
 |-  ( y = 1 -> ( A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ A <-> A. z e. ( 1 [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ A ) )
60 59 rspcev 
 |-  ( ( 1 e. RR+ /\ A. z e. ( 1 [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ A ) -> E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ A )
61 38 57 60 sylancr 
 |-  ( ph -> E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ A )
62 breq2 
 |-  ( t = A -> ( ( abs ` ( ( R ` z ) / z ) ) <_ t <-> ( abs ` ( ( R ` z ) / z ) ) <_ A ) )
63 62 rexralbidv 
 |-  ( t = A -> ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t <-> E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ A ) )
64 63 4 elrab2 
 |-  ( A e. T <-> ( A e. ( 0 [,] A ) /\ E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ A ) )
65 37 61 64 sylanbrc 
 |-  ( ph -> A e. T )
66 65 ne0d 
 |-  ( ph -> T =/= (/) )
67 elicc2 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( t e. ( 0 [,] A ) <-> ( t e. RR /\ 0 <_ t /\ t <_ A ) ) )
68 28 29 67 sylancr 
 |-  ( ph -> ( t e. ( 0 [,] A ) <-> ( t e. RR /\ 0 <_ t /\ t <_ A ) ) )
69 68 biimpa 
 |-  ( ( ph /\ t e. ( 0 [,] A ) ) -> ( t e. RR /\ 0 <_ t /\ t <_ A ) )
70 69 simp2d 
 |-  ( ( ph /\ t e. ( 0 [,] A ) ) -> 0 <_ t )
71 70 a1d 
 |-  ( ( ph /\ t e. ( 0 [,] A ) ) -> ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> 0 <_ t ) )
72 71 ralrimiva 
 |-  ( ph -> A. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> 0 <_ t ) )
73 4 raleqi 
 |-  ( A. w e. T 0 <_ w <-> A. w e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } 0 <_ w )
74 breq2 
 |-  ( w = t -> ( 0 <_ w <-> 0 <_ t ) )
75 74 ralrab2 
 |-  ( A. w e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } 0 <_ w <-> A. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> 0 <_ t ) )
76 73 75 bitri 
 |-  ( A. w e. T 0 <_ w <-> A. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> 0 <_ t ) )
77 72 76 sylibr 
 |-  ( ph -> A. w e. T 0 <_ w )
78 breq1 
 |-  ( x = 0 -> ( x <_ w <-> 0 <_ w ) )
79 78 ralbidv 
 |-  ( x = 0 -> ( A. w e. T x <_ w <-> A. w e. T 0 <_ w ) )
80 79 rspcev 
 |-  ( ( 0 e. RR /\ A. w e. T 0 <_ w ) -> E. x e. RR A. w e. T x <_ w )
81 28 77 80 sylancr 
 |-  ( ph -> E. x e. RR A. w e. T x <_ w )
82 infrecl 
 |-  ( ( T C_ RR /\ T =/= (/) /\ E. x e. RR A. w e. T x <_ w ) -> inf ( T , RR , < ) e. RR )
83 32 66 81 82 syl3anc 
 |-  ( ph -> inf ( T , RR , < ) e. RR )
84 83 recnd 
 |-  ( ph -> inf ( T , RR , < ) e. CC )
85 84 adantr 
 |-  ( ( ph /\ 0 < inf ( T , RR , < ) ) -> inf ( T , RR , < ) e. CC )
86 elrp 
 |-  ( inf ( T , RR , < ) e. RR+ <-> ( inf ( T , RR , < ) e. RR /\ 0 < inf ( T , RR , < ) ) )
87 86 biimpri 
 |-  ( ( inf ( T , RR , < ) e. RR /\ 0 < inf ( T , RR , < ) ) -> inf ( T , RR , < ) e. RR+ )
88 83 87 sylan 
 |-  ( ( ph /\ 0 < inf ( T , RR , < ) ) -> inf ( T , RR , < ) e. RR+ )
89 3z 
 |-  3 e. ZZ
90 rpexpcl 
 |-  ( ( inf ( T , RR , < ) e. RR+ /\ 3 e. ZZ ) -> ( inf ( T , RR , < ) ^ 3 ) e. RR+ )
91 88 89 90 sylancl 
 |-  ( ( ph /\ 0 < inf ( T , RR , < ) ) -> ( inf ( T , RR , < ) ^ 3 ) e. RR+ )
92 15 91 rpmulcld 
 |-  ( ( ph /\ 0 < inf ( T , RR , < ) ) -> ( C x. ( inf ( T , RR , < ) ^ 3 ) ) e. RR+ )
93 cncfi 
 |-  ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) e. ( CC -cn-> CC ) /\ inf ( T , RR , < ) e. CC /\ ( C x. ( inf ( T , RR , < ) ^ 3 ) ) e. RR+ ) -> E. s e. RR+ A. u e. CC ( ( abs ` ( u - inf ( T , RR , < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` inf ( T , RR , < ) ) ) ) < ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) )
94 26 85 92 93 syl3anc 
 |-  ( ( ph /\ 0 < inf ( T , RR , < ) ) -> E. s e. RR+ A. u e. CC ( ( abs ` ( u - inf ( T , RR , < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` inf ( T , RR , < ) ) ) ) < ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) )
95 83 ad2antrr 
 |-  ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) -> inf ( T , RR , < ) e. RR )
96 rphalfcl 
 |-  ( s e. RR+ -> ( s / 2 ) e. RR+ )
97 96 adantl 
 |-  ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) -> ( s / 2 ) e. RR+ )
98 95 97 ltaddrpd 
 |-  ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) -> inf ( T , RR , < ) < ( inf ( T , RR , < ) + ( s / 2 ) ) )
99 97 rpred 
 |-  ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) -> ( s / 2 ) e. RR )
100 95 99 readdcld 
 |-  ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) -> ( inf ( T , RR , < ) + ( s / 2 ) ) e. RR )
101 95 100 ltnled 
 |-  ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) -> ( inf ( T , RR , < ) < ( inf ( T , RR , < ) + ( s / 2 ) ) <-> -. ( inf ( T , RR , < ) + ( s / 2 ) ) <_ inf ( T , RR , < ) ) )
102 98 101 mpbid 
 |-  ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) -> -. ( inf ( T , RR , < ) + ( s / 2 ) ) <_ inf ( T , RR , < ) )
103 ax-resscn 
 |-  RR C_ CC
104 32 103 sstrdi 
 |-  ( ph -> T C_ CC )
105 104 ad2antrr 
 |-  ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) -> T C_ CC )
106 ssralv 
 |-  ( T C_ CC -> ( A. u e. CC ( ( abs ` ( u - inf ( T , RR , < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` inf ( T , RR , < ) ) ) ) < ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) -> A. u e. T ( ( abs ` ( u - inf ( T , RR , < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` inf ( T , RR , < ) ) ) ) < ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) ) )
107 105 106 syl 
 |-  ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) -> ( A. u e. CC ( ( abs ` ( u - inf ( T , RR , < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` inf ( T , RR , < ) ) ) ) < ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) -> A. u e. T ( ( abs ` ( u - inf ( T , RR , < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` inf ( T , RR , < ) ) ) ) < ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) ) )
108 32 ad2antrr 
 |-  ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) -> T C_ RR )
109 108 sselda 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> u e. RR )
110 100 adantr 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( inf ( T , RR , < ) + ( s / 2 ) ) e. RR )
111 109 110 ltnled 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( u < ( inf ( T , RR , < ) + ( s / 2 ) ) <-> -. ( inf ( T , RR , < ) + ( s / 2 ) ) <_ u ) )
112 83 ad3antrrr 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> inf ( T , RR , < ) e. RR )
113 99 adantr 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( s / 2 ) e. RR )
114 112 113 resubcld 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( inf ( T , RR , < ) - ( s / 2 ) ) e. RR )
115 95 97 ltsubrpd 
 |-  ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) -> ( inf ( T , RR , < ) - ( s / 2 ) ) < inf ( T , RR , < ) )
116 115 adantr 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( inf ( T , RR , < ) - ( s / 2 ) ) < inf ( T , RR , < ) )
117 32 ad3antrrr 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> T C_ RR )
118 81 ad3antrrr 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> E. x e. RR A. w e. T x <_ w )
119 simpr 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> u e. T )
120 infrelb 
 |-  ( ( T C_ RR /\ E. x e. RR A. w e. T x <_ w /\ u e. T ) -> inf ( T , RR , < ) <_ u )
121 117 118 119 120 syl3anc 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> inf ( T , RR , < ) <_ u )
122 114 112 109 116 121 ltletrd 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( inf ( T , RR , < ) - ( s / 2 ) ) < u )
123 109 112 113 absdifltd 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( abs ` ( u - inf ( T , RR , < ) ) ) < ( s / 2 ) <-> ( ( inf ( T , RR , < ) - ( s / 2 ) ) < u /\ u < ( inf ( T , RR , < ) + ( s / 2 ) ) ) ) )
124 123 biimprd 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( ( inf ( T , RR , < ) - ( s / 2 ) ) < u /\ u < ( inf ( T , RR , < ) + ( s / 2 ) ) ) -> ( abs ` ( u - inf ( T , RR , < ) ) ) < ( s / 2 ) ) )
125 122 124 mpand 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( u < ( inf ( T , RR , < ) + ( s / 2 ) ) -> ( abs ` ( u - inf ( T , RR , < ) ) ) < ( s / 2 ) ) )
126 rphalflt 
 |-  ( s e. RR+ -> ( s / 2 ) < s )
127 126 ad2antlr 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( s / 2 ) < s )
128 109 112 resubcld 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( u - inf ( T , RR , < ) ) e. RR )
129 128 recnd 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( u - inf ( T , RR , < ) ) e. CC )
130 129 abscld 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( abs ` ( u - inf ( T , RR , < ) ) ) e. RR )
131 rpre 
 |-  ( s e. RR+ -> s e. RR )
132 131 ad2antlr 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> s e. RR )
133 lttr 
 |-  ( ( ( abs ` ( u - inf ( T , RR , < ) ) ) e. RR /\ ( s / 2 ) e. RR /\ s e. RR ) -> ( ( ( abs ` ( u - inf ( T , RR , < ) ) ) < ( s / 2 ) /\ ( s / 2 ) < s ) -> ( abs ` ( u - inf ( T , RR , < ) ) ) < s ) )
134 130 113 132 133 syl3anc 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( ( abs ` ( u - inf ( T , RR , < ) ) ) < ( s / 2 ) /\ ( s / 2 ) < s ) -> ( abs ` ( u - inf ( T , RR , < ) ) ) < s ) )
135 127 134 mpan2d 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( abs ` ( u - inf ( T , RR , < ) ) ) < ( s / 2 ) -> ( abs ` ( u - inf ( T , RR , < ) ) ) < s ) )
136 125 135 syld 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( u < ( inf ( T , RR , < ) + ( s / 2 ) ) -> ( abs ` ( u - inf ( T , RR , < ) ) ) < s ) )
137 111 136 sylbird 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( -. ( inf ( T , RR , < ) + ( s / 2 ) ) <_ u -> ( abs ` ( u - inf ( T , RR , < ) ) ) < s ) )
138 137 con1d 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( -. ( abs ` ( u - inf ( T , RR , < ) ) ) < s -> ( inf ( T , RR , < ) + ( s / 2 ) ) <_ u ) )
139 109 recnd 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> u e. CC )
140 id 
 |-  ( p = u -> p = u )
141 oveq1 
 |-  ( p = u -> ( p ^ 3 ) = ( u ^ 3 ) )
142 141 oveq2d 
 |-  ( p = u -> ( C x. ( p ^ 3 ) ) = ( C x. ( u ^ 3 ) ) )
143 140 142 oveq12d 
 |-  ( p = u -> ( p - ( C x. ( p ^ 3 ) ) ) = ( u - ( C x. ( u ^ 3 ) ) ) )
144 eqid 
 |-  ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) = ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) )
145 ovex 
 |-  ( u - ( C x. ( u ^ 3 ) ) ) e. _V
146 143 144 145 fvmpt 
 |-  ( u e. CC -> ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) = ( u - ( C x. ( u ^ 3 ) ) ) )
147 139 146 syl 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) = ( u - ( C x. ( u ^ 3 ) ) ) )
148 85 ad2antrr 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> inf ( T , RR , < ) e. CC )
149 id 
 |-  ( p = inf ( T , RR , < ) -> p = inf ( T , RR , < ) )
150 oveq1 
 |-  ( p = inf ( T , RR , < ) -> ( p ^ 3 ) = ( inf ( T , RR , < ) ^ 3 ) )
151 150 oveq2d 
 |-  ( p = inf ( T , RR , < ) -> ( C x. ( p ^ 3 ) ) = ( C x. ( inf ( T , RR , < ) ^ 3 ) ) )
152 149 151 oveq12d 
 |-  ( p = inf ( T , RR , < ) -> ( p - ( C x. ( p ^ 3 ) ) ) = ( inf ( T , RR , < ) - ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) )
153 ovex 
 |-  ( inf ( T , RR , < ) - ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) e. _V
154 152 144 153 fvmpt 
 |-  ( inf ( T , RR , < ) e. CC -> ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` inf ( T , RR , < ) ) = ( inf ( T , RR , < ) - ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) )
155 148 154 syl 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` inf ( T , RR , < ) ) = ( inf ( T , RR , < ) - ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) )
156 147 155 oveq12d 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` inf ( T , RR , < ) ) ) = ( ( u - ( C x. ( u ^ 3 ) ) ) - ( inf ( T , RR , < ) - ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) ) )
157 156 fveq2d 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` inf ( T , RR , < ) ) ) ) = ( abs ` ( ( u - ( C x. ( u ^ 3 ) ) ) - ( inf ( T , RR , < ) - ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) ) ) )
158 157 breq1d 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` inf ( T , RR , < ) ) ) ) < ( C x. ( inf ( T , RR , < ) ^ 3 ) ) <-> ( abs ` ( ( u - ( C x. ( u ^ 3 ) ) ) - ( inf ( T , RR , < ) - ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) ) ) < ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) )
159 5 rpred 
 |-  ( ph -> C e. RR )
160 159 ad3antrrr 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> C e. RR )
161 reexpcl 
 |-  ( ( u e. RR /\ 3 e. NN0 ) -> ( u ^ 3 ) e. RR )
162 109 20 161 sylancl 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( u ^ 3 ) e. RR )
163 160 162 remulcld 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( C x. ( u ^ 3 ) ) e. RR )
164 109 163 resubcld 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( u - ( C x. ( u ^ 3 ) ) ) e. RR )
165 20 a1i 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> 3 e. NN0 )
166 112 165 reexpcld 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( inf ( T , RR , < ) ^ 3 ) e. RR )
167 160 166 remulcld 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( C x. ( inf ( T , RR , < ) ^ 3 ) ) e. RR )
168 112 167 resubcld 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( inf ( T , RR , < ) - ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) e. RR )
169 164 168 167 absdifltd 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( abs ` ( ( u - ( C x. ( u ^ 3 ) ) ) - ( inf ( T , RR , < ) - ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) ) ) < ( C x. ( inf ( T , RR , < ) ^ 3 ) ) <-> ( ( ( inf ( T , RR , < ) - ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) - ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) < ( u - ( C x. ( u ^ 3 ) ) ) /\ ( u - ( C x. ( u ^ 3 ) ) ) < ( ( inf ( T , RR , < ) - ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) + ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) ) ) )
170 167 recnd 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( C x. ( inf ( T , RR , < ) ^ 3 ) ) e. CC )
171 148 170 npcand 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( inf ( T , RR , < ) - ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) + ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) = inf ( T , RR , < ) )
172 171 breq2d 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( u - ( C x. ( u ^ 3 ) ) ) < ( ( inf ( T , RR , < ) - ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) + ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) <-> ( u - ( C x. ( u ^ 3 ) ) ) < inf ( T , RR , < ) ) )
173 6 ad4ant14 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( u - ( C x. ( u ^ 3 ) ) ) e. T )
174 infrelb 
 |-  ( ( T C_ RR /\ E. x e. RR A. w e. T x <_ w /\ ( u - ( C x. ( u ^ 3 ) ) ) e. T ) -> inf ( T , RR , < ) <_ ( u - ( C x. ( u ^ 3 ) ) ) )
175 117 118 173 174 syl3anc 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> inf ( T , RR , < ) <_ ( u - ( C x. ( u ^ 3 ) ) ) )
176 112 164 175 lensymd 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> -. ( u - ( C x. ( u ^ 3 ) ) ) < inf ( T , RR , < ) )
177 176 pm2.21d 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( u - ( C x. ( u ^ 3 ) ) ) < inf ( T , RR , < ) -> ( inf ( T , RR , < ) + ( s / 2 ) ) <_ u ) )
178 172 177 sylbid 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( u - ( C x. ( u ^ 3 ) ) ) < ( ( inf ( T , RR , < ) - ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) + ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) -> ( inf ( T , RR , < ) + ( s / 2 ) ) <_ u ) )
179 178 adantld 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( ( ( inf ( T , RR , < ) - ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) - ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) < ( u - ( C x. ( u ^ 3 ) ) ) /\ ( u - ( C x. ( u ^ 3 ) ) ) < ( ( inf ( T , RR , < ) - ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) + ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) ) -> ( inf ( T , RR , < ) + ( s / 2 ) ) <_ u ) )
180 169 179 sylbid 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( abs ` ( ( u - ( C x. ( u ^ 3 ) ) ) - ( inf ( T , RR , < ) - ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) ) ) < ( C x. ( inf ( T , RR , < ) ^ 3 ) ) -> ( inf ( T , RR , < ) + ( s / 2 ) ) <_ u ) )
181 158 180 sylbid 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` inf ( T , RR , < ) ) ) ) < ( C x. ( inf ( T , RR , < ) ^ 3 ) ) -> ( inf ( T , RR , < ) + ( s / 2 ) ) <_ u ) )
182 138 181 jad 
 |-  ( ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( ( abs ` ( u - inf ( T , RR , < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` inf ( T , RR , < ) ) ) ) < ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) -> ( inf ( T , RR , < ) + ( s / 2 ) ) <_ u ) )
183 182 ralimdva 
 |-  ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) -> ( A. u e. T ( ( abs ` ( u - inf ( T , RR , < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` inf ( T , RR , < ) ) ) ) < ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) -> A. u e. T ( inf ( T , RR , < ) + ( s / 2 ) ) <_ u ) )
184 66 ad2antrr 
 |-  ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) -> T =/= (/) )
185 81 ad2antrr 
 |-  ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) -> E. x e. RR A. w e. T x <_ w )
186 infregelb 
 |-  ( ( ( T C_ RR /\ T =/= (/) /\ E. x e. RR A. w e. T x <_ w ) /\ ( inf ( T , RR , < ) + ( s / 2 ) ) e. RR ) -> ( ( inf ( T , RR , < ) + ( s / 2 ) ) <_ inf ( T , RR , < ) <-> A. u e. T ( inf ( T , RR , < ) + ( s / 2 ) ) <_ u ) )
187 108 184 185 100 186 syl31anc 
 |-  ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) -> ( ( inf ( T , RR , < ) + ( s / 2 ) ) <_ inf ( T , RR , < ) <-> A. u e. T ( inf ( T , RR , < ) + ( s / 2 ) ) <_ u ) )
188 183 187 sylibrd 
 |-  ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) -> ( A. u e. T ( ( abs ` ( u - inf ( T , RR , < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` inf ( T , RR , < ) ) ) ) < ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) -> ( inf ( T , RR , < ) + ( s / 2 ) ) <_ inf ( T , RR , < ) ) )
189 107 188 syld 
 |-  ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) -> ( A. u e. CC ( ( abs ` ( u - inf ( T , RR , < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` inf ( T , RR , < ) ) ) ) < ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) -> ( inf ( T , RR , < ) + ( s / 2 ) ) <_ inf ( T , RR , < ) ) )
190 102 189 mtod 
 |-  ( ( ( ph /\ 0 < inf ( T , RR , < ) ) /\ s e. RR+ ) -> -. A. u e. CC ( ( abs ` ( u - inf ( T , RR , < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` inf ( T , RR , < ) ) ) ) < ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) )
191 190 nrexdv 
 |-  ( ( ph /\ 0 < inf ( T , RR , < ) ) -> -. E. s e. RR+ A. u e. CC ( ( abs ` ( u - inf ( T , RR , < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` inf ( T , RR , < ) ) ) ) < ( C x. ( inf ( T , RR , < ) ^ 3 ) ) ) )
192 94 191 pm2.65da 
 |-  ( ph -> -. 0 < inf ( T , RR , < ) )
193 192 adantr 
 |-  ( ( ph /\ s e. RR+ ) -> -. 0 < inf ( T , RR , < ) )
194 32 adantr 
 |-  ( ( ph /\ s e. RR+ ) -> T C_ RR )
195 66 adantr 
 |-  ( ( ph /\ s e. RR+ ) -> T =/= (/) )
196 81 adantr 
 |-  ( ( ph /\ s e. RR+ ) -> E. x e. RR A. w e. T x <_ w )
197 131 adantl 
 |-  ( ( ph /\ s e. RR+ ) -> s e. RR )
198 infregelb 
 |-  ( ( ( T C_ RR /\ T =/= (/) /\ E. x e. RR A. w e. T x <_ w ) /\ s e. RR ) -> ( s <_ inf ( T , RR , < ) <-> A. w e. T s <_ w ) )
199 194 195 196 197 198 syl31anc 
 |-  ( ( ph /\ s e. RR+ ) -> ( s <_ inf ( T , RR , < ) <-> A. w e. T s <_ w ) )
200 4 raleqi 
 |-  ( A. w e. T s <_ w <-> A. w e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } s <_ w )
201 breq2 
 |-  ( w = t -> ( s <_ w <-> s <_ t ) )
202 201 ralrab2 
 |-  ( A. w e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } s <_ w <-> A. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> s <_ t ) )
203 200 202 bitri 
 |-  ( A. w e. T s <_ w <-> A. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> s <_ t ) )
204 199 203 bitrdi 
 |-  ( ( ph /\ s e. RR+ ) -> ( s <_ inf ( T , RR , < ) <-> A. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> s <_ t ) ) )
205 rpgt0 
 |-  ( s e. RR+ -> 0 < s )
206 205 adantl 
 |-  ( ( ph /\ s e. RR+ ) -> 0 < s )
207 83 adantr 
 |-  ( ( ph /\ s e. RR+ ) -> inf ( T , RR , < ) e. RR )
208 ltletr 
 |-  ( ( 0 e. RR /\ s e. RR /\ inf ( T , RR , < ) e. RR ) -> ( ( 0 < s /\ s <_ inf ( T , RR , < ) ) -> 0 < inf ( T , RR , < ) ) )
209 28 197 207 208 mp3an2i 
 |-  ( ( ph /\ s e. RR+ ) -> ( ( 0 < s /\ s <_ inf ( T , RR , < ) ) -> 0 < inf ( T , RR , < ) ) )
210 206 209 mpand 
 |-  ( ( ph /\ s e. RR+ ) -> ( s <_ inf ( T , RR , < ) -> 0 < inf ( T , RR , < ) ) )
211 204 210 sylbird 
 |-  ( ( ph /\ s e. RR+ ) -> ( A. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> s <_ t ) -> 0 < inf ( T , RR , < ) ) )
212 193 211 mtod 
 |-  ( ( ph /\ s e. RR+ ) -> -. A. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> s <_ t ) )
213 rexanali 
 |-  ( E. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t /\ -. s <_ t ) <-> -. A. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> s <_ t ) )
214 212 213 sylibr 
 |-  ( ( ph /\ s e. RR+ ) -> E. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t /\ -. s <_ t ) )
215 fveq2 
 |-  ( z = x -> ( R ` z ) = ( R ` x ) )
216 id 
 |-  ( z = x -> z = x )
217 215 216 oveq12d 
 |-  ( z = x -> ( ( R ` z ) / z ) = ( ( R ` x ) / x ) )
218 217 fveq2d 
 |-  ( z = x -> ( abs ` ( ( R ` z ) / z ) ) = ( abs ` ( ( R ` x ) / x ) ) )
219 218 breq1d 
 |-  ( z = x -> ( ( abs ` ( ( R ` z ) / z ) ) <_ t <-> ( abs ` ( ( R ` x ) / x ) ) <_ t ) )
220 219 cbvralvw 
 |-  ( A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t <-> A. x e. ( y [,) +oo ) ( abs ` ( ( R ` x ) / x ) ) <_ t )
221 rpre 
 |-  ( x e. RR+ -> x e. RR )
222 221 ad2antll 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> x e. RR )
223 simprl 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> y <_ x )
224 simplr 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> y e. RR+ )
225 224 rpred 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> y e. RR )
226 elicopnf 
 |-  ( y e. RR -> ( x e. ( y [,) +oo ) <-> ( x e. RR /\ y <_ x ) ) )
227 225 226 syl 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( x e. ( y [,) +oo ) <-> ( x e. RR /\ y <_ x ) ) )
228 222 223 227 mpbir2and 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> x e. ( y [,) +oo ) )
229 1 pntrval 
 |-  ( x e. RR+ -> ( R ` x ) = ( ( psi ` x ) - x ) )
230 229 ad2antll 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( R ` x ) = ( ( psi ` x ) - x ) )
231 230 oveq1d 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( R ` x ) / x ) = ( ( ( psi ` x ) - x ) / x ) )
232 chpcl 
 |-  ( x e. RR -> ( psi ` x ) e. RR )
233 222 232 syl 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( psi ` x ) e. RR )
234 233 recnd 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( psi ` x ) e. CC )
235 rpcn 
 |-  ( x e. RR+ -> x e. CC )
236 235 ad2antll 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> x e. CC )
237 rpne0 
 |-  ( x e. RR+ -> x =/= 0 )
238 237 ad2antll 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> x =/= 0 )
239 234 236 236 238 divsubdird 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( ( psi ` x ) - x ) / x ) = ( ( ( psi ` x ) / x ) - ( x / x ) ) )
240 236 238 dividd 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( x / x ) = 1 )
241 240 oveq2d 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( ( psi ` x ) / x ) - ( x / x ) ) = ( ( ( psi ` x ) / x ) - 1 ) )
242 231 239 241 3eqtrrd 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( ( psi ` x ) / x ) - 1 ) = ( ( R ` x ) / x ) )
243 242 fveq2d 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) = ( abs ` ( ( R ` x ) / x ) ) )
244 243 breq1d 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) <_ t <-> ( abs ` ( ( R ` x ) / x ) ) <_ t ) )
245 simprr 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) -> -. s <_ t )
246 245 ad2antrr 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> -. s <_ t )
247 31 ad2antrr 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) -> ( 0 [,] A ) C_ RR )
248 247 ad2antrr 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( 0 [,] A ) C_ RR )
249 simplrl 
 |-  ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) -> t e. ( 0 [,] A ) )
250 249 adantr 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> t e. ( 0 [,] A ) )
251 248 250 sseldd 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> t e. RR )
252 simp-4r 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> s e. RR+ )
253 252 rpred 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> s e. RR )
254 251 253 ltnled 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( t < s <-> -. s <_ t ) )
255 246 254 mpbird 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> t < s )
256 221 232 syl 
 |-  ( x e. RR+ -> ( psi ` x ) e. RR )
257 rerpdivcl 
 |-  ( ( ( psi ` x ) e. RR /\ x e. RR+ ) -> ( ( psi ` x ) / x ) e. RR )
258 256 257 mpancom 
 |-  ( x e. RR+ -> ( ( psi ` x ) / x ) e. RR )
259 258 ad2antll 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( psi ` x ) / x ) e. RR )
260 resubcl 
 |-  ( ( ( ( psi ` x ) / x ) e. RR /\ 1 e. RR ) -> ( ( ( psi ` x ) / x ) - 1 ) e. RR )
261 259 45 260 sylancl 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( ( psi ` x ) / x ) - 1 ) e. RR )
262 261 recnd 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( ( psi ` x ) / x ) - 1 ) e. CC )
263 262 abscld 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) e. RR )
264 lelttr 
 |-  ( ( ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) e. RR /\ t e. RR /\ s e. RR ) -> ( ( ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) <_ t /\ t < s ) -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) < s ) )
265 263 251 253 264 syl3anc 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) <_ t /\ t < s ) -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) < s ) )
266 255 265 mpan2d 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) <_ t -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) < s ) )
267 244 266 sylbird 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( abs ` ( ( R ` x ) / x ) ) <_ t -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) < s ) )
268 228 267 embantd 
 |-  ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( x e. ( y [,) +oo ) -> ( abs ` ( ( R ` x ) / x ) ) <_ t ) -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) < s ) )
269 268 exp32 
 |-  ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) -> ( y <_ x -> ( x e. RR+ -> ( ( x e. ( y [,) +oo ) -> ( abs ` ( ( R ` x ) / x ) ) <_ t ) -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) < s ) ) ) )
270 269 com24 
 |-  ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) -> ( ( x e. ( y [,) +oo ) -> ( abs ` ( ( R ` x ) / x ) ) <_ t ) -> ( x e. RR+ -> ( y <_ x -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) < s ) ) ) )
271 270 ralimdv2 
 |-  ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) -> ( A. x e. ( y [,) +oo ) ( abs ` ( ( R ` x ) / x ) ) <_ t -> A. x e. RR+ ( y <_ x -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) < s ) ) )
272 220 271 syl5bi 
 |-  ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) -> ( A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> A. x e. RR+ ( y <_ x -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) < s ) ) )
273 272 reximdva 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) -> ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> E. y e. RR+ A. x e. RR+ ( y <_ x -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) < s ) ) )
274 273 anassrs 
 |-  ( ( ( ( ph /\ s e. RR+ ) /\ t e. ( 0 [,] A ) ) /\ -. s <_ t ) -> ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> E. y e. RR+ A. x e. RR+ ( y <_ x -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) < s ) ) )
275 274 impancom 
 |-  ( ( ( ( ph /\ s e. RR+ ) /\ t e. ( 0 [,] A ) ) /\ E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t ) -> ( -. s <_ t -> E. y e. RR+ A. x e. RR+ ( y <_ x -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) < s ) ) )
276 275 expimpd 
 |-  ( ( ( ph /\ s e. RR+ ) /\ t e. ( 0 [,] A ) ) -> ( ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t /\ -. s <_ t ) -> E. y e. RR+ A. x e. RR+ ( y <_ x -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) < s ) ) )
277 276 rexlimdva 
 |-  ( ( ph /\ s e. RR+ ) -> ( E. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t /\ -. s <_ t ) -> E. y e. RR+ A. x e. RR+ ( y <_ x -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) < s ) ) )
278 214 277 mpd 
 |-  ( ( ph /\ s e. RR+ ) -> E. y e. RR+ A. x e. RR+ ( y <_ x -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) < s ) )
279 ssrexv 
 |-  ( RR+ C_ RR -> ( E. y e. RR+ A. x e. RR+ ( y <_ x -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) < s ) -> E. y e. RR A. x e. RR+ ( y <_ x -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) < s ) ) )
280 7 278 279 mpsyl 
 |-  ( ( ph /\ s e. RR+ ) -> E. y e. RR A. x e. RR+ ( y <_ x -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) < s ) )
281 280 ralrimiva 
 |-  ( ph -> A. s e. RR+ E. y e. RR A. x e. RR+ ( y <_ x -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) < s ) )
282 258 recnd 
 |-  ( x e. RR+ -> ( ( psi ` x ) / x ) e. CC )
283 282 rgen 
 |-  A. x e. RR+ ( ( psi ` x ) / x ) e. CC
284 283 a1i 
 |-  ( ph -> A. x e. RR+ ( ( psi ` x ) / x ) e. CC )
285 7 a1i 
 |-  ( ph -> RR+ C_ RR )
286 1cnd 
 |-  ( ph -> 1 e. CC )
287 284 285 286 rlim2 
 |-  ( ph -> ( ( x e. RR+ |-> ( ( psi ` x ) / x ) ) ~~>r 1 <-> A. s e. RR+ E. y e. RR A. x e. RR+ ( y <_ x -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) < s ) ) )
288 281 287 mpbird 
 |-  ( ph -> ( x e. RR+ |-> ( ( psi ` x ) / x ) ) ~~>r 1 )