Metamath Proof Explorer

Theorem pntleml

Description: Lemma for pnt . Equation 10.6.35 in Shapiro, p. 436. (Contributed by Mario Carneiro, 14-Apr-2016)

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 )
pntlemp.b 
|- ( ph -> B e. RR+ )
pntlemp.l 
|- ( ph -> L e. ( 0 (,) 1 ) )
pntlemp.d 
|- D = ( A + 1 )
pntlemp.f 
|- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
pntlemp.K 
|- ( ph -> A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( B / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( L x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) )
Assertion pntleml 
|- ( 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 pntlemp.b 
 |-  ( ph -> B e. RR+ )
5 pntlemp.l 
 |-  ( ph -> L e. ( 0 (,) 1 ) )
6 pntlemp.d 
 |-  D = ( A + 1 )
7 pntlemp.f 
 |-  F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
8 pntlemp.K 
 |-  ( ph -> A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( B / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( L x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) )
9 eqid 
 |-  { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } = { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t }
10 1 2 4 5 6 7 pntlemd 
 |-  ( ph -> ( L e. RR+ /\ D e. RR+ /\ F e. RR+ ) )
11 10 simp3d 
 |-  ( ph -> F e. RR+ )
12 0m0e0 
 |-  ( 0 - 0 ) = 0
13 simpr 
 |-  ( ( ( ph /\ r e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } ) /\ r = 0 ) -> r = 0 )
14 13 oveq1d 
 |-  ( ( ( ph /\ r e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } ) /\ r = 0 ) -> ( r ^ 3 ) = ( 0 ^ 3 ) )
15 3nn 
 |-  3 e. NN
16 0exp 
 |-  ( 3 e. NN -> ( 0 ^ 3 ) = 0 )
17 15 16 ax-mp 
 |-  ( 0 ^ 3 ) = 0
18 14 17 eqtrdi 
 |-  ( ( ( ph /\ r e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } ) /\ r = 0 ) -> ( r ^ 3 ) = 0 )
19 18 oveq2d 
 |-  ( ( ( ph /\ r e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } ) /\ r = 0 ) -> ( F x. ( r ^ 3 ) ) = ( F x. 0 ) )
20 11 rpcnd 
 |-  ( ph -> F e. CC )
21 20 mul01d 
 |-  ( ph -> ( F x. 0 ) = 0 )
22 21 ad2antrr 
 |-  ( ( ( ph /\ r e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } ) /\ r = 0 ) -> ( F x. 0 ) = 0 )
23 19 22 eqtrd 
 |-  ( ( ( ph /\ r e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } ) /\ r = 0 ) -> ( F x. ( r ^ 3 ) ) = 0 )
24 13 23 oveq12d 
 |-  ( ( ( ph /\ r e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } ) /\ r = 0 ) -> ( r - ( F x. ( r ^ 3 ) ) ) = ( 0 - 0 ) )
25 12 24 13 3eqtr4a 
 |-  ( ( ( ph /\ r e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } ) /\ r = 0 ) -> ( r - ( F x. ( r ^ 3 ) ) ) = r )
26 simplr 
 |-  ( ( ( ph /\ r e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } ) /\ r = 0 ) -> r e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } )
27 25 26 eqeltrd 
 |-  ( ( ( ph /\ r e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } ) /\ r = 0 ) -> ( r - ( F x. ( r ^ 3 ) ) ) e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } )
28 oveq1 
 |-  ( y = s -> ( y [,) +oo ) = ( s [,) +oo ) )
29 28 raleqdv 
 |-  ( y = s -> ( A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r <-> A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) )
30 29 cbvrexvw 
 |-  ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r <-> E. s e. RR+ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r )
31 simplrr 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> r e. ( 0 [,] A ) )
32 0re 
 |-  0 e. RR
33 2 ad2antrr 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> A e. RR+ )
34 33 rpred 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> A e. RR )
35 elicc2 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( r e. ( 0 [,] A ) <-> ( r e. RR /\ 0 <_ r /\ r <_ A ) ) )
36 32 34 35 sylancr 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> ( r e. ( 0 [,] A ) <-> ( r e. RR /\ 0 <_ r /\ r <_ A ) ) )
37 31 36 mpbid 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> ( r e. RR /\ 0 <_ r /\ r <_ A ) )
38 37 simp1d 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> r e. RR )
39 11 ad2antrr 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> F e. RR+ )
40 37 simp2d 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> 0 <_ r )
41 simplrl 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> r =/= 0 )
42 38 40 41 ne0gt0d 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> 0 < r )
43 38 42 elrpd 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> r e. RR+ )
44 3z 
 |-  3 e. ZZ
