Step | Hyp | Ref
| Expression |
1 | | lgseisen.1 |
. . 3
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
2 | | lgseisen.2 |
. . 3
⊢ (𝜑 → 𝑄 ∈ (ℙ ∖
{2})) |
3 | | lgseisen.3 |
. . 3
⊢ (𝜑 → 𝑃 ≠ 𝑄) |
4 | 1, 2, 3 | lgseisen 26127 |
. 2
⊢ (𝜑 → (𝑄 /L 𝑃) = (-1↑Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
5 | | lgsquad.4 |
. . . . . 6
⊢ 𝑀 = ((𝑃 − 1) / 2) |
6 | 5 | oveq2i 7193 |
. . . . 5
⊢
(1...𝑀) =
(1...((𝑃 − 1) /
2)) |
7 | 6 | sumeq1i 15160 |
. . . 4
⊢
Σ𝑢 ∈
(1...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) |
8 | 1, 5 | gausslemma2dlem0b 26105 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℕ) |
9 | 8 | nnred 11743 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℝ) |
10 | 9 | rehalfcld 11975 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 / 2) ∈ ℝ) |
11 | 10 | flcld 13271 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈
ℤ) |
12 | 11 | zred 12180 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈
ℝ) |
13 | 12 | ltp1d 11660 |
. . . . . 6
⊢ (𝜑 → (⌊‘(𝑀 / 2)) <
((⌊‘(𝑀 / 2)) +
1)) |
14 | | fzdisj 13037 |
. . . . . 6
⊢
((⌊‘(𝑀 /
2)) < ((⌊‘(𝑀
/ 2)) + 1) → ((1...(⌊‘(𝑀 / 2))) ∩ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = ∅) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢ (𝜑 →
((1...(⌊‘(𝑀 /
2))) ∩ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = ∅) |
16 | 8 | nnrpd 12524 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈
ℝ+) |
17 | 16 | rphalfcld 12538 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 / 2) ∈
ℝ+) |
18 | 17 | rpge0d 12530 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (𝑀 / 2)) |
19 | | flge0nn0 13293 |
. . . . . . . . 9
⊢ (((𝑀 / 2) ∈ ℝ ∧ 0
≤ (𝑀 / 2)) →
(⌊‘(𝑀 / 2))
∈ ℕ0) |
20 | 10, 18, 19 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈
ℕ0) |
21 | 8 | nnnn0d 12048 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
22 | | rphalflt 12513 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℝ+
→ (𝑀 / 2) < 𝑀) |
23 | 16, 22 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 / 2) < 𝑀) |
24 | 8 | nnzd 12179 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) |
25 | | fllt 13279 |
. . . . . . . . . . 11
⊢ (((𝑀 / 2) ∈ ℝ ∧ 𝑀 ∈ ℤ) → ((𝑀 / 2) < 𝑀 ↔ (⌊‘(𝑀 / 2)) < 𝑀)) |
26 | 10, 24, 25 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 / 2) < 𝑀 ↔ (⌊‘(𝑀 / 2)) < 𝑀)) |
27 | 23, 26 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘(𝑀 / 2)) < 𝑀) |
28 | 12, 9, 27 | ltled 10878 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ≤ 𝑀) |
29 | | elfz2nn0 13101 |
. . . . . . . 8
⊢
((⌊‘(𝑀 /
2)) ∈ (0...𝑀) ↔
((⌊‘(𝑀 / 2))
∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧
(⌊‘(𝑀 / 2))
≤ 𝑀)) |
30 | 20, 21, 28, 29 | syl3anbrc 1344 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈ (0...𝑀)) |
31 | | nn0uz 12374 |
. . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) |
32 | 21, 31 | eleqtrdi 2844 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
33 | | elfzp12 13089 |
. . . . . . . 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 235 |
. . . . . 6
⊢ (𝜑 → ((⌊‘(𝑀 / 2)) = 0 ∨
(⌊‘(𝑀 / 2))
∈ ((0 + 1)...𝑀))) |
36 | | un0 4289 |
. . . . . . . . 9
⊢
((1...𝑀) ∪
∅) = (1...𝑀) |
37 | | uncom 4053 |
. . . . . . . . 9
⊢
((1...𝑀) ∪
∅) = (∅ ∪ (1...𝑀)) |
38 | 36, 37 | eqtr3i 2764 |
. . . . . . . 8
⊢
(1...𝑀) = (∅
∪ (1...𝑀)) |
39 | | oveq2 7190 |
. . . . . . . . . 10
⊢
((⌊‘(𝑀 /
2)) = 0 → (1...(⌊‘(𝑀 / 2))) = (1...0)) |
40 | | fz10 13031 |
. . . . . . . . . 10
⊢ (1...0) =
∅ |
41 | 39, 40 | eqtrdi 2790 |
. . . . . . . . 9
⊢
((⌊‘(𝑀 /
2)) = 0 → (1...(⌊‘(𝑀 / 2))) = ∅) |
42 | | oveq1 7189 |
. . . . . . . . . . 11
⊢
((⌊‘(𝑀 /
2)) = 0 → ((⌊‘(𝑀 / 2)) + 1) = (0 + 1)) |
43 | | 0p1e1 11850 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
44 | 42, 43 | eqtrdi 2790 |
. . . . . . . . . 10
⊢
((⌊‘(𝑀 /
2)) = 0 → ((⌊‘(𝑀 / 2)) + 1) = 1) |
45 | 44 | oveq1d 7197 |
. . . . . . . . 9
⊢
((⌊‘(𝑀 /
2)) = 0 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) = (1...𝑀)) |
46 | 41, 45 | uneq12d 4064 |
. . . . . . . 8
⊢
((⌊‘(𝑀 /
2)) = 0 → ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = (∅ ∪ (1...𝑀))) |
47 | 38, 46 | eqtr4id 2793 |
. . . . . . 7
⊢
((⌊‘(𝑀 /
2)) = 0 → (1...𝑀) =
((1...(⌊‘(𝑀 /
2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))) |
48 | | fzsplit 13036 |
. . . . . . . 8
⊢
((⌊‘(𝑀 /
2)) ∈ (1...𝑀) →
(1...𝑀) =
((1...(⌊‘(𝑀 /
2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))) |
49 | 43 | oveq1i 7192 |
. . . . . . . 8
⊢ ((0 +
1)...𝑀) = (1...𝑀) |
50 | 48, 49 | eleq2s 2852 |
. . . . . . 7
⊢
((⌊‘(𝑀 /
2)) ∈ ((0 + 1)...𝑀)
→ (1...𝑀) =
((1...(⌊‘(𝑀 /
2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))) |
51 | 47, 50 | jaoi 856 |
. . . . . 6
⊢
(((⌊‘(𝑀
/ 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀)) → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))) |
52 | 35, 51 | syl 17 |
. . . . 5
⊢ (𝜑 → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))) |
53 | | fzfid 13444 |
. . . . 5
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
54 | 2 | gausslemma2dlem0a 26104 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ ℕ) |
55 | 54 | nnred 11743 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄 ∈ ℝ) |
56 | 1 | gausslemma2dlem0a 26104 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℕ) |
57 | 55, 56 | nndivred 11782 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄 / 𝑃) ∈ ℝ) |
58 | 57 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (𝑄 / 𝑃) ∈ ℝ) |
59 | | 2nn 11801 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
60 | | elfznn 13039 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (1...𝑀) → 𝑢 ∈ ℕ) |
61 | 60 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → 𝑢 ∈ ℕ) |
62 | | nnmulcl 11752 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ 𝑢
∈ ℕ) → (2 · 𝑢) ∈ ℕ) |
63 | 59, 61, 62 | sylancr 590 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℕ) |
64 | 63 | nnred 11743 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℝ) |
65 | 58, 64 | remulcld 10761 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) |
66 | 54 | nnrpd 12524 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈
ℝ+) |
67 | 56 | nnrpd 12524 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈
ℝ+) |
68 | 66, 67 | rpdivcld 12543 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑄 / 𝑃) ∈
ℝ+) |
69 | 68 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (𝑄 / 𝑃) ∈
ℝ+) |
70 | 63 | nnrpd 12524 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈
ℝ+) |
71 | 69, 70 | rpmulcld 12542 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈
ℝ+) |
72 | 71 | rpge0d 12530 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → 0 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))) |
73 | | flge0nn0 13293 |
. . . . . . 7
⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 0 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
74 | 65, 72, 73 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
75 | 74 | nn0cnd 12050 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ) |
76 | 15, 52, 53, 75 | fsumsplit 15202 |
. . . 4
⊢ (𝜑 → Σ𝑢 ∈ (1...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
77 | 7, 76 | eqtr3id 2788 |
. . 3
⊢ (𝜑 → Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
78 | 77 | oveq2d 7198 |
. 2
⊢ (𝜑 → (-1↑Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
79 | | neg1cn 11842 |
. . . . 5
⊢ -1 ∈
ℂ |
80 | 79 | a1i 11 |
. . . 4
⊢ (𝜑 → -1 ∈
ℂ) |
81 | | fzfid 13444 |
. . . . 5
⊢ (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin) |
82 | | ssun2 4073 |
. . . . . . . 8
⊢
(((⌊‘(𝑀
/ 2)) + 1)...𝑀) ⊆
((1...(⌊‘(𝑀 /
2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) |
83 | 82, 52 | sseqtrrid 3940 |
. . . . . . 7
⊢ (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ⊆ (1...𝑀)) |
84 | 83 | sselda 3887 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ (1...𝑀)) |
85 | 84, 74 | syldan 594 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
86 | 81, 85 | fsumnn0cl 15198 |
. . . 4
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
87 | | fzfid 13444 |
. . . . 5
⊢ (𝜑 → (1...(⌊‘(𝑀 / 2))) ∈
Fin) |
88 | | ssun1 4072 |
. . . . . . . 8
⊢
(1...(⌊‘(𝑀 / 2))) ⊆ ((1...(⌊‘(𝑀 / 2))) ∪
(((⌊‘(𝑀 / 2)) +
1)...𝑀)) |
89 | 88, 52 | sseqtrrid 3940 |
. . . . . . 7
⊢ (𝜑 → (1...(⌊‘(𝑀 / 2))) ⊆ (1...𝑀)) |
90 | 89 | sselda 3887 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ (1...𝑀)) |
91 | 90, 74 | syldan 594 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
92 | 87, 91 | fsumnn0cl 15198 |
. . . 4
⊢ (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
93 | 80, 86, 92 | expaddd 13616 |
. . 3
⊢ (𝜑 → (-1↑(Σ𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
94 | | fzfid 13444 |
. . . . . . . . 9
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
95 | | xpfi 8875 |
. . . . . . . . 9
⊢
(((1...𝑀) ∈ Fin
∧ (1...𝑁) ∈ Fin)
→ ((1...𝑀) ×
(1...𝑁)) ∈
Fin) |
96 | 53, 94, 95 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → ((1...𝑀) × (1...𝑁)) ∈ Fin) |
97 | | lgsquad.6 |
. . . . . . . . 9
⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} |
98 | | opabssxp 5624 |
. . . . . . . . 9
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁)) |
99 | 97, 98 | eqsstri 3921 |
. . . . . . . 8
⊢ 𝑆 ⊆ ((1...𝑀) × (1...𝑁)) |
100 | | ssfi 8784 |
. . . . . . . 8
⊢
((((1...𝑀) ×
(1...𝑁)) ∈ Fin ∧
𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin) |
101 | 96, 99, 100 | sylancl 589 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ Fin) |
102 | | ssrab2 3979 |
. . . . . . 7
⊢ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ⊆ 𝑆 |
103 | | ssfi 8784 |
. . . . . . 7
⊢ ((𝑆 ∈ Fin ∧ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ⊆ 𝑆) → {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
104 | 101, 102,
103 | sylancl 589 |
. . . . . 6
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
105 | | hashcl 13821 |
. . . . . 6
⊢ ({𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈ Fin
→ (♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)}) ∈
ℕ0) |
106 | 104, 105 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) ∈
ℕ0) |
107 | | ssrab2 3979 |
. . . . . . 7
⊢ {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ⊆ 𝑆 |
108 | | ssfi 8784 |
. . . . . . 7
⊢ ((𝑆 ∈ Fin ∧ {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ⊆ 𝑆) → {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
109 | 101, 107,
108 | sylancl 589 |
. . . . . 6
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
110 | | hashcl 13821 |
. . . . . 6
⊢ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∈ Fin
→ (♯‘{𝑧
∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)})
∈ ℕ0) |
111 | 109, 110 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)}) ∈
ℕ0) |
112 | 80, 106, 111 | expaddd 13616 |
. . . 4
⊢ (𝜑 →
(-1↑((♯‘{𝑧
∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)})
+ (♯‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)}))) = ((-1↑(♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)})) ·
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})))) |
113 | 90, 63 | syldan 594 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 ·
𝑢) ∈
ℕ) |
114 | | fzfid 13444 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) ∈
Fin) |
115 | | xpsnen2g 8671 |
. . . . . . . . . . 11
⊢ (((2
· 𝑢) ∈ ℕ
∧ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ Fin) → ({(2 · 𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) ≈
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) |
116 | 113, 114,
115 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 ·
𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) ≈
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) |
117 | | hasheni 13812 |
. . . . . . . . . 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 3979 |
. . . . . . . . . . . . 13
⊢ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ⊆ 𝑆 |
120 | 97 | relopabiv 5674 |
. . . . . . . . . . . . 13
⊢ Rel 𝑆 |
121 | | relss 5637 |
. . . . . . . . . . . . 13
⊢ ({𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ⊆ 𝑆 → (Rel 𝑆 → Rel {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) |
122 | 119, 120,
121 | mp2 9 |
. . . . . . . . . . . 12
⊢ Rel
{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} |
123 | | relxp 5553 |
. . . . . . . . . . . 12
⊢ Rel ({(2
· 𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) |
124 | 97 | eleq2i 2825 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ 𝑆 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}) |
125 | | opabidw 5390 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) |
126 | 124, 125 | bitri 278 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ 𝑆 ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) |
127 | | anass 472 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))))) |
128 | 113 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) ∈
ℕ) |
129 | 128 | nnred 11743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) ∈
ℝ) |
130 | 56 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℕ) |
131 | 130 | nnred 11743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℝ) |
132 | 131 | rehalfcld 11975 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 / 2) ∈
ℝ) |
133 | 9 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑀 ∈
ℝ) |
134 | 133 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑀 ∈
ℝ) |
135 | | elfzle2 13014 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑢 ∈
(1...(⌊‘(𝑀 /
2))) → 𝑢 ≤
(⌊‘(𝑀 /
2))) |
136 | 135 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ≤ (⌊‘(𝑀 / 2))) |
137 | 133 | rehalfcld 11975 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑀 / 2) ∈
ℝ) |
138 | | elfzelz 13010 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑢 ∈
(1...(⌊‘(𝑀 /
2))) → 𝑢 ∈
ℤ) |
139 | 138 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈
ℤ) |
140 | | flge 13278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑀 / 2) ∈ ℝ ∧ 𝑢 ∈ ℤ) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2)))) |
141 | 137, 139,
140 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2)))) |
142 | 136, 141 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ≤ (𝑀 / 2)) |
143 | | elfznn 13039 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑢 ∈
(1...(⌊‘(𝑀 /
2))) → 𝑢 ∈
ℕ) |
144 | 143 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈
ℕ) |
145 | 144 | nnred 11743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈
ℝ) |
146 | | 2re 11802 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 2 ∈
ℝ |
147 | 146 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 2 ∈
ℝ) |
148 | | 2pos 11831 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 0 <
2 |
149 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 0 <
2) |
150 | | lemuldiv2 11611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑢 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → ((2 · 𝑢) ≤ 𝑀 ↔ 𝑢 ≤ (𝑀 / 2))) |
151 | 145, 133,
147, 149, 150 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 ·
𝑢) ≤ 𝑀 ↔ 𝑢 ≤ (𝑀 / 2))) |
152 | 142, 151 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 ·
𝑢) ≤ 𝑀) |
153 | 152 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) ≤ 𝑀) |
154 | 131 | ltm1d 11662 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 − 1) < 𝑃) |
155 | | peano2rem 11043 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 11594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑃 − 1) ∈ ℝ ∧
𝑃 ∈ ℝ ∧ (2
∈ ℝ ∧ 0 < 2)) → ((𝑃 − 1) < 𝑃 ↔ ((𝑃 − 1) / 2) < (𝑃 / 2))) |
160 | 156, 131,
157, 158, 159 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 − 1) < 𝑃 ↔ ((𝑃 − 1) / 2) < (𝑃 / 2))) |
161 | 154, 160 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 − 1) / 2) < (𝑃 / 2)) |
162 | 5, 161 | eqbrtrid 5075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑀 < (𝑃 / 2)) |
163 | 129, 134,
132, 153, 162 | lelttrd 10888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) < (𝑃 / 2)) |
164 | 130 | nnrpd 12524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℝ+) |
165 | | rphalflt 12513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℝ+
→ (𝑃 / 2) < 𝑃) |
166 | 164, 165 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 / 2) < 𝑃) |
167 | 129, 132,
131, 163, 166 | lttrd 10891 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) < 𝑃) |
168 | 129, 131 | ltnled 10877 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((2
· 𝑢) < 𝑃 ↔ ¬ 𝑃 ≤ (2 · 𝑢))) |
169 | 167, 168 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬
𝑃 ≤ (2 · 𝑢)) |
170 | 1 | eldifad 3865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑃 ∈ ℙ) |
171 | 170 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℙ) |
172 | | prmz 16128 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
173 | 171, 172 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℤ) |
174 | | dvdsle 15767 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃 ∈ ℤ ∧ (2
· 𝑢) ∈ ℕ)
→ (𝑃 ∥ (2
· 𝑢) → 𝑃 ≤ (2 · 𝑢))) |
175 | 173, 128,
174 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ (2 · 𝑢) → 𝑃 ≤ (2 · 𝑢))) |
176 | 169, 175 | mtod 201 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬
𝑃 ∥ (2 · 𝑢)) |
177 | 2 | eldifad 3865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑄 ∈ ℙ) |
178 | | prmrp 16165 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄)) |
179 | 170, 177,
178 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄)) |
180 | 3, 179 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑃 gcd 𝑄) = 1) |
181 | 180 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 gcd 𝑄) = 1) |
182 | 177 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈
ℙ) |
183 | | prmz 16128 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℤ) |
184 | 182, 183 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈
ℤ) |
185 | 128 | nnzd 12179 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) ∈
ℤ) |
186 | | coprmdvds 16106 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ (2
· 𝑢) ∈ ℤ)
→ ((𝑃 ∥ (𝑄 · (2 · 𝑢)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑢))) |
187 | 173, 184,
185, 186 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 ∥ (𝑄 · (2 · 𝑢)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑢))) |
188 | 181, 187 | mpan2d 694 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ (𝑄 · (2 · 𝑢)) → 𝑃 ∥ (2 · 𝑢))) |
189 | 176, 188 | mtod 201 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬
𝑃 ∥ (𝑄 · (2 · 𝑢))) |
190 | | nnz 12097 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
191 | 190 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈
ℤ) |
192 | | dvdsmul2 15736 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑃 ∥ (𝑦 · 𝑃)) |
193 | 191, 173,
192 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∥ (𝑦 · 𝑃)) |
194 | | breq2 5044 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑄 · (2 · 𝑢)) = (𝑦 · 𝑃) → (𝑃 ∥ (𝑄 · (2 · 𝑢)) ↔ 𝑃 ∥ (𝑦 · 𝑃))) |
195 | 193, 194 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 · (2 · 𝑢)) = (𝑦 · 𝑃) → 𝑃 ∥ (𝑄 · (2 · 𝑢)))) |
196 | 195 | necon3bd 2949 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (¬
𝑃 ∥ (𝑄 · (2 · 𝑢)) → (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃))) |
197 | 189, 196 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃)) |
198 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈
ℕ) |
199 | 198, 130 | nnmulcld 11781 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℕ) |
200 | 199 | nnred 11743 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℝ) |
201 | 54 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑄 ∈
ℕ) |
202 | 201, 113 | nnmulcld 11781 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑄 · (2 · 𝑢)) ∈
ℕ) |
203 | 202 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈
ℕ) |
204 | 203 | nnred 11743 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈
ℝ) |
205 | 200, 204 | ltlend 10875 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃)))) |
206 | 197, 205 | mpbiran2d 708 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ (𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)))) |
207 | | nnre 11735 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
208 | 207 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈
ℝ) |
209 | 130 | nngt0d 11777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 <
𝑃) |
210 | | lemuldiv 11610 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 <
𝑃)) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))) |
211 | 208, 204,
131, 209, 210 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))) |
212 | 201 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈
ℕ) |
213 | 212 | nncnd 11744 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈
ℂ) |
214 | 128 | nncnd 11744 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) ∈
ℂ) |
215 | 130 | nncnd 11744 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℂ) |
216 | 130 | nnne0d 11778 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ≠ 0) |
217 | 213, 214,
215, 216 | div23d 11543 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 · (2 · 𝑢)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑢))) |
218 | 217 | breq2d 5052 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃) ↔ 𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))) |
219 | 206, 211,
218 | 3bitrd 308 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))) |
220 | 212 | nnred 11743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈
ℝ) |
221 | 212 | nngt0d 11777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 <
𝑄) |
222 | | ltmul2 11581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((2
· 𝑢) ∈ ℝ
∧ (𝑃 / 2) ∈
ℝ ∧ (𝑄 ∈
ℝ ∧ 0 < 𝑄))
→ ((2 · 𝑢) <
(𝑃 / 2) ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2)))) |
223 | 129, 132,
220, 221, 222 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((2
· 𝑢) < (𝑃 / 2) ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2)))) |
224 | 163, 223 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2))) |
225 | | 2cnd 11806 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ∈
ℂ) |
226 | | 2ne0 11832 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 2 ≠
0 |
227 | 226 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ≠
0) |
228 | | divass 11406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → ((𝑄 · 𝑃) / 2) = (𝑄 · (𝑃 / 2))) |
229 | | div23 11407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → ((𝑄 · 𝑃) / 2) = ((𝑄 / 2) · 𝑃)) |
230 | 228, 229 | eqtr3d 2776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → (𝑄 · (𝑃 / 2)) = ((𝑄 / 2) · 𝑃)) |
231 | 213, 215,
225, 227, 230 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (𝑃 / 2)) = ((𝑄 / 2) · 𝑃)) |
232 | 224, 231 | breqtrd 5066 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) |
233 | 220 | rehalfcld 11975 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 / 2) ∈
ℝ) |
234 | 233, 131 | remulcld 10761 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 2) · 𝑃) ∈ ℝ) |
235 | | lttr 10807 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑦 · 𝑃) ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ ((𝑄 / 2) · 𝑃) ∈ ℝ) → (((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃))) |
236 | 200, 204,
234, 235 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃))) |
237 | 232, 236 | mpan2d 694 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃))) |
238 | | ltmul1 11580 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ (𝑄 / 2) ∈ ℝ ∧
(𝑃 ∈ ℝ ∧ 0
< 𝑃)) → (𝑦 < (𝑄 / 2) ↔ (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃))) |
239 | 208, 233,
131, 209, 238 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 / 2) ↔ (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃))) |
240 | 237, 239 | sylibrd 262 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 < (𝑄 / 2))) |
241 | | peano2rem 11043 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑄 ∈ ℝ → (𝑄 − 1) ∈
ℝ) |
242 | 220, 241 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − 1) ∈
ℝ) |
243 | 242 | recnd 10759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − 1) ∈
ℂ) |
244 | 213, 243,
225, 227 | divsubdird 11545 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = ((𝑄 / 2) − ((𝑄 − 1) / 2))) |
245 | | lgsquad.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝑁 = ((𝑄 − 1) / 2) |
246 | 245 | oveq2i 7193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑄 / 2) − 𝑁) = ((𝑄 / 2) − ((𝑄 − 1) / 2)) |
247 | 244, 246 | eqtr4di 2792 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = ((𝑄 / 2) − 𝑁)) |
248 | | ax-1cn 10685 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 1 ∈
ℂ |
249 | | nncan 11005 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑄 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑄 −
(𝑄 − 1)) =
1) |
250 | 213, 248,
249 | sylancl 589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − (𝑄 − 1)) = 1) |
251 | 250 | oveq1d 7197 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = (1 /
2)) |
252 | | halflt1 11946 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (1 / 2)
< 1 |
253 | 251, 252 | eqbrtrdi 5079 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) < 1) |
254 | 247, 253 | eqbrtrrd 5064 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 2) − 𝑁) < 1) |
255 | 2, 245 | gausslemma2dlem0b 26105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑁 ∈ ℕ) |
256 | 255 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈
ℕ) |
257 | 256 | nnred 11743 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈
ℝ) |
258 | | 1red 10732 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 1 ∈
ℝ) |
259 | 233, 257,
258 | ltsubadd2d 11328 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (((𝑄 / 2) − 𝑁) < 1 ↔ (𝑄 / 2) < (𝑁 + 1))) |
260 | 254, 259 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 / 2) < (𝑁 + 1)) |
261 | | peano2re 10903 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈
ℝ) |
262 | 257, 261 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑁 + 1) ∈
ℝ) |
263 | | lttr 10807 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ (𝑄 / 2) ∈ ℝ ∧
(𝑁 + 1) ∈ ℝ)
→ ((𝑦 < (𝑄 / 2) ∧ (𝑄 / 2) < (𝑁 + 1)) → 𝑦 < (𝑁 + 1))) |
264 | 208, 233,
262, 263 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . 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 12130 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑦 ≤ 𝑁 ↔ 𝑦 < (𝑁 + 1))) |
268 | 198, 256,
267 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ 𝑁 ↔ 𝑦 < (𝑁 + 1))) |
269 | 266, 268 | sylibrd 262 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 ≤ 𝑁)) |
270 | 269 | pm4.71rd 566 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))))) |
271 | 90, 65 | syldan 594 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) |
272 | | flge 13278 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑦 ∈ ℤ) → (𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
273 | 271, 190,
272 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
274 | 219, 270,
273 | 3bitr3d 312 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
275 | 274 | pm5.32da 582 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
276 | 127, 275 | syl5bb 286 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
277 | 276 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
278 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑥 = (2 · 𝑢)) |
279 | | nnuz 12375 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ℕ =
(ℤ≥‘1) |
280 | 113, 279 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 ·
𝑢) ∈
(ℤ≥‘1)) |
281 | 24 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑀 ∈
ℤ) |
282 | | elfz5 13002 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((2
· 𝑢) ∈
(ℤ≥‘1) ∧ 𝑀 ∈ ℤ) → ((2 · 𝑢) ∈ (1...𝑀) ↔ (2 · 𝑢) ≤ 𝑀)) |
283 | 280, 281,
282 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 ·
𝑢) ∈ (1...𝑀) ↔ (2 · 𝑢) ≤ 𝑀)) |
284 | 152, 283 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 ·
𝑢) ∈ (1...𝑀)) |
285 | 284 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (2 · 𝑢) ∈ (1...𝑀)) |
286 | 278, 285 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑥 ∈ (1...𝑀)) |
287 | 286 | biantrurd 536 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...𝑁) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)))) |
288 | 255 | nnzd 12179 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℤ) |
289 | 288 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑁 ∈ ℤ) |
290 | | fznn 13078 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℤ → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁))) |
291 | 289, 290 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁))) |
292 | 287, 291 | bitr3d 284 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁))) |
293 | | oveq1 7189 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (2 · 𝑢) → (𝑥 · 𝑄) = ((2 · 𝑢) · 𝑄)) |
294 | 113 | nncnd 11744 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 ·
𝑢) ∈
ℂ) |
295 | 201 | nncnd 11744 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑄 ∈
ℂ) |
296 | 294, 295 | mulcomd 10752 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 ·
𝑢) · 𝑄) = (𝑄 · (2 · 𝑢))) |
297 | 293, 296 | sylan9eqr 2796 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑥 · 𝑄) = (𝑄 · (2 · 𝑢))) |
298 | 297 | breq2d 5052 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → ((𝑦 · 𝑃) < (𝑥 · 𝑄) ↔ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))) |
299 | 292, 298 | anbi12d 634 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ ((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))))) |
300 | 271 | flcld 13271 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℤ) |
301 | | fznn 13078 |
. . . . . . . . . . . . . . . . . 18
⊢
((⌊‘((𝑄
/ 𝑃) · (2 ·
𝑢))) ∈ ℤ →
(𝑦 ∈
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
302 | 300, 301 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑦 ∈
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
303 | 302 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
304 | 277, 299,
303 | 3bitr4d 314 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
305 | 126, 304 | syl5bb 286 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (〈𝑥, 𝑦〉 ∈ 𝑆 ↔ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
306 | 305 | pm5.32da 582 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑥 = (2 · 𝑢) ∧ 〈𝑥, 𝑦〉 ∈ 𝑆) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
307 | | vex 3404 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑥 ∈ V |
308 | | vex 3404 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑦 ∈ V |
309 | 307, 308 | op1std 7736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) |
310 | 309 | eqeq2d 2750 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((2 · 𝑢) = (1st ‘𝑧) ↔ (2 · 𝑢) = 𝑥)) |
311 | | eqcom 2746 |
. . . . . . . . . . . . . . . 16
⊢ ((2
· 𝑢) = 𝑥 ↔ 𝑥 = (2 · 𝑢)) |
312 | 310, 311 | bitrdi 290 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((2 · 𝑢) = (1st ‘𝑧) ↔ 𝑥 = (2 · 𝑢))) |
313 | 312 | elrab 3593 |
. . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑦〉 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ↔ (〈𝑥, 𝑦〉 ∈ 𝑆 ∧ 𝑥 = (2 · 𝑢))) |
314 | 313 | biancomi 466 |
. . . . . . . . . . . . 13
⊢
(〈𝑥, 𝑦〉 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ↔ (𝑥 = (2 · 𝑢) ∧ 〈𝑥, 𝑦〉 ∈ 𝑆)) |
315 | | opelxp 5571 |
. . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑦〉 ∈ ({(2 ·
𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) ↔ (𝑥 ∈ {(2 · 𝑢)} ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
316 | | velsn 4542 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ {(2 · 𝑢)} ↔ 𝑥 = (2 · 𝑢)) |
317 | 316 | anbi1i 627 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ {(2 · 𝑢)} ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
318 | 315, 317 | bitri 278 |
. . . . . . . . . . . . 13
⊢
(〈𝑥, 𝑦〉 ∈ ({(2 ·
𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
319 | 306, 314,
318 | 3bitr4g 317 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (〈𝑥, 𝑦〉 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ↔ 〈𝑥, 𝑦〉 ∈ ({(2 · 𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))))) |
320 | 122, 123,
319 | eqrelrdv 5646 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} = ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
321 | 320 | eqcomd 2745 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 ·
𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) = {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}) |
322 | 321 | fveq2d 6690 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (♯‘{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) |
323 | | hashfz1 13810 |
. . . . . . . . . 10
⊢
((⌊‘((𝑄
/ 𝑃) · (2 ·
𝑢))) ∈
ℕ0 → (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) |
324 | 91, 323 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) |
325 | 118, 322,
324 | 3eqtr3rd 2783 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (♯‘{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) |
326 | 325 | sumeq2dv 15165 |
. . . . . . 7
⊢ (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(♯‘{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) |
327 | 101 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑆 ∈ Fin) |
328 | | ssfi 8784 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Fin ∧ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ⊆ 𝑆) → {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ∈ Fin) |
329 | 327, 119,
328 | sylancl 589 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ∈ Fin) |
330 | | fveq2 6686 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑣 → (1st ‘𝑧) = (1st ‘𝑣)) |
331 | 330 | eqeq2d 2750 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑣 → ((2 · 𝑢) = (1st ‘𝑧) ↔ (2 · 𝑢) = (1st ‘𝑣))) |
332 | 331 | elrab 3593 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ↔ (𝑣 ∈ 𝑆 ∧ (2 · 𝑢) = (1st ‘𝑣))) |
333 | 332 | simprbi 500 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} → (2 · 𝑢) = (1st ‘𝑣)) |
334 | 333 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → (2 · 𝑢) = (1st ‘𝑣)) |
335 | 334 | oveq1d 7197 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → ((2 · 𝑢) / 2) = ((1st ‘𝑣) / 2)) |
336 | 144 | nncnd 11744 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈
ℂ) |
337 | 336 | adantrr 717 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → 𝑢 ∈ ℂ) |
338 | | 2cnd 11806 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → 2 ∈
ℂ) |
339 | 226 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → 2 ≠ 0) |
340 | 337, 338,
339 | divcan3d 11511 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → ((2 · 𝑢) / 2) = 𝑢) |
341 | 335, 340 | eqtr3d 2776 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → ((1st ‘𝑣) / 2) = 𝑢) |
342 | 341 | ralrimivva 3104 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑢 ∈ (1...(⌊‘(𝑀 / 2)))∀𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ((1st ‘𝑣) / 2) = 𝑢) |
343 | | invdisj 5024 |
. . . . . . . . 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 15282 |
. . . . . . 7
⊢ (𝜑 → (♯‘∪ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}) = Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(♯‘{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) |
346 | | iunrab 4948 |
. . . . . . . . 9
⊢ ∪ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} = {𝑧 ∈ 𝑆 ∣ ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧)} |
347 | | 2cn 11803 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
348 | | zcn 12079 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ℤ → 𝑢 ∈
ℂ) |
349 | 348 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ ℤ) → 𝑢 ∈ ℂ) |
350 | | mulcom 10713 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℂ ∧ 𝑢
∈ ℂ) → (2 · 𝑢) = (𝑢 · 2)) |
351 | 347, 349,
350 | sylancr 590 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ ℤ) → (2 · 𝑢) = (𝑢 · 2)) |
352 | 351 | eqeq1d 2741 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ ℤ) → ((2 · 𝑢) = (1st ‘𝑧) ↔ (𝑢 · 2) = (1st ‘𝑧))) |
353 | 352 | rexbidva 3207 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ ℤ (2 · 𝑢) = (1st ‘𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st
‘𝑧))) |
354 | 138 | anim1i 618 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈
(1...(⌊‘(𝑀 /
2))) ∧ (2 · 𝑢) =
(1st ‘𝑧))
→ (𝑢 ∈ ℤ
∧ (2 · 𝑢) =
(1st ‘𝑧))) |
355 | 354 | reximi2 3159 |
. . . . . . . . . . . 12
⊢
(∃𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(2 · 𝑢) =
(1st ‘𝑧)
→ ∃𝑢 ∈
ℤ (2 · 𝑢) =
(1st ‘𝑧)) |
356 | | simprr 773 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (2 · 𝑢) = (1st ‘𝑧)) |
357 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆) |
358 | 99, 357 | sseldi 3885 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ ((1...𝑀) × (1...𝑁))) |
359 | | xp1st 7758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ ((1...𝑀) × (1...𝑁)) → (1st ‘𝑧) ∈ (1...𝑀)) |
360 | 358, 359 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (1st ‘𝑧) ∈ (1...𝑀)) |
361 | 360 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (1st
‘𝑧) ∈ (1...𝑀)) |
362 | | elfzle2 13014 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑧) ∈ (1...𝑀) → (1st ‘𝑧) ≤ 𝑀) |
363 | 361, 362 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (1st
‘𝑧) ≤ 𝑀) |
364 | 356, 363 | eqbrtrd 5062 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (2 · 𝑢) ≤ 𝑀) |
365 | | zre 12078 |
. . . . . . . . . . . . . . . . . . . 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 1375 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → ((2 · 𝑢) ≤ 𝑀 ↔ 𝑢 ≤ (𝑀 / 2))) |
371 | 364, 370 | mpbid 235 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ≤ (𝑀 / 2)) |
372 | 10 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (𝑀 / 2) ∈ ℝ) |
373 | | simprl 771 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈ ℤ) |
374 | 372, 373,
140 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2)))) |
375 | 371, 374 | mpbid 235 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ≤ (⌊‘(𝑀 / 2))) |
376 | | 2t0e0 11897 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
· 0) = 0 |
377 | | elfznn 13039 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((1st ‘𝑧) ∈ (1...𝑀) → (1st ‘𝑧) ∈
ℕ) |
378 | 361, 377 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (1st
‘𝑧) ∈
ℕ) |
379 | 356, 378 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (2 · 𝑢) ∈
ℕ) |
380 | 379 | nngt0d 11777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 0 < (2 ·
𝑢)) |
381 | 376, 380 | eqbrtrid 5075 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (2 · 0) <
(2 · 𝑢)) |
382 | | 0red 10734 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 0 ∈
ℝ) |
383 | | ltmul2 11581 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0
∈ ℝ ∧ 𝑢
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (0 < 𝑢 ↔ (2 · 0) < (2
· 𝑢))) |
384 | 382, 366,
368, 369, 383 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (0 < 𝑢 ↔ (2 · 0) < (2
· 𝑢))) |
385 | 381, 384 | mpbird 260 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 0 < 𝑢) |
386 | | elnnz 12084 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ ℕ ↔ (𝑢 ∈ ℤ ∧ 0 <
𝑢)) |
387 | 373, 385,
386 | sylanbrc 586 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈ ℕ) |
388 | 387, 279 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈
(ℤ≥‘1)) |
389 | 11 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (⌊‘(𝑀 / 2)) ∈
ℤ) |
390 | | elfz5 13002 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈
(ℤ≥‘1) ∧ (⌊‘(𝑀 / 2)) ∈ ℤ) → (𝑢 ∈
(1...(⌊‘(𝑀 /
2))) ↔ 𝑢 ≤
(⌊‘(𝑀 /
2)))) |
391 | 388, 389,
390 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2)))) |
392 | 375, 391 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) |
393 | 392, 356 | jca 515 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st ‘𝑧))) |
394 | 393 | ex 416 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧)) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st ‘𝑧)))) |
395 | 394 | reximdv2 3182 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ ℤ (2 · 𝑢) = (1st ‘𝑧) → ∃𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(2 · 𝑢) =
(1st ‘𝑧))) |
396 | 355, 395 | impbid2 229 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧) ↔ ∃𝑢 ∈ ℤ (2 ·
𝑢) = (1st
‘𝑧))) |
397 | | 2z 12107 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℤ |
398 | 360 | elfzelzd 13011 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (1st ‘𝑧) ∈
ℤ) |
399 | | divides 15713 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℤ ∧ (1st ‘𝑧) ∈ ℤ) → (2 ∥
(1st ‘𝑧)
↔ ∃𝑢 ∈
ℤ (𝑢 · 2) =
(1st ‘𝑧))) |
400 | 397, 398,
399 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (2 ∥ (1st
‘𝑧) ↔
∃𝑢 ∈ ℤ
(𝑢 · 2) =
(1st ‘𝑧))) |
401 | 353, 396,
400 | 3bitr4d 314 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧) ↔ 2 ∥
(1st ‘𝑧))) |
402 | 401 | rabbidva 3380 |
. . . . . . . . 9
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧)} = {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)}) |
403 | 346, 402 | syl5eq 2786 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} = {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)}) |
404 | 403 | fveq2d 6690 |
. . . . . . 7
⊢ (𝜑 → (♯‘∪ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}) = (♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)})) |
405 | 326, 345,
404 | 3eqtr2d 2780 |
. . . . . 6
⊢ (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)})) |
406 | 405 | oveq2d 7198 |
. . . . 5
⊢ (𝜑 → (-1↑Σ𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) =
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)}))) |
407 | 1, 2, 3, 5, 245, 97 | lgsquadlem1 26128 |
. . . . 5
⊢ (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) |
408 | 406, 407 | oveq12d 7200 |
. . . 4
⊢ (𝜑 → ((-1↑Σ𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) ·
(-1↑Σ𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = ((-1↑(♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)})) ·
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})))) |
409 | 112, 408 | eqtr4d 2777 |
. . 3
⊢ (𝜑 →
(-1↑((♯‘{𝑧
∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)})
+ (♯‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)}))) = ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
410 | | inrab 4205 |
. . . . . . 7
⊢ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∩ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) = {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∧ ¬ 2
∥ (1st ‘𝑧))} |
411 | | pm3.24 406 |
. . . . . . . . . 10
⊢ ¬ (2
∥ (1st ‘𝑧) ∧ ¬ 2 ∥ (1st
‘𝑧)) |
412 | 411 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ¬ (2 ∥
(1st ‘𝑧)
∧ ¬ 2 ∥ (1st ‘𝑧))) |
413 | 412 | ralrimivw 3098 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 ¬ (2 ∥ (1st
‘𝑧) ∧ ¬ 2
∥ (1st ‘𝑧))) |
414 | | rabeq0 4283 |
. . . . . . . 8
⊢ ({𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∧ ¬ 2
∥ (1st ‘𝑧))} = ∅ ↔ ∀𝑧 ∈ 𝑆 ¬ (2 ∥ (1st
‘𝑧) ∧ ¬ 2
∥ (1st ‘𝑧))) |
415 | 413, 414 | sylibr 237 |
. . . . . . 7
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∧ ¬ 2
∥ (1st ‘𝑧))} = ∅) |
416 | 410, 415 | syl5eq 2786 |
. . . . . 6
⊢ (𝜑 → ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∩ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) =
∅) |
417 | | hashun 13847 |
. . . . . 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 1372 |
. . . . 5
⊢ (𝜑 → (♯‘({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) =
((♯‘{𝑧 ∈
𝑆 ∣ 2 ∥
(1st ‘𝑧)})
+ (♯‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)}))) |
419 | | unrab 4204 |
. . . . . . 7
⊢ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) = {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∨ ¬ 2
∥ (1st ‘𝑧))} |
420 | | exmid 894 |
. . . . . . . . 9
⊢ (2
∥ (1st ‘𝑧) ∨ ¬ 2 ∥ (1st
‘𝑧)) |
421 | 420 | rgenw 3066 |
. . . . . . . 8
⊢
∀𝑧 ∈
𝑆 (2 ∥
(1st ‘𝑧)
∨ ¬ 2 ∥ (1st ‘𝑧)) |
422 | | rabid2 3285 |
. . . . . . . 8
⊢ (𝑆 = {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∨ ¬ 2
∥ (1st ‘𝑧))} ↔ ∀𝑧 ∈ 𝑆 (2 ∥ (1st ‘𝑧) ∨ ¬ 2 ∥
(1st ‘𝑧))) |
423 | 421, 422 | mpbir 234 |
. . . . . . 7
⊢ 𝑆 = {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∨ ¬ 2
∥ (1st ‘𝑧))} |
424 | 419, 423 | eqtr4i 2765 |
. . . . . 6
⊢ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) = 𝑆 |
425 | 424 | fveq2i 6689 |
. . . . 5
⊢
(♯‘({𝑧
∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)}
∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)})) = (♯‘𝑆) |
426 | 418, 425 | eqtr3di 2789 |
. . . 4
⊢ (𝜑 → ((♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)}) +
(♯‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)})) = (♯‘𝑆)) |
427 | 426 | oveq2d 7198 |
. . 3
⊢ (𝜑 →
(-1↑((♯‘{𝑧
∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)})
+ (♯‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)}))) = (-1↑(♯‘𝑆))) |
428 | 93, 409, 427 | 3eqtr2d 2780 |
. 2
⊢ (𝜑 → (-1↑(Σ𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (-1↑(♯‘𝑆))) |
429 | 4, 78, 428 | 3eqtrd 2778 |
1
⊢ (𝜑 → (𝑄 /L 𝑃) = (-1↑(♯‘𝑆))) |