Metamath Proof Explorer

Theorem pntlema

Description: Lemma for pnt . Closure for the constants used in the proof. The mammoth expression W is a number large enough to satisfy all the lower bounds needed for Z . For comparison with Equation 10.6.27 of Shapiro, p. 434, Y is x_2, X is x_1, C is the big-O constant in Equation 10.6.29 of Shapiro, p. 435, and W is the unnamed lower bound of "for sufficiently large x" in Equation 10.6.34 of Shapiro, p. 436. (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 ) ) )
pntlem1.u 
|- ( ph -> U e. RR+ )
pntlem1.u2 
|- ( ph -> U <_ A )
pntlem1.e 
|- E = ( U / D )
pntlem1.k 
|- K = ( exp ` ( B / E ) )
pntlem1.y 
|- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )
pntlem1.x 
|- ( ph -> ( X e. RR+ /\ Y < X ) )
pntlem1.c 
|- ( ph -> C e. RR+ )
pntlem1.w 
|- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )
Assertion pntlema 
|- ( ph -> W 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 pntlem1.u 
 |-  ( ph -> U e. RR+ )
8 pntlem1.u2 
 |-  ( ph -> U <_ A )
9 pntlem1.e 
 |-  E = ( U / D )
10 pntlem1.k 
 |-  K = ( exp ` ( B / E ) )
11 pntlem1.y 
 |-  ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )
12 pntlem1.x 
 |-  ( ph -> ( X e. RR+ /\ Y < X ) )
13 pntlem1.c 
 |-  ( ph -> C e. RR+ )
14 pntlem1.w 
 |-  W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )
15 11 simpld 
 |-  ( ph -> Y e. RR+ )
16 4nn 
 |-  4 e. NN
17 nnrp 
 |-  ( 4 e. NN -> 4 e. RR+ )
18 16 17 ax-mp 
 |-  4 e. RR+
19 1 2 3 4 5 6 pntlemd 
 |-  ( ph -> ( L e. RR+ /\ D e. RR+ /\ F e. RR+ ) )
20 19 simp1d 
 |-  ( ph -> L e. RR+ )
21 1 2 3 4 5 6 7 8 9 10 pntlemc 
 |-  ( ph -> ( E e. RR+ /\ K e. RR+ /\ ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) ) )
22 21 simp1d 
 |-  ( ph -> E e. RR+ )
23 20 22 rpmulcld 
 |-  ( ph -> ( L x. E ) e. RR+ )
24 rpdivcl 
 |-  ( ( 4 e. RR+ /\ ( L x. E ) e. RR+ ) -> ( 4 / ( L x. E ) ) e. RR+ )
25 18 23 24 sylancr 
 |-  ( ph -> ( 4 / ( L x. E ) ) e. RR+ )
26 15 25 rpaddcld 
 |-  ( ph -> ( Y + ( 4 / ( L x. E ) ) ) e. RR+ )
27 2z 
 |-  2 e. ZZ
28 rpexpcl 
 |-  ( ( ( Y + ( 4 / ( L x. E ) ) ) e. RR+ /\ 2 e. ZZ ) -> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) e. RR+ )
29 26 27 28 sylancl 
 |-  ( ph -> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) e. RR+ )
30 12 simpld 
 |-  ( ph -> X e. RR+ )
31 21 simp2d 
 |-  ( ph -> K e. RR+ )
32 rpexpcl 
 |-  ( ( K e. RR+ /\ 2 e. ZZ ) -> ( K ^ 2 ) e. RR+ )
33 31 27 32 sylancl 
 |-  ( ph -> ( K ^ 2 ) e. RR+ )
34 30 33 rpmulcld 
 |-  ( ph -> ( X x. ( K ^ 2 ) ) e. RR+ )
35 4z 
 |-  4 e. ZZ
36 rpexpcl 
 |-  ( ( ( X x. ( K ^ 2 ) ) e. RR+ /\ 4 e. ZZ ) -> ( ( X x. ( K ^ 2 ) ) ^ 4 ) e. RR+ )
37 34 35 36 sylancl 
 |-  ( ph -> ( ( X x. ( K ^ 2 ) ) ^ 4 ) e. RR+ )
38 3nn0 
 |-  3 e. NN0
39 2nn 
 |-  2 e. NN
40 38 39 decnncl 
 |-  ; 3 2 e. NN
41 nnrp 
 |-  ( ; 3 2 e. NN -> ; 3 2 e. RR+ )
42 40 41 ax-mp 
 |-  ; 3 2 e. RR+
43 rpmulcl 
 |-  ( ( ; 3 2 e. RR+ /\ B e. RR+ ) -> ( ; 3 2 x. B ) e. RR+ )
44 42 3 43 sylancr 
 |-  ( ph -> ( ; 3 2 x. B ) e. RR+ )
45 21 simp3d 
 |-  ( ph -> ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) )
46 45 simp3d 
 |-  ( ph -> ( U - E ) e. RR+ )
47 rpexpcl 
 |-  ( ( E e. RR+ /\ 2 e. ZZ ) -> ( E ^ 2 ) e. RR+ )
48 22 27 47 sylancl 
 |-  ( ph -> ( E ^ 2 ) e. RR+ )
49 20 48 rpmulcld 
 |-  ( ph -> ( L x. ( E ^ 2 ) ) e. RR+ )
50 46 49 rpmulcld 
 |-  ( ph -> ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) e. RR+ )
51 44 50 rpdivcld 
 |-  ( ph -> ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) e. RR+ )
52 3rp 
 |-  3 e. RR+
53 rpmulcl 
 |-  ( ( U e. RR+ /\ 3 e. RR+ ) -> ( U x. 3 ) e. RR+ )
54 7 52 53 sylancl 
 |-  ( ph -> ( U x. 3 ) e. RR+ )
55 54 13 rpaddcld 
 |-  ( ph -> ( ( U x. 3 ) + C ) e. RR+ )
56 51 55 rpmulcld 
 |-  ( ph -> ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) e. RR+ )
57 56 rpred 
 |-  ( ph -> ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) e. RR )
58 57 rpefcld 
 |-  ( ph -> ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) e. RR+ )
59 37 58 rpaddcld 
 |-  ( ph -> ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) e. RR+ )
60 29 59 rpaddcld 
 |-  ( ph -> ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) ) e. RR+ )
61 14 60 eqeltrid 
 |-  ( ph -> W e. RR+ )