Proof of Theorem pntlemn
Step | Hyp | Ref
| Expression |
1 | | pntlem1.u |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈
ℝ+) |
2 | 1 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → 𝑈 ∈
ℝ+) |
3 | 2 | rpred 12628 |
. . . 4
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → 𝑈 ∈ ℝ) |
4 | | simprl 771 |
. . . 4
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → 𝐽 ∈ ℕ) |
5 | 3, 4 | nndivred 11884 |
. . 3
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (𝑈 / 𝐽) ∈ ℝ) |
6 | | pntlem1.r |
. . . . . . . . . . 11
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
7 | | pntlem1.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
8 | | pntlem1.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
9 | | pntlem1.l |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿 ∈ (0(,)1)) |
10 | | pntlem1.d |
. . . . . . . . . . 11
⊢ 𝐷 = (𝐴 + 1) |
11 | | pntlem1.f |
. . . . . . . . . . 11
⊢ 𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (;32 · 𝐵)) / (𝐷↑2))) |
12 | | pntlem1.u2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ≤ 𝐴) |
13 | | pntlem1.e |
. . . . . . . . . . 11
⊢ 𝐸 = (𝑈 / 𝐷) |
14 | | pntlem1.k |
. . . . . . . . . . 11
⊢ 𝐾 = (exp‘(𝐵 / 𝐸)) |
15 | | pntlem1.y |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤
𝑌)) |
16 | | pntlem1.x |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋)) |
17 | | pntlem1.c |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
18 | | pntlem1.w |
. . . . . . . . . . 11
⊢ 𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))))) |
19 | | pntlem1.z |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑍 ∈ (𝑊[,)+∞)) |
20 | 6, 7, 8, 9, 10, 11, 1, 12, 13, 14, 15, 16, 17, 18, 19 | pntlemb 26478 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 <
𝑍 ∧ e ≤
(√‘𝑍) ∧
(√‘𝑍) ≤
(𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))) |
21 | 20 | simp1d 1144 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈
ℝ+) |
22 | 21 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → 𝑍 ∈
ℝ+) |
23 | 4 | nnrpd 12626 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → 𝐽 ∈
ℝ+) |
24 | 22, 23 | rpdivcld 12645 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (𝑍 / 𝐽) ∈
ℝ+) |
25 | 6 | pntrf 26444 |
. . . . . . . 8
⊢ 𝑅:ℝ+⟶ℝ |
26 | 25 | ffvelrni 6903 |
. . . . . . 7
⊢ ((𝑍 / 𝐽) ∈ ℝ+ → (𝑅‘(𝑍 / 𝐽)) ∈ ℝ) |
27 | 24, 26 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (𝑅‘(𝑍 / 𝐽)) ∈ ℝ) |
28 | 27, 22 | rerpdivcld 12659 |
. . . . 5
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → ((𝑅‘(𝑍 / 𝐽)) / 𝑍) ∈ ℝ) |
29 | 28 | recnd 10861 |
. . . 4
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → ((𝑅‘(𝑍 / 𝐽)) / 𝑍) ∈ ℂ) |
30 | 29 | abscld 15000 |
. . 3
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (abs‘((𝑅‘(𝑍 / 𝐽)) / 𝑍)) ∈ ℝ) |
31 | 5, 30 | resubcld 11260 |
. 2
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → ((𝑈 / 𝐽) − (abs‘((𝑅‘(𝑍 / 𝐽)) / 𝑍))) ∈ ℝ) |
32 | 23 | relogcld 25511 |
. 2
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (log‘𝐽) ∈ ℝ) |
33 | 27 | recnd 10861 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (𝑅‘(𝑍 / 𝐽)) ∈ ℂ) |
34 | 22 | rpcnne0d 12637 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0)) |
35 | 23 | rpcnne0d 12637 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (𝐽 ∈ ℂ ∧ 𝐽 ≠ 0)) |
36 | | divdiv2 11544 |
. . . . . . . . 9
⊢ (((𝑅‘(𝑍 / 𝐽)) ∈ ℂ ∧ (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0) ∧ (𝐽 ∈ ℂ ∧ 𝐽 ≠ 0)) → ((𝑅‘(𝑍 / 𝐽)) / (𝑍 / 𝐽)) = (((𝑅‘(𝑍 / 𝐽)) · 𝐽) / 𝑍)) |
37 | 33, 34, 35, 36 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → ((𝑅‘(𝑍 / 𝐽)) / (𝑍 / 𝐽)) = (((𝑅‘(𝑍 / 𝐽)) · 𝐽) / 𝑍)) |
38 | 4 | nncnd 11846 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → 𝐽 ∈ ℂ) |
39 | | div23 11509 |
. . . . . . . . 9
⊢ (((𝑅‘(𝑍 / 𝐽)) ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0)) → (((𝑅‘(𝑍 / 𝐽)) · 𝐽) / 𝑍) = (((𝑅‘(𝑍 / 𝐽)) / 𝑍) · 𝐽)) |
40 | 33, 38, 34, 39 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (((𝑅‘(𝑍 / 𝐽)) · 𝐽) / 𝑍) = (((𝑅‘(𝑍 / 𝐽)) / 𝑍) · 𝐽)) |
41 | 37, 40 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → ((𝑅‘(𝑍 / 𝐽)) / (𝑍 / 𝐽)) = (((𝑅‘(𝑍 / 𝐽)) / 𝑍) · 𝐽)) |
42 | 41 | fveq2d 6721 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (abs‘((𝑅‘(𝑍 / 𝐽)) / (𝑍 / 𝐽))) = (abs‘(((𝑅‘(𝑍 / 𝐽)) / 𝑍) · 𝐽))) |
43 | 29, 38 | absmuld 15018 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (abs‘(((𝑅‘(𝑍 / 𝐽)) / 𝑍) · 𝐽)) = ((abs‘((𝑅‘(𝑍 / 𝐽)) / 𝑍)) · (abs‘𝐽))) |
44 | 23 | rprege0d 12635 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (𝐽 ∈ ℝ ∧ 0 ≤ 𝐽)) |
45 | | absid 14860 |
. . . . . . . 8
⊢ ((𝐽 ∈ ℝ ∧ 0 ≤
𝐽) → (abs‘𝐽) = 𝐽) |
46 | 44, 45 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (abs‘𝐽) = 𝐽) |
47 | 46 | oveq2d 7229 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → ((abs‘((𝑅‘(𝑍 / 𝐽)) / 𝑍)) · (abs‘𝐽)) = ((abs‘((𝑅‘(𝑍 / 𝐽)) / 𝑍)) · 𝐽)) |
48 | 42, 43, 47 | 3eqtrd 2781 |
. . . . 5
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (abs‘((𝑅‘(𝑍 / 𝐽)) / (𝑍 / 𝐽))) = ((abs‘((𝑅‘(𝑍 / 𝐽)) / 𝑍)) · 𝐽)) |
49 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑧 = (𝑍 / 𝐽) → (𝑅‘𝑧) = (𝑅‘(𝑍 / 𝐽))) |
50 | | id 22 |
. . . . . . . . 9
⊢ (𝑧 = (𝑍 / 𝐽) → 𝑧 = (𝑍 / 𝐽)) |
51 | 49, 50 | oveq12d 7231 |
. . . . . . . 8
⊢ (𝑧 = (𝑍 / 𝐽) → ((𝑅‘𝑧) / 𝑧) = ((𝑅‘(𝑍 / 𝐽)) / (𝑍 / 𝐽))) |
52 | 51 | fveq2d 6721 |
. . . . . . 7
⊢ (𝑧 = (𝑍 / 𝐽) → (abs‘((𝑅‘𝑧) / 𝑧)) = (abs‘((𝑅‘(𝑍 / 𝐽)) / (𝑍 / 𝐽)))) |
53 | 52 | breq1d 5063 |
. . . . . 6
⊢ (𝑧 = (𝑍 / 𝐽) → ((abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑈 ↔ (abs‘((𝑅‘(𝑍 / 𝐽)) / (𝑍 / 𝐽))) ≤ 𝑈)) |
54 | | pntlem1.U |
. . . . . . 7
⊢ (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑈) |
55 | 54 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑈) |
56 | 24 | rpred 12628 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (𝑍 / 𝐽) ∈ ℝ) |
57 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → 𝐽 ≤ (𝑍 / 𝑌)) |
58 | 23 | rpred 12628 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → 𝐽 ∈ ℝ) |
59 | 22 | rpred 12628 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → 𝑍 ∈ ℝ) |
60 | 15 | simpld 498 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈
ℝ+) |
61 | 60 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → 𝑌 ∈
ℝ+) |
62 | 58, 59, 61 | lemuldiv2d 12678 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → ((𝑌 · 𝐽) ≤ 𝑍 ↔ 𝐽 ≤ (𝑍 / 𝑌))) |
63 | 57, 62 | mpbird 260 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (𝑌 · 𝐽) ≤ 𝑍) |
64 | 61 | rpred 12628 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → 𝑌 ∈ ℝ) |
65 | 64, 59, 23 | lemuldivd 12677 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → ((𝑌 · 𝐽) ≤ 𝑍 ↔ 𝑌 ≤ (𝑍 / 𝐽))) |
66 | 63, 65 | mpbid 235 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → 𝑌 ≤ (𝑍 / 𝐽)) |
67 | | elicopnf 13033 |
. . . . . . . 8
⊢ (𝑌 ∈ ℝ → ((𝑍 / 𝐽) ∈ (𝑌[,)+∞) ↔ ((𝑍 / 𝐽) ∈ ℝ ∧ 𝑌 ≤ (𝑍 / 𝐽)))) |
68 | 64, 67 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → ((𝑍 / 𝐽) ∈ (𝑌[,)+∞) ↔ ((𝑍 / 𝐽) ∈ ℝ ∧ 𝑌 ≤ (𝑍 / 𝐽)))) |
69 | 56, 66, 68 | mpbir2and 713 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (𝑍 / 𝐽) ∈ (𝑌[,)+∞)) |
70 | 53, 55, 69 | rspcdva 3539 |
. . . . 5
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (abs‘((𝑅‘(𝑍 / 𝐽)) / (𝑍 / 𝐽))) ≤ 𝑈) |
71 | 48, 70 | eqbrtrrd 5077 |
. . . 4
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → ((abs‘((𝑅‘(𝑍 / 𝐽)) / 𝑍)) · 𝐽) ≤ 𝑈) |
72 | 30, 3, 23 | lemuldivd 12677 |
. . . 4
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (((abs‘((𝑅‘(𝑍 / 𝐽)) / 𝑍)) · 𝐽) ≤ 𝑈 ↔ (abs‘((𝑅‘(𝑍 / 𝐽)) / 𝑍)) ≤ (𝑈 / 𝐽))) |
73 | 71, 72 | mpbid 235 |
. . 3
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (abs‘((𝑅‘(𝑍 / 𝐽)) / 𝑍)) ≤ (𝑈 / 𝐽)) |
74 | 5, 30 | subge0d 11422 |
. . 3
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (0 ≤ ((𝑈 / 𝐽) − (abs‘((𝑅‘(𝑍 / 𝐽)) / 𝑍))) ↔ (abs‘((𝑅‘(𝑍 / 𝐽)) / 𝑍)) ≤ (𝑈 / 𝐽))) |
75 | 73, 74 | mpbird 260 |
. 2
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → 0 ≤ ((𝑈 / 𝐽) − (abs‘((𝑅‘(𝑍 / 𝐽)) / 𝑍)))) |
76 | | log1 25474 |
. . 3
⊢
(log‘1) = 0 |
77 | | nnge1 11858 |
. . . . 5
⊢ (𝐽 ∈ ℕ → 1 ≤
𝐽) |
78 | 77 | ad2antrl 728 |
. . . 4
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → 1 ≤ 𝐽) |
79 | | 1rp 12590 |
. . . . 5
⊢ 1 ∈
ℝ+ |
80 | | logleb 25491 |
. . . . 5
⊢ ((1
∈ ℝ+ ∧ 𝐽 ∈ ℝ+) → (1 ≤
𝐽 ↔ (log‘1) ≤
(log‘𝐽))) |
81 | 79, 23, 80 | sylancr 590 |
. . . 4
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (1 ≤ 𝐽 ↔ (log‘1) ≤ (log‘𝐽))) |
82 | 78, 81 | mpbid 235 |
. . 3
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → (log‘1) ≤
(log‘𝐽)) |
83 | 76, 82 | eqbrtrrid 5089 |
. 2
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → 0 ≤ (log‘𝐽)) |
84 | 31, 32, 75, 83 | mulge0d 11409 |
1
⊢ ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → 0 ≤ (((𝑈 / 𝐽) − (abs‘((𝑅‘(𝑍 / 𝐽)) / 𝑍))) · (log‘𝐽))) |