Metamath Proof Explorer

Theorem pntibndlem1

Description: Lemma for pntibnd . (Contributed by Mario Carneiro, 10-Apr-2016)

Ref Expression
Hypotheses pntibnd.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
pntibndlem1.1 
|- ( ph -> A e. RR+ )
pntibndlem1.l 
|- L = ( ( 1 / 4 ) / ( A + 3 ) )
Assertion pntibndlem1 
|- ( ph -> L e. ( 0 (,) 1 ) )

Proof

Step Hyp Ref Expression
1 pntibnd.r 
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2 pntibndlem1.1 
 |-  ( ph -> A e. RR+ )
3 pntibndlem1.l 
 |-  L = ( ( 1 / 4 ) / ( A + 3 ) )
4 4nn 
 |-  4 e. NN
5 nnrp 
 |-  ( 4 e. NN -> 4 e. RR+ )
6 rpreccl 
 |-  ( 4 e. RR+ -> ( 1 / 4 ) e. RR+ )
7 4 5 6 mp2b 
 |-  ( 1 / 4 ) e. RR+
8 3rp 
 |-  3 e. RR+
9 rpaddcl 
 |-  ( ( A e. RR+ /\ 3 e. RR+ ) -> ( A + 3 ) e. RR+ )
10 2 8 9 sylancl 
 |-  ( ph -> ( A + 3 ) e. RR+ )
11 rpdivcl 
 |-  ( ( ( 1 / 4 ) e. RR+ /\ ( A + 3 ) e. RR+ ) -> ( ( 1 / 4 ) / ( A + 3 ) ) e. RR+ )
12 7 10 11 sylancr 
 |-  ( ph -> ( ( 1 / 4 ) / ( A + 3 ) ) e. RR+ )
13 3 12 eqeltrid 
 |-  ( ph -> L e. RR+ )
14 13 rpred 
 |-  ( ph -> L e. RR )
15 13 rpgt0d 
 |-  ( ph -> 0 < L )
16 rpcn 
 |-  ( ( 1 / 4 ) e. RR+ -> ( 1 / 4 ) e. CC )
17 7 16 ax-mp 
 |-  ( 1 / 4 ) e. CC
18 17 div1i 
 |-  ( ( 1 / 4 ) / 1 ) = ( 1 / 4 )
19 rpre 
 |-  ( ( 1 / 4 ) e. RR+ -> ( 1 / 4 ) e. RR )
20 7 19 mp1i 
 |-  ( ph -> ( 1 / 4 ) e. RR )
21 3re 
 |-  3 e. RR
22 21 a1i 
 |-  ( ph -> 3 e. RR )
23 10 rpred 
 |-  ( ph -> ( A + 3 ) e. RR )
24 1lt4 
 |-  1 < 4
25 4re 
 |-  4 e. RR
26 4pos 
 |-  0 < 4
27 recgt1 
 |-  ( ( 4 e. RR /\ 0 < 4 ) -> ( 1 < 4 <-> ( 1 / 4 ) < 1 ) )
28 25 26 27 mp2an 
 |-  ( 1 < 4 <-> ( 1 / 4 ) < 1 )
29 24 28 mpbi 
 |-  ( 1 / 4 ) < 1
30 1lt3 
 |-  1 < 3
31 7 19 ax-mp 
 |-  ( 1 / 4 ) e. RR
32 1re 
 |-  1 e. RR
33 31 32 21 lttri 
 |-  ( ( ( 1 / 4 ) < 1 /\ 1 < 3 ) -> ( 1 / 4 ) < 3 )
34 29 30 33 mp2an 
 |-  ( 1 / 4 ) < 3
35 34 a1i 
 |-  ( ph -> ( 1 / 4 ) < 3 )
36 ltaddrp 
 |-  ( ( 3 e. RR /\ A e. RR+ ) -> 3 < ( 3 + A ) )
37 21 2 36 sylancr 
 |-  ( ph -> 3 < ( 3 + A ) )
38 3cn 
 |-  3 e. CC
39 2 rpcnd 
 |-  ( ph -> A e. CC )
40 addcom 
 |-  ( ( 3 e. CC /\ A e. CC ) -> ( 3 + A ) = ( A + 3 ) )
41 38 39 40 sylancr 
 |-  ( ph -> ( 3 + A ) = ( A + 3 ) )
42 37 41 breqtrd 
 |-  ( ph -> 3 < ( A + 3 ) )
43 20 22 23 35 42 lttrd 
 |-  ( ph -> ( 1 / 4 ) < ( A + 3 ) )
44 18 43 eqbrtrid 
 |-  ( ph -> ( ( 1 / 4 ) / 1 ) < ( A + 3 ) )
45 32 a1i 
 |-  ( ph -> 1 e. RR )
46 0lt1 
 |-  0 < 1
47 46 a1i 
 |-  ( ph -> 0 < 1 )
48 10 rpregt0d 
 |-  ( ph -> ( ( A + 3 ) e. RR /\ 0 < ( A + 3 ) ) )
49 ltdiv23 
 |-  ( ( ( 1 / 4 ) e. RR /\ ( 1 e. RR /\ 0 < 1 ) /\ ( ( A + 3 ) e. RR /\ 0 < ( A + 3 ) ) ) -> ( ( ( 1 / 4 ) / 1 ) < ( A + 3 ) <-> ( ( 1 / 4 ) / ( A + 3 ) ) < 1 ) )
50 20 45 47 48 49 syl121anc 
 |-  ( ph -> ( ( ( 1 / 4 ) / 1 ) < ( A + 3 ) <-> ( ( 1 / 4 ) / ( A + 3 ) ) < 1 ) )
51 44 50 mpbid 
 |-  ( ph -> ( ( 1 / 4 ) / ( A + 3 ) ) < 1 )
52 3 51 eqbrtrid 
 |-  ( ph -> L < 1 )
53 0xr 
 |-  0 e. RR*
54 1xr 
 |-  1 e. RR*
55 elioo2 
 |-  ( ( 0 e. RR* /\ 1 e. RR* ) -> ( L e. ( 0 (,) 1 ) <-> ( L e. RR /\ 0 < L /\ L < 1 ) ) )
56 53 54 55 mp2an 
 |-  ( L e. ( 0 (,) 1 ) <-> ( L e. RR /\ 0 < L /\ L < 1 ) )
57 14 15 52 56 syl3anbrc 
 |-  ( ph -> L e. ( 0 (,) 1 ) )