Proof of Theorem basellem1
| Step | Hyp | Ref
| Expression |
| 1 | | elfznn 13593 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑀) → 𝐾 ∈ ℕ) |
| 2 | 1 | nnrpd 13075 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑀) → 𝐾 ∈
ℝ+) |
| 3 | | pirp 26503 |
. . . . 5
⊢ π
∈ ℝ+ |
| 4 | | rpmulcl 13058 |
. . . . 5
⊢ ((𝐾 ∈ ℝ+
∧ π ∈ ℝ+) → (𝐾 · π) ∈
ℝ+) |
| 5 | 2, 3, 4 | sylancl 586 |
. . . 4
⊢ (𝐾 ∈ (1...𝑀) → (𝐾 · π) ∈
ℝ+) |
| 6 | | basel.n |
. . . . . 6
⊢ 𝑁 = ((2 · 𝑀) + 1) |
| 7 | | 2nn 12339 |
. . . . . . . 8
⊢ 2 ∈
ℕ |
| 8 | | nnmulcl 12290 |
. . . . . . . 8
⊢ ((2
∈ ℕ ∧ 𝑀
∈ ℕ) → (2 · 𝑀) ∈ ℕ) |
| 9 | 7, 8 | mpan 690 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
ℕ) |
| 10 | 9 | peano2nnd 12283 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) + 1) ∈
ℕ) |
| 11 | 6, 10 | eqeltrid 2845 |
. . . . 5
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℕ) |
| 12 | 11 | nnrpd 13075 |
. . . 4
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℝ+) |
| 13 | | rpdivcl 13060 |
. . . 4
⊢ (((𝐾 · π) ∈
ℝ+ ∧ 𝑁
∈ ℝ+) → ((𝐾 · π) / 𝑁) ∈
ℝ+) |
| 14 | 5, 12, 13 | syl2anr 597 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → ((𝐾 · π) / 𝑁) ∈
ℝ+) |
| 15 | 14 | rpred 13077 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → ((𝐾 · π) / 𝑁) ∈ ℝ) |
| 16 | 14 | rpgt0d 13080 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → 0 < ((𝐾 · π) / 𝑁)) |
| 17 | 1 | adantl 481 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → 𝐾 ∈ ℕ) |
| 18 | | nnmulcl 12290 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℕ ∧ 2 ∈
ℕ) → (𝐾 ·
2) ∈ ℕ) |
| 19 | 17, 7, 18 | sylancl 586 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → (𝐾 · 2) ∈
ℕ) |
| 20 | 19 | nnred 12281 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → (𝐾 · 2) ∈
ℝ) |
| 21 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → (2 · 𝑀) ∈ ℕ) |
| 22 | 21 | nnred 12281 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → (2 · 𝑀) ∈ ℝ) |
| 23 | 11 | adantr 480 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → 𝑁 ∈ ℕ) |
| 24 | 23 | nnred 12281 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → 𝑁 ∈ ℝ) |
| 25 | 6, 24 | eqeltrrid 2846 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → ((2 · 𝑀) + 1) ∈ ℝ) |
| 26 | 17 | nncnd 12282 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → 𝐾 ∈ ℂ) |
| 27 | | 2cn 12341 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
| 28 | | mulcom 11241 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℂ ∧ 2 ∈
ℂ) → (𝐾 ·
2) = (2 · 𝐾)) |
| 29 | 26, 27, 28 | sylancl 586 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → (𝐾 · 2) = (2 · 𝐾)) |
| 30 | | elfzle2 13568 |
. . . . . . . . 9
⊢ (𝐾 ∈ (1...𝑀) → 𝐾 ≤ 𝑀) |
| 31 | 30 | adantl 481 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → 𝐾 ≤ 𝑀) |
| 32 | 17 | nnred 12281 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → 𝐾 ∈ ℝ) |
| 33 | | nnre 12273 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
| 34 | 33 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → 𝑀 ∈ ℝ) |
| 35 | | 2re 12340 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
| 36 | | 2pos 12369 |
. . . . . . . . . . 11
⊢ 0 <
2 |
| 37 | 35, 36 | pm3.2i 470 |
. . . . . . . . . 10
⊢ (2 ∈
ℝ ∧ 0 < 2) |
| 38 | 37 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → (2 ∈ ℝ ∧ 0 <
2)) |
| 39 | | lemul2 12120 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → (𝐾 ≤ 𝑀 ↔ (2 · 𝐾) ≤ (2 · 𝑀))) |
| 40 | 32, 34, 38, 39 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → (𝐾 ≤ 𝑀 ↔ (2 · 𝐾) ≤ (2 · 𝑀))) |
| 41 | 31, 40 | mpbid 232 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → (2 · 𝐾) ≤ (2 · 𝑀)) |
| 42 | 29, 41 | eqbrtrd 5165 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → (𝐾 · 2) ≤ (2 · 𝑀)) |
| 43 | 22 | ltp1d 12198 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → (2 · 𝑀) < ((2 · 𝑀) + 1)) |
| 44 | 20, 22, 25, 42, 43 | lelttrd 11419 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → (𝐾 · 2) < ((2 · 𝑀) + 1)) |
| 45 | 44, 6 | breqtrrdi 5185 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → (𝐾 · 2) < 𝑁) |
| 46 | 19 | nngt0d 12315 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → 0 < (𝐾 · 2)) |
| 47 | 23 | nngt0d 12315 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → 0 < 𝑁) |
| 48 | | pire 26500 |
. . . . . 6
⊢ π
∈ ℝ |
| 49 | | remulcl 11240 |
. . . . . 6
⊢ ((𝐾 ∈ ℝ ∧ π
∈ ℝ) → (𝐾
· π) ∈ ℝ) |
| 50 | 32, 48, 49 | sylancl 586 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → (𝐾 · π) ∈
ℝ) |
| 51 | 5 | adantl 481 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → (𝐾 · π) ∈
ℝ+) |
| 52 | 51 | rpgt0d 13080 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → 0 < (𝐾 · π)) |
| 53 | | ltdiv2 12154 |
. . . . 5
⊢ ((((𝐾 · 2) ∈ ℝ
∧ 0 < (𝐾 ·
2)) ∧ (𝑁 ∈ ℝ
∧ 0 < 𝑁) ∧
((𝐾 · π) ∈
ℝ ∧ 0 < (𝐾
· π))) → ((𝐾
· 2) < 𝑁 ↔
((𝐾 · π) / 𝑁) < ((𝐾 · π) / (𝐾 · 2)))) |
| 54 | 20, 46, 24, 47, 50, 52, 53 | syl222anc 1388 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → ((𝐾 · 2) < 𝑁 ↔ ((𝐾 · π) / 𝑁) < ((𝐾 · π) / (𝐾 · 2)))) |
| 55 | 45, 54 | mpbid 232 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → ((𝐾 · π) / 𝑁) < ((𝐾 · π) / (𝐾 · 2))) |
| 56 | | picn 26501 |
. . . . 5
⊢ π
∈ ℂ |
| 57 | 56 | a1i 11 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → π ∈
ℂ) |
| 58 | | 2cnne0 12476 |
. . . . 5
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
| 59 | 58 | a1i 11 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → (2 ∈ ℂ ∧ 2 ≠
0)) |
| 60 | 17 | nnne0d 12316 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → 𝐾 ≠ 0) |
| 61 | | divcan5 11969 |
. . . 4
⊢ ((π
∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐾 ∈ ℂ ∧ 𝐾 ≠ 0)) → ((𝐾 · π) / (𝐾 · 2)) = (π / 2)) |
| 62 | 57, 59, 26, 60, 61 | syl112anc 1376 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → ((𝐾 · π) / (𝐾 · 2)) = (π / 2)) |
| 63 | 55, 62 | breqtrd 5169 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → ((𝐾 · π) / 𝑁) < (π / 2)) |
| 64 | | 0xr 11308 |
. . 3
⊢ 0 ∈
ℝ* |
| 65 | | rehalfcl 12492 |
. . . 4
⊢ (π
∈ ℝ → (π / 2) ∈ ℝ) |
| 66 | | rexr 11307 |
. . . 4
⊢ ((π /
2) ∈ ℝ → (π / 2) ∈
ℝ*) |
| 67 | 48, 65, 66 | mp2b 10 |
. . 3
⊢ (π /
2) ∈ ℝ* |
| 68 | | elioo2 13428 |
. . 3
⊢ ((0
∈ ℝ* ∧ (π / 2) ∈ ℝ*) →
(((𝐾 · π) / 𝑁) ∈ (0(,)(π / 2)) ↔
(((𝐾 · π) / 𝑁) ∈ ℝ ∧ 0 <
((𝐾 · π) / 𝑁) ∧ ((𝐾 · π) / 𝑁) < (π / 2)))) |
| 69 | 64, 67, 68 | mp2an 692 |
. 2
⊢ (((𝐾 · π) / 𝑁) ∈ (0(,)(π / 2)) ↔
(((𝐾 · π) / 𝑁) ∈ ℝ ∧ 0 <
((𝐾 · π) / 𝑁) ∧ ((𝐾 · π) / 𝑁) < (π / 2))) |
| 70 | 15, 16, 63, 69 | syl3anbrc 1344 |
1
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → ((𝐾 · π) / 𝑁) ∈ (0(,)(π / 2))) |