| Step | Hyp | Ref
| Expression |
| 1 | | lgseisen.1 |
. . 3
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
| 2 | | lgseisen.2 |
. . 3
⊢ (𝜑 → 𝑄 ∈ (ℙ ∖
{2})) |
| 3 | | lgseisen.3 |
. . 3
⊢ (𝜑 → 𝑃 ≠ 𝑄) |
| 4 | 1, 2, 3 | lgseisen 27423 |
. 2
⊢ (𝜑 → (𝑄 /L 𝑃) = (-1↑Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 5 | | lgsquad.4 |
. . . . . 6
⊢ 𝑀 = ((𝑃 − 1) / 2) |
| 6 | 5 | oveq2i 7442 |
. . . . 5
⊢
(1...𝑀) =
(1...((𝑃 − 1) /
2)) |
| 7 | 6 | sumeq1i 15733 |
. . . 4
⊢
Σ𝑢 ∈
(1...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) |
| 8 | 1, 5 | gausslemma2dlem0b 27401 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 9 | 8 | nnred 12281 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 10 | 9 | rehalfcld 12513 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 / 2) ∈ ℝ) |
| 11 | 10 | flcld 13838 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈
ℤ) |
| 12 | 11 | zred 12722 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈
ℝ) |
| 13 | 12 | ltp1d 12198 |
. . . . . 6
⊢ (𝜑 → (⌊‘(𝑀 / 2)) <
((⌊‘(𝑀 / 2)) +
1)) |
| 14 | | fzdisj 13591 |
. . . . . 6
⊢
((⌊‘(𝑀 /
2)) < ((⌊‘(𝑀
/ 2)) + 1) → ((1...(⌊‘(𝑀 / 2))) ∩ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = ∅) |
| 15 | 13, 14 | syl 17 |
. . . . 5
⊢ (𝜑 →
((1...(⌊‘(𝑀 /
2))) ∩ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = ∅) |
| 16 | 8 | nnrpd 13075 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈
ℝ+) |
| 17 | 16 | rphalfcld 13089 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 / 2) ∈
ℝ+) |
| 18 | 17 | rpge0d 13081 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (𝑀 / 2)) |
| 19 | | flge0nn0 13860 |
. . . . . . . . 9
⊢ (((𝑀 / 2) ∈ ℝ ∧ 0
≤ (𝑀 / 2)) →
(⌊‘(𝑀 / 2))
∈ ℕ0) |
| 20 | 10, 18, 19 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈
ℕ0) |
| 21 | 8 | nnnn0d 12587 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
| 22 | | rphalflt 13064 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℝ+
→ (𝑀 / 2) < 𝑀) |
| 23 | 16, 22 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 / 2) < 𝑀) |
| 24 | 8 | nnzd 12640 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 25 | | fllt 13846 |
. . . . . . . . . . 11
⊢ (((𝑀 / 2) ∈ ℝ ∧ 𝑀 ∈ ℤ) → ((𝑀 / 2) < 𝑀 ↔ (⌊‘(𝑀 / 2)) < 𝑀)) |
| 26 | 10, 24, 25 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 / 2) < 𝑀 ↔ (⌊‘(𝑀 / 2)) < 𝑀)) |
| 27 | 23, 26 | mpbid 232 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘(𝑀 / 2)) < 𝑀) |
| 28 | 12, 9, 27 | ltled 11409 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ≤ 𝑀) |
| 29 | | elfz2nn0 13658 |
. . . . . . . 8
⊢
((⌊‘(𝑀 /
2)) ∈ (0...𝑀) ↔
((⌊‘(𝑀 / 2))
∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧
(⌊‘(𝑀 / 2))
≤ 𝑀)) |
| 30 | 20, 21, 28, 29 | syl3anbrc 1344 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈ (0...𝑀)) |
| 31 | | nn0uz 12920 |
. . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) |
| 32 | 21, 31 | eleqtrdi 2851 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
| 33 | | elfzp12 13643 |
. . . . . . . 8
⊢ (𝑀 ∈
(ℤ≥‘0) → ((⌊‘(𝑀 / 2)) ∈ (0...𝑀) ↔ ((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀)))) |
| 34 | 32, 33 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((⌊‘(𝑀 / 2)) ∈ (0...𝑀) ↔ ((⌊‘(𝑀 / 2)) = 0 ∨
(⌊‘(𝑀 / 2))
∈ ((0 + 1)...𝑀)))) |
| 35 | 30, 34 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → ((⌊‘(𝑀 / 2)) = 0 ∨
(⌊‘(𝑀 / 2))
∈ ((0 + 1)...𝑀))) |
| 36 | | un0 4394 |
. . . . . . . . 9
⊢
((1...𝑀) ∪
∅) = (1...𝑀) |
| 37 | | uncom 4158 |
. . . . . . . . 9
⊢
((1...𝑀) ∪
∅) = (∅ ∪ (1...𝑀)) |
| 38 | 36, 37 | eqtr3i 2767 |
. . . . . . . 8
⊢
(1...𝑀) = (∅
∪ (1...𝑀)) |
| 39 | | oveq2 7439 |
. . . . . . . . . 10
⊢
((⌊‘(𝑀 /
2)) = 0 → (1...(⌊‘(𝑀 / 2))) = (1...0)) |
| 40 | | fz10 13585 |
. . . . . . . . . 10
⊢ (1...0) =
∅ |
| 41 | 39, 40 | eqtrdi 2793 |
. . . . . . . . 9
⊢
((⌊‘(𝑀 /
2)) = 0 → (1...(⌊‘(𝑀 / 2))) = ∅) |
| 42 | | oveq1 7438 |
. . . . . . . . . . 11
⊢
((⌊‘(𝑀 /
2)) = 0 → ((⌊‘(𝑀 / 2)) + 1) = (0 + 1)) |
| 43 | | 0p1e1 12388 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
| 44 | 42, 43 | eqtrdi 2793 |
. . . . . . . . . 10
⊢
((⌊‘(𝑀 /
2)) = 0 → ((⌊‘(𝑀 / 2)) + 1) = 1) |
| 45 | 44 | oveq1d 7446 |
. . . . . . . . 9
⊢
((⌊‘(𝑀 /
2)) = 0 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) = (1...𝑀)) |
| 46 | 41, 45 | uneq12d 4169 |
. . . . . . . 8
⊢
((⌊‘(𝑀 /
2)) = 0 → ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = (∅ ∪ (1...𝑀))) |
| 47 | 38, 46 | eqtr4id 2796 |
. . . . . . 7
⊢
((⌊‘(𝑀 /
2)) = 0 → (1...𝑀) =
((1...(⌊‘(𝑀 /
2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))) |
| 48 | | fzsplit 13590 |
. . . . . . . 8
⊢
((⌊‘(𝑀 /
2)) ∈ (1...𝑀) →
(1...𝑀) =
((1...(⌊‘(𝑀 /
2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))) |
| 49 | 43 | oveq1i 7441 |
. . . . . . . 8
⊢ ((0 +
1)...𝑀) = (1...𝑀) |
| 50 | 48, 49 | eleq2s 2859 |
. . . . . . 7
⊢
((⌊‘(𝑀 /
2)) ∈ ((0 + 1)...𝑀)
→ (1...𝑀) =
((1...(⌊‘(𝑀 /
2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))) |
| 51 | 47, 50 | jaoi 858 |
. . . . . 6
⊢
(((⌊‘(𝑀
/ 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀)) → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))) |
| 52 | 35, 51 | syl 17 |
. . . . 5
⊢ (𝜑 → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))) |
| 53 | | fzfid 14014 |
. . . . 5
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
| 54 | 2 | gausslemma2dlem0a 27400 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ ℕ) |
| 55 | 54 | nnred 12281 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄 ∈ ℝ) |
| 56 | 1 | gausslemma2dlem0a 27400 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℕ) |
| 57 | 55, 56 | nndivred 12320 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄 / 𝑃) ∈ ℝ) |
| 58 | 57 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (𝑄 / 𝑃) ∈ ℝ) |
| 59 | | 2nn 12339 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
| 60 | | elfznn 13593 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (1...𝑀) → 𝑢 ∈ ℕ) |
| 61 | 60 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → 𝑢 ∈ ℕ) |
| 62 | | nnmulcl 12290 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ 𝑢
∈ ℕ) → (2 · 𝑢) ∈ ℕ) |
| 63 | 59, 61, 62 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℕ) |
| 64 | 63 | nnred 12281 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℝ) |
| 65 | 58, 64 | remulcld 11291 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) |
| 66 | 54 | nnrpd 13075 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈
ℝ+) |
| 67 | 56 | nnrpd 13075 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈
ℝ+) |
| 68 | 66, 67 | rpdivcld 13094 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑄 / 𝑃) ∈
ℝ+) |
| 69 | 68 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (𝑄 / 𝑃) ∈
ℝ+) |
| 70 | 63 | nnrpd 13075 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈
ℝ+) |
| 71 | 69, 70 | rpmulcld 13093 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈
ℝ+) |
| 72 | 71 | rpge0d 13081 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → 0 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))) |
| 73 | | flge0nn0 13860 |
. . . . . . 7
⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 0 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
| 74 | 65, 72, 73 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
| 75 | 74 | nn0cnd 12589 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ) |
| 76 | 15, 52, 53, 75 | fsumsplit 15777 |
. . . 4
⊢ (𝜑 → Σ𝑢 ∈ (1...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 77 | 7, 76 | eqtr3id 2791 |
. . 3
⊢ (𝜑 → Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 78 | 77 | oveq2d 7447 |
. 2
⊢ (𝜑 → (-1↑Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 79 | | neg1cn 12380 |
. . . . 5
⊢ -1 ∈
ℂ |
| 80 | 79 | a1i 11 |
. . . 4
⊢ (𝜑 → -1 ∈
ℂ) |
| 81 | | fzfid 14014 |
. . . . 5
⊢ (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin) |
| 82 | | ssun2 4179 |
. . . . . . . 8
⊢
(((⌊‘(𝑀
/ 2)) + 1)...𝑀) ⊆
((1...(⌊‘(𝑀 /
2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) |
| 83 | 82, 52 | sseqtrrid 4027 |
. . . . . . 7
⊢ (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ⊆ (1...𝑀)) |
| 84 | 83 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ (1...𝑀)) |
| 85 | 84, 74 | syldan 591 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
| 86 | 81, 85 | fsumnn0cl 15772 |
. . . 4
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
| 87 | | fzfid 14014 |
. . . . 5
⊢ (𝜑 → (1...(⌊‘(𝑀 / 2))) ∈
Fin) |
| 88 | | ssun1 4178 |
. . . . . . . 8
⊢
(1...(⌊‘(𝑀 / 2))) ⊆ ((1...(⌊‘(𝑀 / 2))) ∪
(((⌊‘(𝑀 / 2)) +
1)...𝑀)) |
| 89 | 88, 52 | sseqtrrid 4027 |
. . . . . . 7
⊢ (𝜑 → (1...(⌊‘(𝑀 / 2))) ⊆ (1...𝑀)) |
| 90 | 89 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ (1...𝑀)) |
| 91 | 90, 74 | syldan 591 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
| 92 | 87, 91 | fsumnn0cl 15772 |
. . . 4
⊢ (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
| 93 | 80, 86, 92 | expaddd 14188 |
. . 3
⊢ (𝜑 → (-1↑(Σ𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 94 | | fzfid 14014 |
. . . . . . . . 9
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
| 95 | | xpfi 9358 |
. . . . . . . . 9
⊢
(((1...𝑀) ∈ Fin
∧ (1...𝑁) ∈ Fin)
→ ((1...𝑀) ×
(1...𝑁)) ∈
Fin) |
| 96 | 53, 94, 95 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ((1...𝑀) × (1...𝑁)) ∈ Fin) |
| 97 | | lgsquad.6 |
. . . . . . . . 9
⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} |
| 98 | | opabssxp 5778 |
. . . . . . . . 9
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁)) |
| 99 | 97, 98 | eqsstri 4030 |
. . . . . . . 8
⊢ 𝑆 ⊆ ((1...𝑀) × (1...𝑁)) |
| 100 | | ssfi 9213 |
. . . . . . . 8
⊢
((((1...𝑀) ×
(1...𝑁)) ∈ Fin ∧
𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin) |
| 101 | 96, 99, 100 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ Fin) |
| 102 | | ssrab2 4080 |
. . . . . . 7
⊢ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ⊆ 𝑆 |
| 103 | | ssfi 9213 |
. . . . . . 7
⊢ ((𝑆 ∈ Fin ∧ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ⊆ 𝑆) → {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
| 104 | 101, 102,
103 | sylancl 586 |
. . . . . 6
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
| 105 | | hashcl 14395 |
. . . . . 6
⊢ ({𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈ Fin
→ (♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)}) ∈
ℕ0) |
| 106 | 104, 105 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) ∈
ℕ0) |
| 107 | | ssrab2 4080 |
. . . . . . 7
⊢ {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ⊆ 𝑆 |
| 108 | | ssfi 9213 |
. . . . . . 7
⊢ ((𝑆 ∈ Fin ∧ {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ⊆ 𝑆) → {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
| 109 | 101, 107,
108 | sylancl 586 |
. . . . . 6
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
| 110 | | hashcl 14395 |
. . . . . 6
⊢ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∈ Fin
→ (♯‘{𝑧
∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)})
∈ ℕ0) |
| 111 | 109, 110 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)}) ∈
ℕ0) |
| 112 | 80, 106, 111 | expaddd 14188 |
. . . 4
⊢ (𝜑 →
(-1↑((♯‘{𝑧
∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)})
+ (♯‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)}))) = ((-1↑(♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)})) ·
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})))) |
| 113 | 90, 63 | syldan 591 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 ·
𝑢) ∈
ℕ) |
| 114 | | fzfid 14014 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) ∈
Fin) |
| 115 | | xpsnen2g 9105 |
. . . . . . . . . . 11
⊢ (((2
· 𝑢) ∈ ℕ
∧ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ Fin) → ({(2 · 𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) ≈
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) |
| 116 | 113, 114,
115 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 ·
𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) ≈
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) |
| 117 | | hasheni 14387 |
. . . . . . . . . 10
⊢ (({(2
· 𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) ≈
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) →
(♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) =
(♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 118 | 116, 117 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) =
(♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 119 | | ssrab2 4080 |
. . . . . . . . . . . . 13
⊢ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ⊆ 𝑆 |
| 120 | 97 | relopabiv 5830 |
. . . . . . . . . . . . 13
⊢ Rel 𝑆 |
| 121 | | relss 5791 |
. . . . . . . . . . . . 13
⊢ ({𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ⊆ 𝑆 → (Rel 𝑆 → Rel {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) |
| 122 | 119, 120,
121 | mp2 9 |
. . . . . . . . . . . 12
⊢ Rel
{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} |
| 123 | | relxp 5703 |
. . . . . . . . . . . 12
⊢ Rel ({(2
· 𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) |
| 124 | 97 | eleq2i 2833 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ 𝑆 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}) |
| 125 | | opabidw 5529 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) |
| 126 | 124, 125 | bitri 275 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ 𝑆 ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) |
| 127 | | anass 468 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))))) |
| 128 | 113 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) ∈
ℕ) |
| 129 | 128 | nnred 12281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) ∈
ℝ) |
| 130 | 56 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℕ) |
| 131 | 130 | nnred 12281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℝ) |
| 132 | 131 | rehalfcld 12513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 / 2) ∈
ℝ) |
| 133 | 9 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑀 ∈
ℝ) |
| 134 | 133 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑀 ∈
ℝ) |
| 135 | | elfzle2 13568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑢 ∈
(1...(⌊‘(𝑀 /
2))) → 𝑢 ≤
(⌊‘(𝑀 /
2))) |
| 136 | 135 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ≤ (⌊‘(𝑀 / 2))) |
| 137 | 133 | rehalfcld 12513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑀 / 2) ∈
ℝ) |
| 138 | | elfzelz 13564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑢 ∈
(1...(⌊‘(𝑀 /
2))) → 𝑢 ∈
ℤ) |
| 139 | 138 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈
ℤ) |
| 140 | | flge 13845 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑀 / 2) ∈ ℝ ∧ 𝑢 ∈ ℤ) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2)))) |
| 141 | 137, 139,
140 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2)))) |
| 142 | 136, 141 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ≤ (𝑀 / 2)) |
| 143 | | elfznn 13593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑢 ∈
(1...(⌊‘(𝑀 /
2))) → 𝑢 ∈
ℕ) |
| 144 | 143 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈
ℕ) |
| 145 | 144 | nnred 12281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈
ℝ) |
| 146 | | 2re 12340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 2 ∈
ℝ |
| 147 | 146 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 2 ∈
ℝ) |
| 148 | | 2pos 12369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 0 <
2 |
| 149 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 0 <
2) |
| 150 | | lemuldiv2 12149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑢 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → ((2 · 𝑢) ≤ 𝑀 ↔ 𝑢 ≤ (𝑀 / 2))) |
| 151 | 145, 133,
147, 149, 150 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 ·
𝑢) ≤ 𝑀 ↔ 𝑢 ≤ (𝑀 / 2))) |
| 152 | 142, 151 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 ·
𝑢) ≤ 𝑀) |
| 153 | 152 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) ≤ 𝑀) |
| 154 | 131 | ltm1d 12200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 − 1) < 𝑃) |
| 155 | | peano2rem 11576 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈
ℝ) |
| 156 | 131, 155 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 − 1) ∈
ℝ) |
| 157 | 146 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ∈
ℝ) |
| 158 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 <
2) |
| 159 | | ltdiv1 12132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑃 − 1) ∈ ℝ ∧
𝑃 ∈ ℝ ∧ (2
∈ ℝ ∧ 0 < 2)) → ((𝑃 − 1) < 𝑃 ↔ ((𝑃 − 1) / 2) < (𝑃 / 2))) |
| 160 | 156, 131,
157, 158, 159 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 − 1) < 𝑃 ↔ ((𝑃 − 1) / 2) < (𝑃 / 2))) |
| 161 | 154, 160 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 − 1) / 2) < (𝑃 / 2)) |
| 162 | 5, 161 | eqbrtrid 5178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑀 < (𝑃 / 2)) |
| 163 | 129, 134,
132, 153, 162 | lelttrd 11419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) < (𝑃 / 2)) |
| 164 | 130 | nnrpd 13075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℝ+) |
| 165 | | rphalflt 13064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℝ+
→ (𝑃 / 2) < 𝑃) |
| 166 | 164, 165 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 / 2) < 𝑃) |
| 167 | 129, 132,
131, 163, 166 | lttrd 11422 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) < 𝑃) |
| 168 | 129, 131 | ltnled 11408 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((2
· 𝑢) < 𝑃 ↔ ¬ 𝑃 ≤ (2 · 𝑢))) |
| 169 | 167, 168 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬
𝑃 ≤ (2 · 𝑢)) |
| 170 | 1 | eldifad 3963 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑃 ∈ ℙ) |
| 171 | 170 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℙ) |
| 172 | | prmz 16712 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
| 173 | 171, 172 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℤ) |
| 174 | | dvdsle 16347 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃 ∈ ℤ ∧ (2
· 𝑢) ∈ ℕ)
→ (𝑃 ∥ (2
· 𝑢) → 𝑃 ≤ (2 · 𝑢))) |
| 175 | 173, 128,
174 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ (2 · 𝑢) → 𝑃 ≤ (2 · 𝑢))) |
| 176 | 169, 175 | mtod 198 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬
𝑃 ∥ (2 · 𝑢)) |
| 177 | 2 | eldifad 3963 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑄 ∈ ℙ) |
| 178 | | prmrp 16749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄)) |
| 179 | 170, 177,
178 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄)) |
| 180 | 3, 179 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑃 gcd 𝑄) = 1) |
| 181 | 180 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 gcd 𝑄) = 1) |
| 182 | 177 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈
ℙ) |
| 183 | | prmz 16712 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℤ) |
| 184 | 182, 183 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈
ℤ) |
| 185 | 128 | nnzd 12640 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) ∈
ℤ) |
| 186 | | coprmdvds 16690 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ (2
· 𝑢) ∈ ℤ)
→ ((𝑃 ∥ (𝑄 · (2 · 𝑢)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑢))) |
| 187 | 173, 184,
185, 186 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 ∥ (𝑄 · (2 · 𝑢)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑢))) |
| 188 | 181, 187 | mpan2d 694 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ (𝑄 · (2 · 𝑢)) → 𝑃 ∥ (2 · 𝑢))) |
| 189 | 176, 188 | mtod 198 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬
𝑃 ∥ (𝑄 · (2 · 𝑢))) |
| 190 | | nnz 12634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
| 191 | 190 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈
ℤ) |
| 192 | | dvdsmul2 16316 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑃 ∥ (𝑦 · 𝑃)) |
| 193 | 191, 173,
192 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∥ (𝑦 · 𝑃)) |
| 194 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑄 · (2 · 𝑢)) = (𝑦 · 𝑃) → (𝑃 ∥ (𝑄 · (2 · 𝑢)) ↔ 𝑃 ∥ (𝑦 · 𝑃))) |
| 195 | 193, 194 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 · (2 · 𝑢)) = (𝑦 · 𝑃) → 𝑃 ∥ (𝑄 · (2 · 𝑢)))) |
| 196 | 195 | necon3bd 2954 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (¬
𝑃 ∥ (𝑄 · (2 · 𝑢)) → (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃))) |
| 197 | 189, 196 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃)) |
| 198 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈
ℕ) |
| 199 | 198, 130 | nnmulcld 12319 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℕ) |
| 200 | 199 | nnred 12281 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℝ) |
| 201 | 54 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑄 ∈
ℕ) |
| 202 | 201, 113 | nnmulcld 12319 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑄 · (2 · 𝑢)) ∈
ℕ) |
| 203 | 202 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈
ℕ) |
| 204 | 203 | nnred 12281 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈
ℝ) |
| 205 | 200, 204 | ltlend 11406 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃)))) |
| 206 | 197, 205 | mpbiran2d 708 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ (𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)))) |
| 207 | | nnre 12273 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
| 208 | 207 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈
ℝ) |
| 209 | 130 | nngt0d 12315 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 <
𝑃) |
| 210 | | lemuldiv 12148 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 <
𝑃)) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))) |
| 211 | 208, 204,
131, 209, 210 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))) |
| 212 | 201 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈
ℕ) |
| 213 | 212 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈
ℂ) |
| 214 | 128 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) ∈
ℂ) |
| 215 | 130 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℂ) |
| 216 | 130 | nnne0d 12316 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ≠ 0) |
| 217 | 213, 214,
215, 216 | div23d 12080 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 · (2 · 𝑢)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑢))) |
| 218 | 217 | breq2d 5155 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃) ↔ 𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))) |
| 219 | 206, 211,
218 | 3bitrd 305 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))) |
| 220 | 212 | nnred 12281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈
ℝ) |
| 221 | 212 | nngt0d 12315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 <
𝑄) |
| 222 | | ltmul2 12118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((2
· 𝑢) ∈ ℝ
∧ (𝑃 / 2) ∈
ℝ ∧ (𝑄 ∈
ℝ ∧ 0 < 𝑄))
→ ((2 · 𝑢) <
(𝑃 / 2) ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2)))) |
| 223 | 129, 132,
220, 221, 222 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((2
· 𝑢) < (𝑃 / 2) ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2)))) |
| 224 | 163, 223 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2))) |
| 225 | | 2cnd 12344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ∈
ℂ) |
| 226 | | 2ne0 12370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 2 ≠
0 |
| 227 | 226 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ≠
0) |
| 228 | | divass 11940 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → ((𝑄 · 𝑃) / 2) = (𝑄 · (𝑃 / 2))) |
| 229 | | div23 11941 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → ((𝑄 · 𝑃) / 2) = ((𝑄 / 2) · 𝑃)) |
| 230 | 228, 229 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → (𝑄 · (𝑃 / 2)) = ((𝑄 / 2) · 𝑃)) |
| 231 | 213, 215,
225, 227, 230 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (𝑃 / 2)) = ((𝑄 / 2) · 𝑃)) |
| 232 | 224, 231 | breqtrd 5169 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) |
| 233 | 220 | rehalfcld 12513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 / 2) ∈
ℝ) |
| 234 | 233, 131 | remulcld 11291 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 2) · 𝑃) ∈ ℝ) |
| 235 | | lttr 11337 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑦 · 𝑃) ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ ((𝑄 / 2) · 𝑃) ∈ ℝ) → (((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃))) |
| 236 | 200, 204,
234, 235 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃))) |
| 237 | 232, 236 | mpan2d 694 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃))) |
| 238 | | ltmul1 12117 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ (𝑄 / 2) ∈ ℝ ∧
(𝑃 ∈ ℝ ∧ 0
< 𝑃)) → (𝑦 < (𝑄 / 2) ↔ (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃))) |
| 239 | 208, 233,
131, 209, 238 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 / 2) ↔ (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃))) |
| 240 | 237, 239 | sylibrd 259 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 < (𝑄 / 2))) |
| 241 | | peano2rem 11576 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑄 ∈ ℝ → (𝑄 − 1) ∈
ℝ) |
| 242 | 220, 241 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − 1) ∈
ℝ) |
| 243 | 242 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − 1) ∈
ℂ) |
| 244 | 213, 243,
225, 227 | divsubdird 12082 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = ((𝑄 / 2) − ((𝑄 − 1) / 2))) |
| 245 | | lgsquad.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝑁 = ((𝑄 − 1) / 2) |
| 246 | 245 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑄 / 2) − 𝑁) = ((𝑄 / 2) − ((𝑄 − 1) / 2)) |
| 247 | 244, 246 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = ((𝑄 / 2) − 𝑁)) |
| 248 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 1 ∈
ℂ |
| 249 | | nncan 11538 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑄 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑄 −
(𝑄 − 1)) =
1) |
| 250 | 213, 248,
249 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − (𝑄 − 1)) = 1) |
| 251 | 250 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = (1 /
2)) |
| 252 | | halflt1 12484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (1 / 2)
< 1 |
| 253 | 251, 252 | eqbrtrdi 5182 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) < 1) |
| 254 | 247, 253 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 2) − 𝑁) < 1) |
| 255 | 2, 245 | gausslemma2dlem0b 27401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 256 | 255 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈
ℕ) |
| 257 | 256 | nnred 12281 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈
ℝ) |
| 258 | | 1red 11262 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 1 ∈
ℝ) |
| 259 | 233, 257,
258 | ltsubadd2d 11861 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (((𝑄 / 2) − 𝑁) < 1 ↔ (𝑄 / 2) < (𝑁 + 1))) |
| 260 | 254, 259 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 / 2) < (𝑁 + 1)) |
| 261 | | peano2re 11434 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈
ℝ) |
| 262 | 257, 261 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑁 + 1) ∈
ℝ) |
| 263 | | lttr 11337 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ (𝑄 / 2) ∈ ℝ ∧
(𝑁 + 1) ∈ ℝ)
→ ((𝑦 < (𝑄 / 2) ∧ (𝑄 / 2) < (𝑁 + 1)) → 𝑦 < (𝑁 + 1))) |
| 264 | 208, 233,
262, 263 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 < (𝑄 / 2) ∧ (𝑄 / 2) < (𝑁 + 1)) → 𝑦 < (𝑁 + 1))) |
| 265 | 260, 264 | mpan2d 694 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 / 2) → 𝑦 < (𝑁 + 1))) |
| 266 | 240, 265 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 < (𝑁 + 1))) |
| 267 | | nnleltp1 12673 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑦 ≤ 𝑁 ↔ 𝑦 < (𝑁 + 1))) |
| 268 | 198, 256,
267 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ 𝑁 ↔ 𝑦 < (𝑁 + 1))) |
| 269 | 266, 268 | sylibrd 259 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 ≤ 𝑁)) |
| 270 | 269 | pm4.71rd 562 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))))) |
| 271 | 90, 65 | syldan 591 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) |
| 272 | | flge 13845 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑦 ∈ ℤ) → (𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 273 | 271, 190,
272 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 274 | 219, 270,
273 | 3bitr3d 309 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 275 | 274 | pm5.32da 579 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 276 | 127, 275 | bitrid 283 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 277 | 276 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 278 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑥 = (2 · 𝑢)) |
| 279 | | nnuz 12921 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ℕ =
(ℤ≥‘1) |
| 280 | 113, 279 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 ·
𝑢) ∈
(ℤ≥‘1)) |
| 281 | 24 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑀 ∈
ℤ) |
| 282 | | elfz5 13556 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((2
· 𝑢) ∈
(ℤ≥‘1) ∧ 𝑀 ∈ ℤ) → ((2 · 𝑢) ∈ (1...𝑀) ↔ (2 · 𝑢) ≤ 𝑀)) |
| 283 | 280, 281,
282 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 ·
𝑢) ∈ (1...𝑀) ↔ (2 · 𝑢) ≤ 𝑀)) |
| 284 | 152, 283 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 ·
𝑢) ∈ (1...𝑀)) |
| 285 | 284 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (2 · 𝑢) ∈ (1...𝑀)) |
| 286 | 278, 285 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑥 ∈ (1...𝑀)) |
| 287 | 286 | biantrurd 532 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...𝑁) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)))) |
| 288 | 255 | nnzd 12640 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 289 | 288 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑁 ∈ ℤ) |
| 290 | | fznn 13632 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℤ → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁))) |
| 291 | 289, 290 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁))) |
| 292 | 287, 291 | bitr3d 281 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁))) |
| 293 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (2 · 𝑢) → (𝑥 · 𝑄) = ((2 · 𝑢) · 𝑄)) |
| 294 | 113 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 ·
𝑢) ∈
ℂ) |
| 295 | 201 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑄 ∈
ℂ) |
| 296 | 294, 295 | mulcomd 11282 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 ·
𝑢) · 𝑄) = (𝑄 · (2 · 𝑢))) |
| 297 | 293, 296 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑥 · 𝑄) = (𝑄 · (2 · 𝑢))) |
| 298 | 297 | breq2d 5155 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → ((𝑦 · 𝑃) < (𝑥 · 𝑄) ↔ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))) |
| 299 | 292, 298 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ ((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))))) |
| 300 | 271 | flcld 13838 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℤ) |
| 301 | | fznn 13632 |
. . . . . . . . . . . . . . . . . 18
⊢
((⌊‘((𝑄
/ 𝑃) · (2 ·
𝑢))) ∈ ℤ →
(𝑦 ∈
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 302 | 300, 301 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑦 ∈
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 303 | 302 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 304 | 277, 299,
303 | 3bitr4d 311 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 305 | 126, 304 | bitrid 283 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (〈𝑥, 𝑦〉 ∈ 𝑆 ↔ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 306 | 305 | pm5.32da 579 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑥 = (2 · 𝑢) ∧ 〈𝑥, 𝑦〉 ∈ 𝑆) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 307 | | vex 3484 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑥 ∈ V |
| 308 | | vex 3484 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑦 ∈ V |
| 309 | 307, 308 | op1std 8024 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) |
| 310 | 309 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((2 · 𝑢) = (1st ‘𝑧) ↔ (2 · 𝑢) = 𝑥)) |
| 311 | | eqcom 2744 |
. . . . . . . . . . . . . . . 16
⊢ ((2
· 𝑢) = 𝑥 ↔ 𝑥 = (2 · 𝑢)) |
| 312 | 310, 311 | bitrdi 287 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((2 · 𝑢) = (1st ‘𝑧) ↔ 𝑥 = (2 · 𝑢))) |
| 313 | 312 | elrab 3692 |
. . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑦〉 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ↔ (〈𝑥, 𝑦〉 ∈ 𝑆 ∧ 𝑥 = (2 · 𝑢))) |
| 314 | 313 | biancomi 462 |
. . . . . . . . . . . . 13
⊢
(〈𝑥, 𝑦〉 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ↔ (𝑥 = (2 · 𝑢) ∧ 〈𝑥, 𝑦〉 ∈ 𝑆)) |
| 315 | | opelxp 5721 |
. . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑦〉 ∈ ({(2 ·
𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) ↔ (𝑥 ∈ {(2 · 𝑢)} ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 316 | | velsn 4642 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ {(2 · 𝑢)} ↔ 𝑥 = (2 · 𝑢)) |
| 317 | 316 | anbi1i 624 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ {(2 · 𝑢)} ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 318 | 315, 317 | bitri 275 |
. . . . . . . . . . . . 13
⊢
(〈𝑥, 𝑦〉 ∈ ({(2 ·
𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 319 | 306, 314,
318 | 3bitr4g 314 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (〈𝑥, 𝑦〉 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ↔ 〈𝑥, 𝑦〉 ∈ ({(2 · 𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))))) |
| 320 | 122, 123,
319 | eqrelrdv 5802 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} = ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 321 | 320 | eqcomd 2743 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 ·
𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) = {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}) |
| 322 | 321 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (♯‘{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) |
| 323 | | hashfz1 14385 |
. . . . . . . . . 10
⊢
((⌊‘((𝑄
/ 𝑃) · (2 ·
𝑢))) ∈
ℕ0 → (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) |
| 324 | 91, 323 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) |
| 325 | 118, 322,
324 | 3eqtr3rd 2786 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (♯‘{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) |
| 326 | 325 | sumeq2dv 15738 |
. . . . . . 7
⊢ (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(♯‘{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) |
| 327 | 101 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑆 ∈ Fin) |
| 328 | | ssfi 9213 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Fin ∧ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ⊆ 𝑆) → {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ∈ Fin) |
| 329 | 327, 119,
328 | sylancl 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ∈ Fin) |
| 330 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑣 → (1st ‘𝑧) = (1st ‘𝑣)) |
| 331 | 330 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑣 → ((2 · 𝑢) = (1st ‘𝑧) ↔ (2 · 𝑢) = (1st ‘𝑣))) |
| 332 | 331 | elrab 3692 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ↔ (𝑣 ∈ 𝑆 ∧ (2 · 𝑢) = (1st ‘𝑣))) |
| 333 | 332 | simprbi 496 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} → (2 · 𝑢) = (1st ‘𝑣)) |
| 334 | 333 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → (2 · 𝑢) = (1st ‘𝑣)) |
| 335 | 334 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → ((2 · 𝑢) / 2) = ((1st ‘𝑣) / 2)) |
| 336 | 144 | nncnd 12282 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈
ℂ) |
| 337 | 336 | adantrr 717 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → 𝑢 ∈ ℂ) |
| 338 | | 2cnd 12344 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → 2 ∈
ℂ) |
| 339 | 226 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → 2 ≠ 0) |
| 340 | 337, 338,
339 | divcan3d 12048 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → ((2 · 𝑢) / 2) = 𝑢) |
| 341 | 335, 340 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → ((1st ‘𝑣) / 2) = 𝑢) |
| 342 | 341 | ralrimivva 3202 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑢 ∈ (1...(⌊‘(𝑀 / 2)))∀𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ((1st ‘𝑣) / 2) = 𝑢) |
| 343 | | invdisj 5129 |
. . . . . . . . 9
⊢
(∀𝑢 ∈
(1...(⌊‘(𝑀 /
2)))∀𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ((1st ‘𝑣) / 2) = 𝑢 → Disj 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}) |
| 344 | 342, 343 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → Disj 𝑢 ∈
(1...(⌊‘(𝑀 /
2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}) |
| 345 | 87, 329, 344 | hashiun 15858 |
. . . . . . 7
⊢ (𝜑 → (♯‘∪ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}) = Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(♯‘{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) |
| 346 | | iunrab 5052 |
. . . . . . . . 9
⊢ ∪ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} = {𝑧 ∈ 𝑆 ∣ ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧)} |
| 347 | | 2cn 12341 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
| 348 | | zcn 12618 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ℤ → 𝑢 ∈
ℂ) |
| 349 | 348 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ ℤ) → 𝑢 ∈ ℂ) |
| 350 | | mulcom 11241 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℂ ∧ 𝑢
∈ ℂ) → (2 · 𝑢) = (𝑢 · 2)) |
| 351 | 347, 349,
350 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ ℤ) → (2 · 𝑢) = (𝑢 · 2)) |
| 352 | 351 | eqeq1d 2739 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ ℤ) → ((2 · 𝑢) = (1st ‘𝑧) ↔ (𝑢 · 2) = (1st ‘𝑧))) |
| 353 | 352 | rexbidva 3177 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ ℤ (2 · 𝑢) = (1st ‘𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st
‘𝑧))) |
| 354 | 138 | anim1i 615 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈
(1...(⌊‘(𝑀 /
2))) ∧ (2 · 𝑢) =
(1st ‘𝑧))
→ (𝑢 ∈ ℤ
∧ (2 · 𝑢) =
(1st ‘𝑧))) |
| 355 | 354 | reximi2 3079 |
. . . . . . . . . . . 12
⊢
(∃𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(2 · 𝑢) =
(1st ‘𝑧)
→ ∃𝑢 ∈
ℤ (2 · 𝑢) =
(1st ‘𝑧)) |
| 356 | | simprr 773 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (2 · 𝑢) = (1st ‘𝑧)) |
| 357 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆) |
| 358 | 99, 357 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ ((1...𝑀) × (1...𝑁))) |
| 359 | | xp1st 8046 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ ((1...𝑀) × (1...𝑁)) → (1st ‘𝑧) ∈ (1...𝑀)) |
| 360 | 358, 359 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (1st ‘𝑧) ∈ (1...𝑀)) |
| 361 | 360 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (1st
‘𝑧) ∈ (1...𝑀)) |
| 362 | | elfzle2 13568 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑧) ∈ (1...𝑀) → (1st ‘𝑧) ≤ 𝑀) |
| 363 | 361, 362 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (1st
‘𝑧) ≤ 𝑀) |
| 364 | 356, 363 | eqbrtrd 5165 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (2 · 𝑢) ≤ 𝑀) |
| 365 | | zre 12617 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ ℤ → 𝑢 ∈
ℝ) |
| 366 | 365 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈ ℝ) |
| 367 | 9 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑀 ∈ ℝ) |
| 368 | 146 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 2 ∈
ℝ) |
| 369 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 0 <
2) |
| 370 | 366, 367,
368, 369, 150 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → ((2 · 𝑢) ≤ 𝑀 ↔ 𝑢 ≤ (𝑀 / 2))) |
| 371 | 364, 370 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ≤ (𝑀 / 2)) |
| 372 | 10 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (𝑀 / 2) ∈ ℝ) |
| 373 | | simprl 771 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈ ℤ) |
| 374 | 372, 373,
140 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2)))) |
| 375 | 371, 374 | mpbid 232 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ≤ (⌊‘(𝑀 / 2))) |
| 376 | | 2t0e0 12435 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
· 0) = 0 |
| 377 | | elfznn 13593 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((1st ‘𝑧) ∈ (1...𝑀) → (1st ‘𝑧) ∈
ℕ) |
| 378 | 361, 377 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (1st
‘𝑧) ∈
ℕ) |
| 379 | 356, 378 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (2 · 𝑢) ∈
ℕ) |
| 380 | 379 | nngt0d 12315 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 0 < (2 ·
𝑢)) |
| 381 | 376, 380 | eqbrtrid 5178 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (2 · 0) <
(2 · 𝑢)) |
| 382 | | 0red 11264 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 0 ∈
ℝ) |
| 383 | | ltmul2 12118 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0
∈ ℝ ∧ 𝑢
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (0 < 𝑢 ↔ (2 · 0) < (2
· 𝑢))) |
| 384 | 382, 366,
368, 369, 383 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (0 < 𝑢 ↔ (2 · 0) < (2
· 𝑢))) |
| 385 | 381, 384 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 0 < 𝑢) |
| 386 | | elnnz 12623 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ ℕ ↔ (𝑢 ∈ ℤ ∧ 0 <
𝑢)) |
| 387 | 373, 385,
386 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈ ℕ) |
| 388 | 387, 279 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈
(ℤ≥‘1)) |
| 389 | 11 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (⌊‘(𝑀 / 2)) ∈
ℤ) |
| 390 | | elfz5 13556 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈
(ℤ≥‘1) ∧ (⌊‘(𝑀 / 2)) ∈ ℤ) → (𝑢 ∈
(1...(⌊‘(𝑀 /
2))) ↔ 𝑢 ≤
(⌊‘(𝑀 /
2)))) |
| 391 | 388, 389,
390 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2)))) |
| 392 | 375, 391 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) |
| 393 | 392, 356 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st ‘𝑧))) |
| 394 | 393 | ex 412 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧)) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st ‘𝑧)))) |
| 395 | 394 | reximdv2 3164 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ ℤ (2 · 𝑢) = (1st ‘𝑧) → ∃𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(2 · 𝑢) =
(1st ‘𝑧))) |
| 396 | 355, 395 | impbid2 226 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧) ↔ ∃𝑢 ∈ ℤ (2 ·
𝑢) = (1st
‘𝑧))) |
| 397 | | 2z 12649 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℤ |
| 398 | 360 | elfzelzd 13565 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (1st ‘𝑧) ∈
ℤ) |
| 399 | | divides 16292 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℤ ∧ (1st ‘𝑧) ∈ ℤ) → (2 ∥
(1st ‘𝑧)
↔ ∃𝑢 ∈
ℤ (𝑢 · 2) =
(1st ‘𝑧))) |
| 400 | 397, 398,
399 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (2 ∥ (1st
‘𝑧) ↔
∃𝑢 ∈ ℤ
(𝑢 · 2) =
(1st ‘𝑧))) |
| 401 | 353, 396,
400 | 3bitr4d 311 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧) ↔ 2 ∥
(1st ‘𝑧))) |
| 402 | 401 | rabbidva 3443 |
. . . . . . . . 9
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧)} = {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)}) |
| 403 | 346, 402 | eqtrid 2789 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} = {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)}) |
| 404 | 403 | fveq2d 6910 |
. . . . . . 7
⊢ (𝜑 → (♯‘∪ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}) = (♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)})) |
| 405 | 326, 345,
404 | 3eqtr2d 2783 |
. . . . . 6
⊢ (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)})) |
| 406 | 405 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (-1↑Σ𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) =
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)}))) |
| 407 | 1, 2, 3, 5, 245, 97 | lgsquadlem1 27424 |
. . . . 5
⊢ (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) |
| 408 | 406, 407 | oveq12d 7449 |
. . . 4
⊢ (𝜑 → ((-1↑Σ𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) ·
(-1↑Σ𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = ((-1↑(♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)})) ·
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})))) |
| 409 | 112, 408 | eqtr4d 2780 |
. . 3
⊢ (𝜑 →
(-1↑((♯‘{𝑧
∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)})
+ (♯‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)}))) = ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 410 | | inrab 4316 |
. . . . . . 7
⊢ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∩ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) = {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∧ ¬ 2
∥ (1st ‘𝑧))} |
| 411 | | pm3.24 402 |
. . . . . . . . . 10
⊢ ¬ (2
∥ (1st ‘𝑧) ∧ ¬ 2 ∥ (1st
‘𝑧)) |
| 412 | 411 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ¬ (2 ∥
(1st ‘𝑧)
∧ ¬ 2 ∥ (1st ‘𝑧))) |
| 413 | 412 | ralrimivw 3150 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 ¬ (2 ∥ (1st
‘𝑧) ∧ ¬ 2
∥ (1st ‘𝑧))) |
| 414 | | rabeq0 4388 |
. . . . . . . 8
⊢ ({𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∧ ¬ 2
∥ (1st ‘𝑧))} = ∅ ↔ ∀𝑧 ∈ 𝑆 ¬ (2 ∥ (1st
‘𝑧) ∧ ¬ 2
∥ (1st ‘𝑧))) |
| 415 | 413, 414 | sylibr 234 |
. . . . . . 7
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∧ ¬ 2
∥ (1st ‘𝑧))} = ∅) |
| 416 | 410, 415 | eqtrid 2789 |
. . . . . 6
⊢ (𝜑 → ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∩ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) =
∅) |
| 417 | | hashun 14421 |
. . . . . 6
⊢ (({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∈ Fin ∧
{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈ Fin ∧
({𝑧 ∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)}
∩ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)})
= ∅) → (♯‘({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) =
((♯‘{𝑧 ∈
𝑆 ∣ 2 ∥
(1st ‘𝑧)})
+ (♯‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)}))) |
| 418 | 109, 104,
416, 417 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (♯‘({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) =
((♯‘{𝑧 ∈
𝑆 ∣ 2 ∥
(1st ‘𝑧)})
+ (♯‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)}))) |
| 419 | | unrab 4315 |
. . . . . . 7
⊢ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) = {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∨ ¬ 2
∥ (1st ‘𝑧))} |
| 420 | | exmid 895 |
. . . . . . . . 9
⊢ (2
∥ (1st ‘𝑧) ∨ ¬ 2 ∥ (1st
‘𝑧)) |
| 421 | 420 | rgenw 3065 |
. . . . . . . 8
⊢
∀𝑧 ∈
𝑆 (2 ∥
(1st ‘𝑧)
∨ ¬ 2 ∥ (1st ‘𝑧)) |
| 422 | | rabid2 3470 |
. . . . . . . 8
⊢ (𝑆 = {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∨ ¬ 2
∥ (1st ‘𝑧))} ↔ ∀𝑧 ∈ 𝑆 (2 ∥ (1st ‘𝑧) ∨ ¬ 2 ∥
(1st ‘𝑧))) |
| 423 | 421, 422 | mpbir 231 |
. . . . . . 7
⊢ 𝑆 = {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∨ ¬ 2
∥ (1st ‘𝑧))} |
| 424 | 419, 423 | eqtr4i 2768 |
. . . . . 6
⊢ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) = 𝑆 |
| 425 | 424 | fveq2i 6909 |
. . . . 5
⊢
(♯‘({𝑧
∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)}
∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)})) = (♯‘𝑆) |
| 426 | 418, 425 | eqtr3di 2792 |
. . . 4
⊢ (𝜑 → ((♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)}) +
(♯‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)})) = (♯‘𝑆)) |
| 427 | 426 | oveq2d 7447 |
. . 3
⊢ (𝜑 →
(-1↑((♯‘{𝑧
∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)})
+ (♯‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)}))) = (-1↑(♯‘𝑆))) |
| 428 | 93, 409, 427 | 3eqtr2d 2783 |
. 2
⊢ (𝜑 → (-1↑(Σ𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (-1↑(♯‘𝑆))) |
| 429 | 4, 78, 428 | 3eqtrd 2781 |
1
⊢ (𝜑 → (𝑄 /L 𝑃) = (-1↑(♯‘𝑆))) |