45 rpexpcl 
 |-  ( ( r e. RR+ /\ 3 e. ZZ ) -> ( r ^ 3 ) e. RR+ )
46 43 44 45 sylancl 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> ( r ^ 3 ) e. RR+ )
47 39 46 rpmulcld 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> ( F x. ( r ^ 3 ) ) e. RR+ )
48 47 rpred 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> ( F x. ( r ^ 3 ) ) e. RR )
49 38 48 resubcld 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> ( r - ( F x. ( r ^ 3 ) ) ) e. RR )
50 3 ad2antrr 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )
51 4 ad2antrr 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> B e. RR+ )
52 5 ad2antrr 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> L e. ( 0 (,) 1 ) )
53 8 ad2antrr 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( B / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( L x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) )
54 37 simp3d 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> r <_ A )
55 eqid 
 |-  ( r / D ) = ( r / D )
56 eqid 
 |-  ( exp ` ( B / ( r / D ) ) ) = ( exp ` ( B / ( r / D ) ) )
57 simprl 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> s e. RR+ )
58 1rp 
 |-  1 e. RR+
59 rpaddcl 
 |-  ( ( s e. RR+ /\ 1 e. RR+ ) -> ( s + 1 ) e. RR+ )
60 57 58 59 sylancl 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> ( s + 1 ) e. RR+ )
61 57 rpge0d 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> 0 <_ s )
62 1re 
 |-  1 e. RR
63 57 rpred 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> s e. RR )
64 addge02 
 |-  ( ( 1 e. RR /\ s e. RR ) -> ( 0 <_ s <-> 1 <_ ( s + 1 ) ) )
65 62 63 64 sylancr 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> ( 0 <_ s <-> 1 <_ ( s + 1 ) ) )
66 61 65 mpbid 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> 1 <_ ( s + 1 ) )
67 60 66 jca 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> ( ( s + 1 ) e. RR+ /\ 1 <_ ( s + 1 ) ) )
68 57 rpxrd 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> s e. RR* )
69 63 lep1d 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> s <_ ( s + 1 ) )
70 df-ico 
 |-  [,) = ( t e. RR* , r e. RR* |-> { w e. RR* | ( t <_ w /\ w < r ) } )
71 xrletr 
 |-  ( ( s e. RR* /\ ( s + 1 ) e. RR* /\ v e. RR* ) -> ( ( s <_ ( s + 1 ) /\ ( s + 1 ) <_ v ) -> s <_ v ) )
72 70 70 71 ixxss1 
 |-  ( ( s e. RR* /\ s <_ ( s + 1 ) ) -> ( ( s + 1 ) [,) +oo ) C_ ( s [,) +oo ) )
73 68 69 72 syl2anc 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> ( ( s + 1 ) [,) +oo ) C_ ( s [,) +oo ) )
74 simprr 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r )
75 ssralv 
 |-  ( ( ( s + 1 ) [,) +oo ) C_ ( s [,) +oo ) -> ( A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r -> A. z e. ( ( s + 1 ) [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) )
76 73 74 75 sylc 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> A. z e. ( ( s + 1 ) [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r )
77 1 33 50 51 52 6 7 53 43 54 55 56 67 76 pntlemp 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> E. w e. RR+ A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) )
78 rpre 
 |-  ( w e. RR+ -> w e. RR )
79 78 adantl 
 |-  ( ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) /\ w e. RR+ ) -> w e. RR )
80 79 leidd 
 |-  ( ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) /\ w e. RR+ ) -> w <_ w )
81 elicopnf 
 |-  ( w e. RR -> ( w e. ( w [,) +oo ) <-> ( w e. RR /\ w <_ w ) ) )
82 79 81 syl 
 |-  ( ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) /\ w e. RR+ ) -> ( w e. ( w [,) +oo ) <-> ( w e. RR /\ w <_ w ) ) )
83 79 80 82 mpbir2and 
 |-  ( ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) /\ w e. RR+ ) -> w e. ( w [,) +oo ) )
84 fveq2 
 |-  ( v = w -> ( R ` v ) = ( R ` w ) )
85 id 
 |-  ( v = w -> v = w )
86 84 85 oveq12d 
 |-  ( v = w -> ( ( R ` v ) / v ) = ( ( R ` w ) / w ) )
87 86 fveq2d 
 |-  ( v = w -> ( abs ` ( ( R ` v ) / v ) ) = ( abs ` ( ( R ` w ) / w ) ) )
88 87 breq1d 
 |-  ( v = w -> ( ( abs ` ( ( R ` v ) / v ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) <-> ( abs ` ( ( R ` w ) / w ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) ) )
