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 ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
pntlem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
pntlem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
pntlem1.l ⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
pntlem1.d ⊢ 𝐷 = ( 𝐴 + 1 )
pntlem1.f ⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
pntlem1.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
pntlem1.u2 ⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
pntlem1.e ⊢ 𝐸 = ( 𝑈 / 𝐷 )
pntlem1.k ⊢ 𝐾 = ( exp ‘ ( 𝐵 / 𝐸 ) )
Assertion pntlemc ( 𝜑 → ( 𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+ ∧ ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) ) )

Proof

Step Hyp Ref Expression
1 pntlem1.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2 pntlem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
3 pntlem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
4 pntlem1.l ⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
5 pntlem1.d ⊢ 𝐷 = ( 𝐴 + 1 )
6 pntlem1.f ⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
7 pntlem1.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
8 pntlem1.u2 ⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
9 pntlem1.e ⊢ 𝐸 = ( 𝑈 / 𝐷 )
10 pntlem1.k ⊢ 𝐾 = ( exp ‘ ( 𝐵 / 𝐸 ) )
11 1 2 3 4 5 6 pntlemd ⊢ ( 𝜑 → ( 𝐿 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+ ∧ 𝐹 ∈ ℝ+ ) )
12 11 simp2d ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
13 7 12 rpdivcld ⊢ ( 𝜑 → ( 𝑈 / 𝐷 ) ∈ ℝ+ )
14 9 13 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
15 3 14 rpdivcld ⊢ ( 𝜑 → ( 𝐵 / 𝐸 ) ∈ ℝ+ )
16 15 rpred ⊢ ( 𝜑 → ( 𝐵 / 𝐸 ) ∈ ℝ )
17 16 rpefcld ⊢ ( 𝜑 → ( exp ‘ ( 𝐵 / 𝐸 ) ) ∈ ℝ+ )
18 10 17 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ℝ+ )
19 14 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
20 14 rpgt0d ⊢ ( 𝜑 → 0 < 𝐸 )
21 7 rpred ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
22 2 rpred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
23 12 rpred ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
24 22 ltp1d ⊢ ( 𝜑 → 𝐴 < ( 𝐴 + 1 ) )
25 24 5 breqtrrdi ⊢ ( 𝜑 → 𝐴 < 𝐷 )
26 21 22 23 8 25 lelttrd ⊢ ( 𝜑 → 𝑈 < 𝐷 )
27 12 rpcnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
28 27 mulid1d ⊢ ( 𝜑 → ( 𝐷 · 1 ) = 𝐷 )
29 26 28 breqtrrd ⊢ ( 𝜑 → 𝑈 < ( 𝐷 · 1 ) )
30 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
31 21 30 12 ltdivmuld ⊢ ( 𝜑 → ( ( 𝑈 / 𝐷 ) < 1 ↔ 𝑈 < ( 𝐷 · 1 ) ) )
32 29 31 mpbird ⊢ ( 𝜑 → ( 𝑈 / 𝐷 ) < 1 )
33 9 32 eqbrtrid ⊢ ( 𝜑 → 𝐸 < 1 )
34 0xr ⊢ 0 ∈ ℝ*
35 1xr ⊢ 1 ∈ ℝ*
36 elioo2 ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( 𝐸 ∈ ( 0 (,) 1 ) ↔ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ∧ 𝐸 < 1 ) ) )
37 34 35 36 mp2an ⊢ ( 𝐸 ∈ ( 0 (,) 1 ) ↔ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ∧ 𝐸 < 1 ) )
38 19 20 33 37 syl3anbrc ⊢ ( 𝜑 → 𝐸 ∈ ( 0 (,) 1 ) )
39 efgt1 ⊢ ( ( 𝐵 / 𝐸 ) ∈ ℝ+ → 1 < ( exp ‘ ( 𝐵 / 𝐸 ) ) )
40 15 39 syl ⊢ ( 𝜑 → 1 < ( exp ‘ ( 𝐵 / 𝐸 ) ) )
41 40 10 breqtrrdi ⊢ ( 𝜑 → 1 < 𝐾 )
42 1re ⊢ 1 ∈ ℝ
43 ltaddrp ⊢ ( ( 1 ∈ ℝ ∧ 𝐴 ∈ ℝ+ ) → 1 < ( 1 + 𝐴 ) )
44 42 2 43 sylancr ⊢ ( 𝜑 → 1 < ( 1 + 𝐴 ) )
45 7 rpcnne0d ⊢ ( 𝜑 → ( 𝑈 ∈ ℂ ∧ 𝑈 ≠ 0 ) )
46 divid ⊢ ( ( 𝑈 ∈ ℂ ∧ 𝑈 ≠ 0 ) → ( 𝑈 / 𝑈 ) = 1 )
47 45 46 syl ⊢ ( 𝜑 → ( 𝑈 / 𝑈 ) = 1 )
48 2 rpcnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
49 ax-1cn ⊢ 1 ∈ ℂ
50 addcom ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐴 + 1 ) = ( 1 + 𝐴 ) )
51 48 49 50 sylancl ⊢ ( 𝜑 → ( 𝐴 + 1 ) = ( 1 + 𝐴 ) )
52 5 51 syl5eq ⊢ ( 𝜑 → 𝐷 = ( 1 + 𝐴 ) )
53 44 47 52 3brtr4d ⊢ ( 𝜑 → ( 𝑈 / 𝑈 ) < 𝐷 )
54 21 7 12 53 ltdiv23d ⊢ ( 𝜑 → ( 𝑈 / 𝐷 ) < 𝑈 )
55 9 54 eqbrtrid ⊢ ( 𝜑 → 𝐸 < 𝑈 )
56 difrp ⊢ ( ( 𝐸 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → ( 𝐸 < 𝑈 ↔ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) )
57 19 21 56 syl2anc ⊢ ( 𝜑 → ( 𝐸 < 𝑈 ↔ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) )
58 55 57 mpbid ⊢ ( 𝜑 → ( 𝑈 − 𝐸 ) ∈ ℝ+ )
59 38 41 58 3jca ⊢ ( 𝜑 → ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) )
60 14 18 59 3jca ⊢ ( 𝜑 → ( 𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+ ∧ ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) ) )