Proof of Theorem pntlemh
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pntlem1.x | . . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋)) | 
| 2 | 1 | simpld 494 | . . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈
ℝ+) | 
| 3 | 2 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → 𝑋 ∈
ℝ+) | 
| 4 | 3 | relogcld 26666 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (log‘𝑋) ∈ ℝ) | 
| 5 |  | pntlem1.r | . . . . . . . . . . . 12
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) | 
| 6 |  | pntlem1.a | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈
ℝ+) | 
| 7 |  | pntlem1.b | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈
ℝ+) | 
| 8 |  | pntlem1.l | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐿 ∈ (0(,)1)) | 
| 9 |  | pntlem1.d | . . . . . . . . . . . 12
⊢ 𝐷 = (𝐴 + 1) | 
| 10 |  | pntlem1.f | . . . . . . . . . . . 12
⊢ 𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (;32 · 𝐵)) / (𝐷↑2))) | 
| 11 |  | pntlem1.u | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈
ℝ+) | 
| 12 |  | pntlem1.u2 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ≤ 𝐴) | 
| 13 |  | pntlem1.e | . . . . . . . . . . . 12
⊢ 𝐸 = (𝑈 / 𝐷) | 
| 14 |  | pntlem1.k | . . . . . . . . . . . 12
⊢ 𝐾 = (exp‘(𝐵 / 𝐸)) | 
| 15 | 5, 6, 7, 8, 9, 10,
11, 12, 13, 14 | pntlemc 27640 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+
∧ (𝐸 ∈ (0(,)1)
∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈
ℝ+))) | 
| 16 | 15 | simp2d 1143 | . . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈
ℝ+) | 
| 17 | 16 | rpred 13078 | . . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℝ) | 
| 18 | 15 | simp3d 1144 | . . . . . . . . . 10
⊢ (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈
ℝ+)) | 
| 19 | 18 | simp2d 1143 | . . . . . . . . 9
⊢ (𝜑 → 1 < 𝐾) | 
| 20 | 17, 19 | rplogcld 26672 | . . . . . . . 8
⊢ (𝜑 → (log‘𝐾) ∈
ℝ+) | 
| 21 | 20 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (log‘𝐾) ∈
ℝ+) | 
| 22 | 4, 21 | rerpdivcld 13109 | . . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → ((log‘𝑋) / (log‘𝐾)) ∈ ℝ) | 
| 23 |  | pntlem1.y | . . . . . . . . . 10
⊢ (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤
𝑌)) | 
| 24 |  | pntlem1.c | . . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈
ℝ+) | 
| 25 |  | pntlem1.w | . . . . . . . . . 10
⊢ 𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))))) | 
| 26 |  | pntlem1.z | . . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ (𝑊[,)+∞)) | 
| 27 |  | pntlem1.m | . . . . . . . . . 10
⊢ 𝑀 =
((⌊‘((log‘𝑋) / (log‘𝐾))) + 1) | 
| 28 |  | pntlem1.n | . . . . . . . . . 10
⊢ 𝑁 =
(⌊‘(((log‘𝑍) / (log‘𝐾)) / 2)) | 
| 29 | 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 23, 1, 24, 25, 26, 27, 28 | pntlemg 27643 | . . . . . . . . 9
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘𝑀) ∧ (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁 − 𝑀))) | 
| 30 | 29 | simp1d 1142 | . . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 31 | 30 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℕ) | 
| 32 | 31 | nnred 12282 | . . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℝ) | 
| 33 |  | elfzuz 13561 | . . . . . . . 8
⊢ (𝐽 ∈ (𝑀...𝑁) → 𝐽 ∈ (ℤ≥‘𝑀)) | 
| 34 |  | eluznn 12961 | . . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐽 ∈
(ℤ≥‘𝑀)) → 𝐽 ∈ ℕ) | 
| 35 | 30, 33, 34 | syl2an 596 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → 𝐽 ∈ ℕ) | 
| 36 | 35 | nnred 12282 | . . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → 𝐽 ∈ ℝ) | 
| 37 |  | flltp1 13841 | . . . . . . . 8
⊢
(((log‘𝑋) /
(log‘𝐾)) ∈
ℝ → ((log‘𝑋) / (log‘𝐾)) < ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)) | 
| 38 | 22, 37 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → ((log‘𝑋) / (log‘𝐾)) < ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)) | 
| 39 | 38, 27 | breqtrrdi 5184 | . . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → ((log‘𝑋) / (log‘𝐾)) < 𝑀) | 
| 40 |  | elfzle1 13568 | . . . . . . 7
⊢ (𝐽 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝐽) | 
| 41 | 40 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → 𝑀 ≤ 𝐽) | 
| 42 | 22, 32, 36, 39, 41 | ltletrd 11422 | . . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → ((log‘𝑋) / (log‘𝐾)) < 𝐽) | 
| 43 | 4, 36, 21 | ltdivmul2d 13130 | . . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (((log‘𝑋) / (log‘𝐾)) < 𝐽 ↔ (log‘𝑋) < (𝐽 · (log‘𝐾)))) | 
| 44 | 42, 43 | mpbid 232 | . . . 4
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (log‘𝑋) < (𝐽 · (log‘𝐾))) | 
| 45 | 16 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → 𝐾 ∈
ℝ+) | 
| 46 |  | elfzelz 13565 | . . . . . 6
⊢ (𝐽 ∈ (𝑀...𝑁) → 𝐽 ∈ ℤ) | 
| 47 | 46 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → 𝐽 ∈ ℤ) | 
| 48 |  | relogexp 26639 | . . . . 5
⊢ ((𝐾 ∈ ℝ+
∧ 𝐽 ∈ ℤ)
→ (log‘(𝐾↑𝐽)) = (𝐽 · (log‘𝐾))) | 
| 49 | 45, 47, 48 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (log‘(𝐾↑𝐽)) = (𝐽 · (log‘𝐾))) | 
| 50 | 44, 49 | breqtrrd 5170 | . . 3
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (log‘𝑋) < (log‘(𝐾↑𝐽))) | 
| 51 | 45, 47 | rpexpcld 14287 | . . . 4
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (𝐾↑𝐽) ∈
ℝ+) | 
| 52 |  | logltb 26643 | . . . 4
⊢ ((𝑋 ∈ ℝ+
∧ (𝐾↑𝐽) ∈ ℝ+)
→ (𝑋 < (𝐾↑𝐽) ↔ (log‘𝑋) < (log‘(𝐾↑𝐽)))) | 
| 53 | 3, 51, 52 | syl2anc 584 | . . 3
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (𝑋 < (𝐾↑𝐽) ↔ (log‘𝑋) < (log‘(𝐾↑𝐽)))) | 
| 54 | 50, 53 | mpbird 257 | . 2
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → 𝑋 < (𝐾↑𝐽)) | 
| 55 | 49 | oveq2d 7448 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (2 · (log‘(𝐾↑𝐽))) = (2 · (𝐽 · (log‘𝐾)))) | 
| 56 |  | 2z 12651 | . . . . . . . 8
⊢ 2 ∈
ℤ | 
| 57 |  | relogexp 26639 | . . . . . . . 8
⊢ (((𝐾↑𝐽) ∈ ℝ+ ∧ 2 ∈
ℤ) → (log‘((𝐾↑𝐽)↑2)) = (2 · (log‘(𝐾↑𝐽)))) | 
| 58 | 51, 56, 57 | sylancl 586 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (log‘((𝐾↑𝐽)↑2)) = (2 · (log‘(𝐾↑𝐽)))) | 
| 59 |  | 2cnd 12345 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → 2 ∈ ℂ) | 
| 60 | 36 | recnd 11290 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → 𝐽 ∈ ℂ) | 
| 61 | 45 | relogcld 26666 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (log‘𝐾) ∈ ℝ) | 
| 62 | 61 | recnd 11290 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (log‘𝐾) ∈ ℂ) | 
| 63 | 59, 60, 62 | mulassd 11285 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → ((2 · 𝐽) · (log‘𝐾)) = (2 · (𝐽 · (log‘𝐾)))) | 
| 64 | 55, 58, 63 | 3eqtr4d 2786 | . . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (log‘((𝐾↑𝐽)↑2)) = ((2 · 𝐽) · (log‘𝐾))) | 
| 65 |  | elfzle2 13569 | . . . . . . . . . . 11
⊢ (𝐽 ∈ (𝑀...𝑁) → 𝐽 ≤ 𝑁) | 
| 66 | 65 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → 𝐽 ≤ 𝑁) | 
| 67 | 66, 28 | breqtrdi 5183 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → 𝐽 ≤ (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2))) | 
| 68 | 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 23, 1, 24, 25, 26 | pntlemb 27642 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 <
𝑍 ∧ e ≤
(√‘𝑍) ∧
(√‘𝑍) ≤
(𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))) | 
| 69 | 68 | simp1d 1142 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑍 ∈
ℝ+) | 
| 70 | 69 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → 𝑍 ∈
ℝ+) | 
| 71 | 70 | relogcld 26666 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (log‘𝑍) ∈ ℝ) | 
| 72 | 71, 21 | rerpdivcld 13109 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → ((log‘𝑍) / (log‘𝐾)) ∈ ℝ) | 
| 73 | 72 | rehalfcld 12515 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (((log‘𝑍) / (log‘𝐾)) / 2) ∈ ℝ) | 
| 74 |  | flge 13846 | . . . . . . . . . 10
⊢
(((((log‘𝑍) /
(log‘𝐾)) / 2) ∈
ℝ ∧ 𝐽 ∈
ℤ) → (𝐽 ≤
(((log‘𝑍) /
(log‘𝐾)) / 2) ↔
𝐽 ≤
(⌊‘(((log‘𝑍) / (log‘𝐾)) / 2)))) | 
| 75 | 73, 47, 74 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (𝐽 ≤ (((log‘𝑍) / (log‘𝐾)) / 2) ↔ 𝐽 ≤ (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2)))) | 
| 76 | 67, 75 | mpbird 257 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → 𝐽 ≤ (((log‘𝑍) / (log‘𝐾)) / 2)) | 
| 77 |  | 2re 12341 | . . . . . . . . . 10
⊢ 2 ∈
ℝ | 
| 78 | 77 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → 2 ∈ ℝ) | 
| 79 |  | 2pos 12370 | . . . . . . . . . 10
⊢ 0 <
2 | 
| 80 | 79 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → 0 < 2) | 
| 81 |  | lemuldiv2 12150 | . . . . . . . . 9
⊢ ((𝐽 ∈ ℝ ∧
((log‘𝑍) /
(log‘𝐾)) ∈
ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝐽) ≤ ((log‘𝑍) / (log‘𝐾)) ↔ 𝐽 ≤ (((log‘𝑍) / (log‘𝐾)) / 2))) | 
| 82 | 36, 72, 78, 80, 81 | syl112anc 1375 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → ((2 · 𝐽) ≤ ((log‘𝑍) / (log‘𝐾)) ↔ 𝐽 ≤ (((log‘𝑍) / (log‘𝐾)) / 2))) | 
| 83 | 76, 82 | mpbird 257 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (2 · 𝐽) ≤ ((log‘𝑍) / (log‘𝐾))) | 
| 84 |  | remulcl 11241 | . . . . . . . . 9
⊢ ((2
∈ ℝ ∧ 𝐽
∈ ℝ) → (2 · 𝐽) ∈ ℝ) | 
| 85 | 77, 36, 84 | sylancr 587 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (2 · 𝐽) ∈ ℝ) | 
| 86 | 85, 71, 21 | lemuldivd 13127 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (((2 · 𝐽) · (log‘𝐾)) ≤ (log‘𝑍) ↔ (2 · 𝐽) ≤ ((log‘𝑍) / (log‘𝐾)))) | 
| 87 | 83, 86 | mpbird 257 | . . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → ((2 · 𝐽) · (log‘𝐾)) ≤ (log‘𝑍)) | 
| 88 | 64, 87 | eqbrtrd 5164 | . . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (log‘((𝐾↑𝐽)↑2)) ≤ (log‘𝑍)) | 
| 89 |  | rpexpcl 14122 | . . . . . . 7
⊢ (((𝐾↑𝐽) ∈ ℝ+ ∧ 2 ∈
ℤ) → ((𝐾↑𝐽)↑2) ∈
ℝ+) | 
| 90 | 51, 56, 89 | sylancl 586 | . . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → ((𝐾↑𝐽)↑2) ∈
ℝ+) | 
| 91 | 90, 70 | logled 26670 | . . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (((𝐾↑𝐽)↑2) ≤ 𝑍 ↔ (log‘((𝐾↑𝐽)↑2)) ≤ (log‘𝑍))) | 
| 92 | 88, 91 | mpbird 257 | . . . 4
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → ((𝐾↑𝐽)↑2) ≤ 𝑍) | 
| 93 | 70 | rprege0d 13085 | . . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (𝑍 ∈ ℝ ∧ 0 ≤ 𝑍)) | 
| 94 |  | resqrtth 15295 | . . . . 5
⊢ ((𝑍 ∈ ℝ ∧ 0 ≤
𝑍) →
((√‘𝑍)↑2)
= 𝑍) | 
| 95 | 93, 94 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → ((√‘𝑍)↑2) = 𝑍) | 
| 96 | 92, 95 | breqtrrd 5170 | . . 3
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → ((𝐾↑𝐽)↑2) ≤ ((√‘𝑍)↑2)) | 
| 97 | 51 | rprege0d 13085 | . . . 4
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → ((𝐾↑𝐽) ∈ ℝ ∧ 0 ≤ (𝐾↑𝐽))) | 
| 98 | 70 | rpsqrtcld 15451 | . . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (√‘𝑍) ∈
ℝ+) | 
| 99 | 98 | rprege0d 13085 | . . . 4
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → ((√‘𝑍) ∈ ℝ ∧ 0 ≤
(√‘𝑍))) | 
| 100 |  | le2sq 14175 | . . . 4
⊢ ((((𝐾↑𝐽) ∈ ℝ ∧ 0 ≤ (𝐾↑𝐽)) ∧ ((√‘𝑍) ∈ ℝ ∧ 0 ≤
(√‘𝑍))) →
((𝐾↑𝐽) ≤ (√‘𝑍) ↔ ((𝐾↑𝐽)↑2) ≤ ((√‘𝑍)↑2))) | 
| 101 | 97, 99, 100 | syl2anc 584 | . . 3
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → ((𝐾↑𝐽) ≤ (√‘𝑍) ↔ ((𝐾↑𝐽)↑2) ≤ ((√‘𝑍)↑2))) | 
| 102 | 96, 101 | mpbird 257 | . 2
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (𝐾↑𝐽) ≤ (√‘𝑍)) | 
| 103 | 54, 102 | jca 511 | 1
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (𝑋 < (𝐾↑𝐽) ∧ (𝐾↑𝐽) ≤ (√‘𝑍))) |