Metamath Proof Explorer


Theorem pntlemd

Description: Lemma for pnt . Closure for the constants used in the proof. For comparison with Equation 10.6.27 of Shapiro, p. 434, A is C^*, B is c_1, L is λ, D is c_2, and F is c_3. (Contributed by Mario Carneiro, 13-Apr-2016)

Ref Expression
Hypotheses pntlem1.r
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
pntlem1.a
|- ( ph -> A e. RR+ )
pntlem1.b
|- ( ph -> B e. RR+ )
pntlem1.l
|- ( ph -> L e. ( 0 (,) 1 ) )
pntlem1.d
|- D = ( A + 1 )
pntlem1.f
|- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
Assertion pntlemd
|- ( ph -> ( L e. RR+ /\ D e. RR+ /\ F e. RR+ ) )

Proof

Step Hyp Ref Expression
1 pntlem1.r
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2 pntlem1.a
 |-  ( ph -> A e. RR+ )
3 pntlem1.b
 |-  ( ph -> B e. RR+ )
4 pntlem1.l
 |-  ( ph -> L e. ( 0 (,) 1 ) )
5 pntlem1.d
 |-  D = ( A + 1 )
6 pntlem1.f
 |-  F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
7 ioossre
 |-  ( 0 (,) 1 ) C_ RR
8 7 4 sselid
 |-  ( ph -> L e. RR )
9 eliooord
 |-  ( L e. ( 0 (,) 1 ) -> ( 0 < L /\ L < 1 ) )
10 4 9 syl
 |-  ( ph -> ( 0 < L /\ L < 1 ) )
11 10 simpld
 |-  ( ph -> 0 < L )
12 8 11 elrpd
 |-  ( ph -> L e. RR+ )
13 1rp
 |-  1 e. RR+
14 rpaddcl
 |-  ( ( A e. RR+ /\ 1 e. RR+ ) -> ( A + 1 ) e. RR+ )
15 2 13 14 sylancl
 |-  ( ph -> ( A + 1 ) e. RR+ )
16 5 15 eqeltrid
 |-  ( ph -> D e. RR+ )
17 1re
 |-  1 e. RR
18 ltaddrp
 |-  ( ( 1 e. RR /\ A e. RR+ ) -> 1 < ( 1 + A ) )
19 17 2 18 sylancr
 |-  ( ph -> 1 < ( 1 + A ) )
20 2 rpcnd
 |-  ( ph -> A e. CC )
21 ax-1cn
 |-  1 e. CC
22 addcom
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( A + 1 ) = ( 1 + A ) )
23 20 21 22 sylancl
 |-  ( ph -> ( A + 1 ) = ( 1 + A ) )
24 5 23 syl5eq
 |-  ( ph -> D = ( 1 + A ) )
25 19 24 breqtrrd
 |-  ( ph -> 1 < D )
26 16 recgt1d
 |-  ( ph -> ( 1 < D <-> ( 1 / D ) < 1 ) )
27 25 26 mpbid
 |-  ( ph -> ( 1 / D ) < 1 )
28 16 rprecred
 |-  ( ph -> ( 1 / D ) e. RR )
29 difrp
 |-  ( ( ( 1 / D ) e. RR /\ 1 e. RR ) -> ( ( 1 / D ) < 1 <-> ( 1 - ( 1 / D ) ) e. RR+ ) )
30 28 17 29 sylancl
 |-  ( ph -> ( ( 1 / D ) < 1 <-> ( 1 - ( 1 / D ) ) e. RR+ ) )
31 27 30 mpbid
 |-  ( ph -> ( 1 - ( 1 / D ) ) e. RR+ )
32 3nn0
 |-  3 e. NN0
33 2nn
 |-  2 e. NN
34 32 33 decnncl
 |-  ; 3 2 e. NN
35 nnrp
 |-  ( ; 3 2 e. NN -> ; 3 2 e. RR+ )
36 34 35 ax-mp
 |-  ; 3 2 e. RR+
37 rpmulcl
 |-  ( ( ; 3 2 e. RR+ /\ B e. RR+ ) -> ( ; 3 2 x. B ) e. RR+ )
38 36 3 37 sylancr
 |-  ( ph -> ( ; 3 2 x. B ) e. RR+ )
39 12 38 rpdivcld
 |-  ( ph -> ( L / ( ; 3 2 x. B ) ) e. RR+ )
40 2z
 |-  2 e. ZZ
41 rpexpcl
 |-  ( ( D e. RR+ /\ 2 e. ZZ ) -> ( D ^ 2 ) e. RR+ )
42 16 40 41 sylancl
 |-  ( ph -> ( D ^ 2 ) e. RR+ )
43 39 42 rpdivcld
 |-  ( ph -> ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) e. RR+ )
44 31 43 rpmulcld
 |-  ( ph -> ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) ) e. RR+ )
45 6 44 eqeltrid
 |-  ( ph -> F e. RR+ )
46 12 16 45 3jca
 |-  ( ph -> ( L e. RR+ /\ D e. RR+ /\ F e. RR+ ) )