89 88 rspcv 
 |-  ( w e. ( w [,) +oo ) -> ( A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) -> ( abs ` ( ( R ` w ) / w ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) ) )
90 83 89 syl 
 |-  ( ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) /\ w e. RR+ ) -> ( A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) -> ( abs ` ( ( R ` w ) / w ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) ) )
91 1 pntrf 
 |-  R : RR+ --> RR
92 91 ffvelcdmi 
 |-  ( w e. RR+ -> ( R ` w ) e. RR )
93 rerpdivcl 
 |-  ( ( ( R ` w ) e. RR /\ w e. RR+ ) -> ( ( R ` w ) / w ) e. RR )
94 92 93 mpancom 
 |-  ( w e. RR+ -> ( ( R ` w ) / w ) e. RR )
95 94 adantl 
 |-  ( ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) /\ w e. RR+ ) -> ( ( R ` w ) / w ) e. RR )
96 95 recnd 
 |-  ( ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) /\ w e. RR+ ) -> ( ( R ` w ) / w ) e. CC )
97 96 absge0d 
 |-  ( ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) /\ w e. RR+ ) -> 0 <_ ( abs ` ( ( R ` w ) / w ) ) )
98 96 abscld 
 |-  ( ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) /\ w e. RR+ ) -> ( abs ` ( ( R ` w ) / w ) ) e. RR )
99 49 adantr 
 |-  ( ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) /\ w e. RR+ ) -> ( r - ( F x. ( r ^ 3 ) ) ) e. RR )
100 letr 
 |-  ( ( 0 e. RR /\ ( abs ` ( ( R ` w ) / w ) ) e. RR /\ ( r - ( F x. ( r ^ 3 ) ) ) e. RR ) -> ( ( 0 <_ ( abs ` ( ( R ` w ) / w ) ) /\ ( abs ` ( ( R ` w ) / w ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) ) -> 0 <_ ( r - ( F x. ( r ^ 3 ) ) ) ) )
101 32 98 99 100 mp3an2i 
 |-  ( ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) /\ w e. RR+ ) -> ( ( 0 <_ ( abs ` ( ( R ` w ) / w ) ) /\ ( abs ` ( ( R ` w ) / w ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) ) -> 0 <_ ( r - ( F x. ( r ^ 3 ) ) ) ) )
102 97 101 mpand 
 |-  ( ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) /\ w e. RR+ ) -> ( ( abs ` ( ( R ` w ) / w ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) -> 0 <_ ( r - ( F x. ( r ^ 3 ) ) ) ) )
103 90 102 syld 
 |-  ( ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) /\ w e. RR+ ) -> ( A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) -> 0 <_ ( r - ( F x. ( r ^ 3 ) ) ) ) )
104 103 rexlimdva 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> ( E. w e. RR+ A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) -> 0 <_ ( r - ( F x. ( r ^ 3 ) ) ) ) )
105 77 104 mpd 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> 0 <_ ( r - ( F x. ( r ^ 3 ) ) ) )
106 47 rpge0d 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> 0 <_ ( F x. ( r ^ 3 ) ) )
107 38 48 subge02d 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> ( 0 <_ ( F x. ( r ^ 3 ) ) <-> ( r - ( F x. ( r ^ 3 ) ) ) <_ r ) )
108 106 107 mpbid 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> ( r - ( F x. ( r ^ 3 ) ) ) <_ r )
109 49 38 34 108 54 letrd 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> ( r - ( F x. ( r ^ 3 ) ) ) <_ A )
110 elicc2 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( ( r - ( F x. ( r ^ 3 ) ) ) e. ( 0 [,] A ) <-> ( ( r - ( F x. ( r ^ 3 ) ) ) e. RR /\ 0 <_ ( r - ( F x. ( r ^ 3 ) ) ) /\ ( r - ( F x. ( r ^ 3 ) ) ) <_ A ) ) )
111 32 34 110 sylancr 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> ( ( r - ( F x. ( r ^ 3 ) ) ) e. ( 0 [,] A ) <-> ( ( r - ( F x. ( r ^ 3 ) ) ) e. RR /\ 0 <_ ( r - ( F x. ( r ^ 3 ) ) ) /\ ( r - ( F x. ( r ^ 3 ) ) ) <_ A ) ) )
112 49 105 109 111 mpbir3and 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> ( r - ( F x. ( r ^ 3 ) ) ) e. ( 0 [,] A ) )
113 112 77 jca 
 |-  ( ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) /\ ( s e. RR+ /\ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) ) -> ( ( r - ( F x. ( r ^ 3 ) ) ) e. ( 0 [,] A ) /\ E. w e. RR+ A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) ) )
