Metamath Proof Explorer

Theorem pntlemc

Description: Lemma for pnt . Closure for the constants used in the proof. For comparison with Equation 10.6.27 of Shapiro, p. 434, U is α, E is ε, and K isK. (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 ) )
Assertion pntlemc 
|- ( ph -> ( E e. RR+ /\ K e. RR+ /\ ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) 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 1 2 3 4 5 6 pntlemd 
 |-  ( ph -> ( L e. RR+ /\ D e. RR+ /\ F e. RR+ ) )
12 11 simp2d 
 |-  ( ph -> D e. RR+ )
13 7 12 rpdivcld 
 |-  ( ph -> ( U / D ) e. RR+ )
14 9 13 eqeltrid 
 |-  ( ph -> E e. RR+ )
15 3 14 rpdivcld 
 |-  ( ph -> ( B / E ) e. RR+ )
16 15 rpred 
 |-  ( ph -> ( B / E ) e. RR )
17 16 rpefcld 
 |-  ( ph -> ( exp ` ( B / E ) ) e. RR+ )
18 10 17 eqeltrid 
 |-  ( ph -> K e. RR+ )
19 14 rpred 
 |-  ( ph -> E e. RR )
20 14 rpgt0d 
 |-  ( ph -> 0 < E )
21 7 rpred 
 |-  ( ph -> U e. RR )
22 2 rpred 
 |-  ( ph -> A e. RR )
23 12 rpred 
 |-  ( ph -> D e. RR )
24 22 ltp1d 
 |-  ( ph -> A < ( A + 1 ) )
25 24 5 breqtrrdi 
 |-  ( ph -> A < D )
26 21 22 23 8 25 lelttrd 
 |-  ( ph -> U < D )
27 12 rpcnd 
 |-  ( ph -> D e. CC )
28 27 mulid1d 
 |-  ( ph -> ( D x. 1 ) = D )
29 26 28 breqtrrd 
 |-  ( ph -> U < ( D x. 1 ) )
30 1red 
 |-  ( ph -> 1 e. RR )
31 21 30 12 ltdivmuld 
 |-  ( ph -> ( ( U / D ) < 1 <-> U < ( D x. 1 ) ) )
32 29 31 mpbird 
 |-  ( ph -> ( U / D ) < 1 )
33 9 32 eqbrtrid 
 |-  ( ph -> E < 1 )
34 0xr 
 |-  0 e. RR*
35 1xr 
 |-  1 e. RR*
36 elioo2 
 |-  ( ( 0 e. RR* /\ 1 e. RR* ) -> ( E e. ( 0 (,) 1 ) <-> ( E e. RR /\ 0 < E /\ E < 1 ) ) )
37 34 35 36 mp2an 
 |-  ( E e. ( 0 (,) 1 ) <-> ( E e. RR /\ 0 < E /\ E < 1 ) )
38 19 20 33 37 syl3anbrc 
 |-  ( ph -> E e. ( 0 (,) 1 ) )
39 efgt1 
 |-  ( ( B / E ) e. RR+ -> 1 < ( exp ` ( B / E ) ) )
40 15 39 syl 
 |-  ( ph -> 1 < ( exp ` ( B / E ) ) )
41 40 10 breqtrrdi 
 |-  ( ph -> 1 < K )
42 1re 
 |-  1 e. RR
43 ltaddrp 
 |-  ( ( 1 e. RR /\ A e. RR+ ) -> 1 < ( 1 + A ) )
44 42 2 43 sylancr 
 |-  ( ph -> 1 < ( 1 + A ) )
45 7 rpcnne0d 
 |-  ( ph -> ( U e. CC /\ U =/= 0 ) )
46 divid 
 |-  ( ( U e. CC /\ U =/= 0 ) -> ( U / U ) = 1 )
47 45 46 syl 
 |-  ( ph -> ( U / U ) = 1 )
48 2 rpcnd 
 |-  ( ph -> A e. CC )
49 ax-1cn 
 |-  1 e. CC
50 addcom 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( A + 1 ) = ( 1 + A ) )
51 48 49 50 sylancl 
 |-  ( ph -> ( A + 1 ) = ( 1 + A ) )
52 5 51 syl5eq 
 |-  ( ph -> D = ( 1 + A ) )
53 44 47 52 3brtr4d 
 |-  ( ph -> ( U / U ) < D )
54 21 7 12 53 ltdiv23d 
 |-  ( ph -> ( U / D ) < U )
55 9 54 eqbrtrid 
 |-  ( ph -> E < U )
56 difrp 
 |-  ( ( E e. RR /\ U e. RR ) -> ( E < U <-> ( U - E ) e. RR+ ) )
57 19 21 56 syl2anc 
 |-  ( ph -> ( E < U <-> ( U - E ) e. RR+ ) )
58 55 57 mpbid 
 |-  ( ph -> ( U - E ) e. RR+ )
59 38 41 58 3jca 
 |-  ( ph -> ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) )
60 14 18 59 3jca 
 |-  ( ph -> ( E e. RR+ /\ K e. RR+ /\ ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) ) )