114 113 rexlimdvaa 
 |-  ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) -> ( E. s e. RR+ A. z e. ( s [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r -> ( ( r - ( F x. ( r ^ 3 ) ) ) e. ( 0 [,] A ) /\ E. w e. RR+ A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) ) ) )
115 30 114 biimtrid 
 |-  ( ( ph /\ ( r =/= 0 /\ r e. ( 0 [,] A ) ) ) -> ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r -> ( ( r - ( F x. ( r ^ 3 ) ) ) e. ( 0 [,] A ) /\ E. w e. RR+ A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) ) ) )
116 115 anassrs 
 |-  ( ( ( ph /\ r =/= 0 ) /\ r e. ( 0 [,] A ) ) -> ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r -> ( ( r - ( F x. ( r ^ 3 ) ) ) e. ( 0 [,] A ) /\ E. w e. RR+ A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) ) ) )
117 116 expimpd 
 |-  ( ( ph /\ r =/= 0 ) -> ( ( r e. ( 0 [,] A ) /\ E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) -> ( ( r - ( F x. ( r ^ 3 ) ) ) e. ( 0 [,] A ) /\ E. w e. RR+ A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) ) ) )
118 breq2 
 |-  ( t = r -> ( ( abs ` ( ( R ` z ) / z ) ) <_ t <-> ( abs ` ( ( R ` z ) / z ) ) <_ r ) )
119 118 rexralbidv 
 |-  ( t = r -> ( 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 ) ) <_ r ) )
120 119 elrab 
 |-  ( r e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } <-> ( r e. ( 0 [,] A ) /\ E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ r ) )
121 breq2 
 |-  ( t = ( r - ( F x. ( r ^ 3 ) ) ) -> ( ( abs ` ( ( R ` z ) / z ) ) <_ t <-> ( abs ` ( ( R ` z ) / z ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) ) )
122 121 rexralbidv 
 |-  ( t = ( r - ( F x. ( r ^ 3 ) ) ) -> ( 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 ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) ) )
123 fveq2 
 |-  ( v = z -> ( R ` v ) = ( R ` z ) )
124 id 
 |-  ( v = z -> v = z )
125 123 124 oveq12d 
 |-  ( v = z -> ( ( R ` v ) / v ) = ( ( R ` z ) / z ) )
126 125 fveq2d 
 |-  ( v = z -> ( abs ` ( ( R ` v ) / v ) ) = ( abs ` ( ( R ` z ) / z ) ) )
127 126 breq1d 
 |-  ( v = z -> ( ( abs ` ( ( R ` v ) / v ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) <-> ( abs ` ( ( R ` z ) / z ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) ) )
128 127 cbvralvw 
 |-  ( A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) <-> A. z e. ( w [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) )
129 oveq1 
 |-  ( w = y -> ( w [,) +oo ) = ( y [,) +oo ) )
130 129 raleqdv 
 |-  ( w = y -> ( A. z e. ( w [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) <-> A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) ) )
131 128 130 bitrid 
 |-  ( w = y -> ( A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) <-> A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) ) )
132 131 cbvrexvw 
 |-  ( E. w e. RR+ A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) <-> E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) )
133 122 132 bitr4di 
 |-  ( t = ( r - ( F x. ( r ^ 3 ) ) ) -> ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t <-> E. w e. RR+ A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) ) )
134 133 elrab 
 |-  ( ( r - ( F x. ( r ^ 3 ) ) ) e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } <-> ( ( r - ( F x. ( r ^ 3 ) ) ) e. ( 0 [,] A ) /\ E. w e. RR+ A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( r - ( F x. ( r ^ 3 ) ) ) ) )
135 117 120 134 3imtr4g 
 |-  ( ( ph /\ r =/= 0 ) -> ( r e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } -> ( r - ( F x. ( r ^ 3 ) ) ) e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } ) )
136 135 imp 
 |-  ( ( ( ph /\ r =/= 0 ) /\ r e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } ) -> ( r - ( F x. ( r ^ 3 ) ) ) e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } )
137 136 an32s 
 |-  ( ( ( ph /\ r e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } ) /\ r =/= 0 ) -> ( r - ( F x. ( r ^ 3 ) ) ) e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } )
138 27 137 pm2.61dane 
 |-  ( ( ph /\ r e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } ) -> ( r - ( F x. ( r ^ 3 ) ) ) e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } )
139 1 2 3 9 11 138 pntlem3 
 |-  ( ph -> ( x e. RR+ |-> ( ( psi ` x ) / x ) ) ~~>r 1 )