Step | Hyp | Ref
| Expression |
1 | | lgseisen.1 |
. . 3
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
2 | | lgseisen.2 |
. . 3
⊢ (𝜑 → 𝑄 ∈ (ℙ ∖
{2})) |
3 | | lgseisen.3 |
. . 3
⊢ (𝜑 → 𝑃 ≠ 𝑄) |
4 | 1, 2, 3 | lgseisen 25299 |
. 2
⊢ (𝜑 → (𝑄 /L 𝑃) = (-1↑Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
5 | | lgsquad.4 |
. . . . . 6
⊢ 𝑀 = ((𝑃 − 1) / 2) |
6 | 5 | oveq2i 6820 |
. . . . 5
⊢
(1...𝑀) =
(1...((𝑃 − 1) /
2)) |
7 | 6 | sumeq1i 14623 |
. . . 4
⊢
Σ𝑢 ∈
(1...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) |
8 | | oddprm 15713 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
9 | 1, 8 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ) |
10 | 5, 9 | syl5eqel 2839 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℕ) |
11 | 10 | nnred 11223 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℝ) |
12 | 11 | rehalfcld 11467 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 / 2) ∈ ℝ) |
13 | 12 | flcld 12789 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈
ℤ) |
14 | 13 | zred 11670 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈
ℝ) |
15 | 14 | ltp1d 11142 |
. . . . . 6
⊢ (𝜑 → (⌊‘(𝑀 / 2)) <
((⌊‘(𝑀 / 2)) +
1)) |
16 | | fzdisj 12557 |
. . . . . 6
⊢
((⌊‘(𝑀 /
2)) < ((⌊‘(𝑀
/ 2)) + 1) → ((1...(⌊‘(𝑀 / 2))) ∩ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = ∅) |
17 | 15, 16 | syl 17 |
. . . . 5
⊢ (𝜑 →
((1...(⌊‘(𝑀 /
2))) ∩ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = ∅) |
18 | 10 | nnrpd 12059 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈
ℝ+) |
19 | 18 | rphalfcld 12073 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 / 2) ∈
ℝ+) |
20 | 19 | rpge0d 12065 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (𝑀 / 2)) |
21 | | flge0nn0 12811 |
. . . . . . . . 9
⊢ (((𝑀 / 2) ∈ ℝ ∧ 0
≤ (𝑀 / 2)) →
(⌊‘(𝑀 / 2))
∈ ℕ0) |
22 | 12, 20, 21 | syl2anc 696 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈
ℕ0) |
23 | 10 | nnnn0d 11539 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
24 | | rphalflt 12049 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℝ+
→ (𝑀 / 2) < 𝑀) |
25 | 18, 24 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 / 2) < 𝑀) |
26 | 10 | nnzd 11669 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) |
27 | | fllt 12797 |
. . . . . . . . . . 11
⊢ (((𝑀 / 2) ∈ ℝ ∧ 𝑀 ∈ ℤ) → ((𝑀 / 2) < 𝑀 ↔ (⌊‘(𝑀 / 2)) < 𝑀)) |
28 | 12, 26, 27 | syl2anc 696 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 / 2) < 𝑀 ↔ (⌊‘(𝑀 / 2)) < 𝑀)) |
29 | 25, 28 | mpbid 222 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘(𝑀 / 2)) < 𝑀) |
30 | 14, 11, 29 | ltled 10373 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ≤ 𝑀) |
31 | | elfz2nn0 12620 |
. . . . . . . 8
⊢
((⌊‘(𝑀 /
2)) ∈ (0...𝑀) ↔
((⌊‘(𝑀 / 2))
∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧
(⌊‘(𝑀 / 2))
≤ 𝑀)) |
32 | 22, 23, 30, 31 | syl3anbrc 1429 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈ (0...𝑀)) |
33 | | nn0uz 11911 |
. . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) |
34 | 23, 33 | syl6eleq 2845 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
35 | | elfzp12 12608 |
. . . . . . . 8
⊢ (𝑀 ∈
(ℤ≥‘0) → ((⌊‘(𝑀 / 2)) ∈ (0...𝑀) ↔ ((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀)))) |
36 | 34, 35 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((⌊‘(𝑀 / 2)) ∈ (0...𝑀) ↔ ((⌊‘(𝑀 / 2)) = 0 ∨
(⌊‘(𝑀 / 2))
∈ ((0 + 1)...𝑀)))) |
37 | 32, 36 | mpbid 222 |
. . . . . 6
⊢ (𝜑 → ((⌊‘(𝑀 / 2)) = 0 ∨
(⌊‘(𝑀 / 2))
∈ ((0 + 1)...𝑀))) |
38 | | oveq2 6817 |
. . . . . . . . . 10
⊢
((⌊‘(𝑀 /
2)) = 0 → (1...(⌊‘(𝑀 / 2))) = (1...0)) |
39 | | fz10 12551 |
. . . . . . . . . 10
⊢ (1...0) =
∅ |
40 | 38, 39 | syl6eq 2806 |
. . . . . . . . 9
⊢
((⌊‘(𝑀 /
2)) = 0 → (1...(⌊‘(𝑀 / 2))) = ∅) |
41 | | oveq1 6816 |
. . . . . . . . . . 11
⊢
((⌊‘(𝑀 /
2)) = 0 → ((⌊‘(𝑀 / 2)) + 1) = (0 + 1)) |
42 | | 0p1e1 11320 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
43 | 41, 42 | syl6eq 2806 |
. . . . . . . . . 10
⊢
((⌊‘(𝑀 /
2)) = 0 → ((⌊‘(𝑀 / 2)) + 1) = 1) |
44 | 43 | oveq1d 6824 |
. . . . . . . . 9
⊢
((⌊‘(𝑀 /
2)) = 0 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) = (1...𝑀)) |
45 | 40, 44 | uneq12d 3907 |
. . . . . . . 8
⊢
((⌊‘(𝑀 /
2)) = 0 → ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = (∅ ∪ (1...𝑀))) |
46 | | un0 4106 |
. . . . . . . . 9
⊢
((1...𝑀) ∪
∅) = (1...𝑀) |
47 | | uncom 3896 |
. . . . . . . . 9
⊢
((1...𝑀) ∪
∅) = (∅ ∪ (1...𝑀)) |
48 | 46, 47 | eqtr3i 2780 |
. . . . . . . 8
⊢
(1...𝑀) = (∅
∪ (1...𝑀)) |
49 | 45, 48 | syl6reqr 2809 |
. . . . . . 7
⊢
((⌊‘(𝑀 /
2)) = 0 → (1...𝑀) =
((1...(⌊‘(𝑀 /
2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))) |
50 | | fzsplit 12556 |
. . . . . . . 8
⊢
((⌊‘(𝑀 /
2)) ∈ (1...𝑀) →
(1...𝑀) =
((1...(⌊‘(𝑀 /
2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))) |
51 | 42 | oveq1i 6819 |
. . . . . . . 8
⊢ ((0 +
1)...𝑀) = (1...𝑀) |
52 | 50, 51 | eleq2s 2853 |
. . . . . . 7
⊢
((⌊‘(𝑀 /
2)) ∈ ((0 + 1)...𝑀)
→ (1...𝑀) =
((1...(⌊‘(𝑀 /
2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))) |
53 | 49, 52 | jaoi 393 |
. . . . . 6
⊢
(((⌊‘(𝑀
/ 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀)) → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))) |
54 | 37, 53 | syl 17 |
. . . . 5
⊢ (𝜑 → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))) |
55 | | fzfid 12962 |
. . . . 5
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
56 | 2 | eldifad 3723 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∈ ℙ) |
57 | | prmnn 15586 |
. . . . . . . . . . . 12
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℕ) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ ℕ) |
59 | 58 | nnred 11223 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄 ∈ ℝ) |
60 | 1 | eldifad 3723 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ ℙ) |
61 | | prmnn 15586 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
62 | 60, 61 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℕ) |
63 | 59, 62 | nndivred 11257 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄 / 𝑃) ∈ ℝ) |
64 | 63 | adantr 472 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (𝑄 / 𝑃) ∈ ℝ) |
65 | | 2nn 11373 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
66 | | elfznn 12559 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (1...𝑀) → 𝑢 ∈ ℕ) |
67 | 66 | adantl 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → 𝑢 ∈ ℕ) |
68 | | nnmulcl 11231 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ 𝑢
∈ ℕ) → (2 · 𝑢) ∈ ℕ) |
69 | 65, 67, 68 | sylancr 698 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℕ) |
70 | 69 | nnred 11223 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℝ) |
71 | 64, 70 | remulcld 10258 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) |
72 | 58 | nnrpd 12059 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈
ℝ+) |
73 | 62 | nnrpd 12059 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈
ℝ+) |
74 | 72, 73 | rpdivcld 12078 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑄 / 𝑃) ∈
ℝ+) |
75 | 74 | adantr 472 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (𝑄 / 𝑃) ∈
ℝ+) |
76 | 69 | nnrpd 12059 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈
ℝ+) |
77 | 75, 76 | rpmulcld 12077 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈
ℝ+) |
78 | 77 | rpge0d 12065 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → 0 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))) |
79 | | flge0nn0 12811 |
. . . . . . 7
⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 0 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
80 | 71, 78, 79 | syl2anc 696 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
81 | 80 | nn0cnd 11541 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ) |
82 | 17, 54, 55, 81 | fsumsplit 14666 |
. . . 4
⊢ (𝜑 → Σ𝑢 ∈ (1...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
83 | 7, 82 | syl5eqr 2804 |
. . 3
⊢ (𝜑 → Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
84 | 83 | oveq2d 6825 |
. 2
⊢ (𝜑 → (-1↑Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
85 | | neg1cn 11312 |
. . . . 5
⊢ -1 ∈
ℂ |
86 | 85 | a1i 11 |
. . . 4
⊢ (𝜑 → -1 ∈
ℂ) |
87 | | fzfid 12962 |
. . . . 5
⊢ (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin) |
88 | | ssun2 3916 |
. . . . . . . 8
⊢
(((⌊‘(𝑀
/ 2)) + 1)...𝑀) ⊆
((1...(⌊‘(𝑀 /
2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) |
89 | 88, 54 | syl5sseqr 3791 |
. . . . . . 7
⊢ (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ⊆ (1...𝑀)) |
90 | 89 | sselda 3740 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ (1...𝑀)) |
91 | 90, 80 | syldan 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
92 | 87, 91 | fsumnn0cl 14662 |
. . . 4
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
93 | | fzfid 12962 |
. . . . 5
⊢ (𝜑 → (1...(⌊‘(𝑀 / 2))) ∈
Fin) |
94 | | ssun1 3915 |
. . . . . . . 8
⊢
(1...(⌊‘(𝑀 / 2))) ⊆ ((1...(⌊‘(𝑀 / 2))) ∪
(((⌊‘(𝑀 / 2)) +
1)...𝑀)) |
95 | 94, 54 | syl5sseqr 3791 |
. . . . . . 7
⊢ (𝜑 → (1...(⌊‘(𝑀 / 2))) ⊆ (1...𝑀)) |
96 | 95 | sselda 3740 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ (1...𝑀)) |
97 | 96, 80 | syldan 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
98 | 93, 97 | fsumnn0cl 14662 |
. . . 4
⊢ (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
99 | 86, 92, 98 | expaddd 13200 |
. . 3
⊢ (𝜑 → (-1↑(Σ𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
100 | | fzfid 12962 |
. . . . . . . . 9
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
101 | | xpfi 8392 |
. . . . . . . . 9
⊢
(((1...𝑀) ∈ Fin
∧ (1...𝑁) ∈ Fin)
→ ((1...𝑀) ×
(1...𝑁)) ∈
Fin) |
102 | 55, 100, 101 | syl2anc 696 |
. . . . . . . 8
⊢ (𝜑 → ((1...𝑀) × (1...𝑁)) ∈ Fin) |
103 | | lgsquad.6 |
. . . . . . . . 9
⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} |
104 | | opabssxp 5346 |
. . . . . . . . 9
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁)) |
105 | 103, 104 | eqsstri 3772 |
. . . . . . . 8
⊢ 𝑆 ⊆ ((1...𝑀) × (1...𝑁)) |
106 | | ssfi 8341 |
. . . . . . . 8
⊢
((((1...𝑀) ×
(1...𝑁)) ∈ Fin ∧
𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin) |
107 | 102, 105,
106 | sylancl 697 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ Fin) |
108 | | ssrab2 3824 |
. . . . . . 7
⊢ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ⊆ 𝑆 |
109 | | ssfi 8341 |
. . . . . . 7
⊢ ((𝑆 ∈ Fin ∧ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ⊆ 𝑆) → {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
110 | 107, 108,
109 | sylancl 697 |
. . . . . 6
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
111 | | hashcl 13335 |
. . . . . 6
⊢ ({𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈ Fin
→ (♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)}) ∈
ℕ0) |
112 | 110, 111 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) ∈
ℕ0) |
113 | | ssrab2 3824 |
. . . . . . 7
⊢ {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ⊆ 𝑆 |
114 | | ssfi 8341 |
. . . . . . 7
⊢ ((𝑆 ∈ Fin ∧ {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ⊆ 𝑆) → {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
115 | 107, 113,
114 | sylancl 697 |
. . . . . 6
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
116 | | hashcl 13335 |
. . . . . 6
⊢ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∈ Fin
→ (♯‘{𝑧
∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)})
∈ ℕ0) |
117 | 115, 116 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)}) ∈
ℕ0) |
118 | 86, 112, 117 | expaddd 13200 |
. . . 4
⊢ (𝜑 →
(-1↑((♯‘{𝑧
∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)})
+ (♯‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)}))) = ((-1↑(♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)})) ·
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})))) |
119 | 96, 69 | syldan 488 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 ·
𝑢) ∈
ℕ) |
120 | | fzfid 12962 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) ∈
Fin) |
121 | | xpsnen2g 8214 |
. . . . . . . . . . 11
⊢ (((2
· 𝑢) ∈ ℕ
∧ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ Fin) → ({(2 · 𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) ≈
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) |
122 | 119, 120,
121 | syl2anc 696 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 ·
𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) ≈
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) |
123 | | hasheni 13326 |
. . . . . . . . . 10
⊢ (({(2
· 𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) ≈
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) →
(♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) =
(♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
124 | 122, 123 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) =
(♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
125 | | ssrab2 3824 |
. . . . . . . . . . . . 13
⊢ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ⊆ 𝑆 |
126 | 103 | relopabi 5397 |
. . . . . . . . . . . . 13
⊢ Rel 𝑆 |
127 | | relss 5359 |
. . . . . . . . . . . . 13
⊢ ({𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ⊆ 𝑆 → (Rel 𝑆 → Rel {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) |
128 | 125, 126,
127 | mp2 9 |
. . . . . . . . . . . 12
⊢ Rel
{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} |
129 | | relxp 5279 |
. . . . . . . . . . . 12
⊢ Rel ({(2
· 𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) |
130 | 103 | eleq2i 2827 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ 𝑆 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}) |
131 | | opabid 5128 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) |
132 | 130, 131 | bitri 264 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ 𝑆 ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) |
133 | | anass 684 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))))) |
134 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈
ℕ) |
135 | 62 | ad2antrr 764 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℕ) |
136 | 134, 135 | nnmulcld 11256 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℕ) |
137 | 136 | nnred 11223 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℝ) |
138 | 58 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑄 ∈
ℕ) |
139 | 138, 119 | nnmulcld 11256 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑄 · (2 · 𝑢)) ∈
ℕ) |
140 | 139 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈
ℕ) |
141 | 140 | nnred 11223 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈
ℝ) |
142 | 137, 141 | ltlend 10370 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃)))) |
143 | 119 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) ∈
ℕ) |
144 | 143 | nnred 11223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) ∈
ℝ) |
145 | 135 | nnred 11223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℝ) |
146 | 145 | rehalfcld 11467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 / 2) ∈
ℝ) |
147 | 11 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑀 ∈
ℝ) |
148 | 147 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑀 ∈
ℝ) |
149 | | elfzle2 12534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑢 ∈
(1...(⌊‘(𝑀 /
2))) → 𝑢 ≤
(⌊‘(𝑀 /
2))) |
150 | 149 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ≤ (⌊‘(𝑀 / 2))) |
151 | 147 | rehalfcld 11467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑀 / 2) ∈
ℝ) |
152 | | elfzelz 12531 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑢 ∈
(1...(⌊‘(𝑀 /
2))) → 𝑢 ∈
ℤ) |
153 | 152 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈
ℤ) |
154 | | flge 12796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑀 / 2) ∈ ℝ ∧ 𝑢 ∈ ℤ) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2)))) |
155 | 151, 153,
154 | syl2anc 696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2)))) |
156 | 150, 155 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ≤ (𝑀 / 2)) |
157 | | elfznn 12559 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑢 ∈
(1...(⌊‘(𝑀 /
2))) → 𝑢 ∈
ℕ) |
158 | 157 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈
ℕ) |
159 | 158 | nnred 11223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈
ℝ) |
160 | | 2re 11278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 2 ∈
ℝ |
161 | 160 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 2 ∈
ℝ) |
162 | | 2pos 11300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 0 <
2 |
163 | 162 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 0 <
2) |
164 | | lemuldiv2 11092 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑢 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → ((2 · 𝑢) ≤ 𝑀 ↔ 𝑢 ≤ (𝑀 / 2))) |
165 | 159, 147,
161, 163, 164 | syl112anc 1481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 ·
𝑢) ≤ 𝑀 ↔ 𝑢 ≤ (𝑀 / 2))) |
166 | 156, 165 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 ·
𝑢) ≤ 𝑀) |
167 | 166 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) ≤ 𝑀) |
168 | 145 | ltm1d 11144 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 − 1) < 𝑃) |
169 | | peano2rem 10536 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈
ℝ) |
170 | 145, 169 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 − 1) ∈
ℝ) |
171 | 160 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ∈
ℝ) |
172 | 162 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 <
2) |
173 | | ltdiv1 11075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑃 − 1) ∈ ℝ ∧
𝑃 ∈ ℝ ∧ (2
∈ ℝ ∧ 0 < 2)) → ((𝑃 − 1) < 𝑃 ↔ ((𝑃 − 1) / 2) < (𝑃 / 2))) |
174 | 170, 145,
171, 172, 173 | syl112anc 1481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 − 1) < 𝑃 ↔ ((𝑃 − 1) / 2) < (𝑃 / 2))) |
175 | 168, 174 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 − 1) / 2) < (𝑃 / 2)) |
176 | 5, 175 | syl5eqbr 4835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑀 < (𝑃 / 2)) |
177 | 144, 148,
146, 167, 176 | lelttrd 10383 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) < (𝑃 / 2)) |
178 | 135 | nnrpd 12059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℝ+) |
179 | | rphalflt 12049 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℝ+
→ (𝑃 / 2) < 𝑃) |
180 | 178, 179 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 / 2) < 𝑃) |
181 | 144, 146,
145, 177, 180 | lttrd 10386 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) < 𝑃) |
182 | 144, 145 | ltnled 10372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((2
· 𝑢) < 𝑃 ↔ ¬ 𝑃 ≤ (2 · 𝑢))) |
183 | 181, 182 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬
𝑃 ≤ (2 · 𝑢)) |
184 | 60 | ad2antrr 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℙ) |
185 | | prmz 15587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
186 | 184, 185 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℤ) |
187 | | dvdsle 15230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ ℤ ∧ (2
· 𝑢) ∈ ℕ)
→ (𝑃 ∥ (2
· 𝑢) → 𝑃 ≤ (2 · 𝑢))) |
188 | 186, 143,
187 | syl2anc 696 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ (2 · 𝑢) → 𝑃 ≤ (2 · 𝑢))) |
189 | 183, 188 | mtod 189 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬
𝑃 ∥ (2 · 𝑢)) |
190 | | prmrp 15622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄)) |
191 | 60, 56, 190 | syl2anc 696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄)) |
192 | 3, 191 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝑃 gcd 𝑄) = 1) |
193 | 192 | ad2antrr 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 gcd 𝑄) = 1) |
194 | 56 | ad2antrr 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈
ℙ) |
195 | | prmz 15587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℤ) |
196 | 194, 195 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈
ℤ) |
197 | 143 | nnzd 11669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) ∈
ℤ) |
198 | | coprmdvds 15564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ (2
· 𝑢) ∈ ℤ)
→ ((𝑃 ∥ (𝑄 · (2 · 𝑢)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑢))) |
199 | 186, 196,
197, 198 | syl3anc 1477 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 ∥ (𝑄 · (2 · 𝑢)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑢))) |
200 | 193, 199 | mpan2d 712 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ (𝑄 · (2 · 𝑢)) → 𝑃 ∥ (2 · 𝑢))) |
201 | 189, 200 | mtod 189 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬
𝑃 ∥ (𝑄 · (2 · 𝑢))) |
202 | | nnz 11587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
203 | 202 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈
ℤ) |
204 | | dvdsmul2 15202 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑃 ∥ (𝑦 · 𝑃)) |
205 | 203, 186,
204 | syl2anc 696 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∥ (𝑦 · 𝑃)) |
206 | | breq2 4804 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑄 · (2 · 𝑢)) = (𝑦 · 𝑃) → (𝑃 ∥ (𝑄 · (2 · 𝑢)) ↔ 𝑃 ∥ (𝑦 · 𝑃))) |
207 | 205, 206 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 · (2 · 𝑢)) = (𝑦 · 𝑃) → 𝑃 ∥ (𝑄 · (2 · 𝑢)))) |
208 | 207 | necon3bd 2942 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (¬
𝑃 ∥ (𝑄 · (2 · 𝑢)) → (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃))) |
209 | 201, 208 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃)) |
210 | 209 | biantrud 529 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃)))) |
211 | 142, 210 | bitr4d 271 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ (𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)))) |
212 | | nnre 11215 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
213 | 212 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈
ℝ) |
214 | 135 | nngt0d 11252 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 <
𝑃) |
215 | | lemuldiv 11091 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 <
𝑃)) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))) |
216 | 213, 141,
145, 214, 215 | syl112anc 1481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))) |
217 | 138 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈
ℕ) |
218 | 217 | nncnd 11224 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈
ℂ) |
219 | 143 | nncnd 11224 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) ∈
ℂ) |
220 | 135 | nncnd 11224 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℂ) |
221 | 135 | nnne0d 11253 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ≠ 0) |
222 | 218, 219,
220, 221 | div23d 11026 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 · (2 · 𝑢)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑢))) |
223 | 222 | breq2d 4812 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃) ↔ 𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))) |
224 | 211, 216,
223 | 3bitrd 294 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))) |
225 | 217 | nnred 11223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈
ℝ) |
226 | 217 | nngt0d 11252 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 <
𝑄) |
227 | | ltmul2 11062 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((2
· 𝑢) ∈ ℝ
∧ (𝑃 / 2) ∈
ℝ ∧ (𝑄 ∈
ℝ ∧ 0 < 𝑄))
→ ((2 · 𝑢) <
(𝑃 / 2) ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2)))) |
228 | 144, 146,
225, 226, 227 | syl112anc 1481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((2
· 𝑢) < (𝑃 / 2) ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2)))) |
229 | 177, 228 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2))) |
230 | | 2cnd 11281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ∈
ℂ) |
231 | | 2ne0 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 2 ≠
0 |
232 | 231 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ≠
0) |
233 | | divass 10891 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → ((𝑄 · 𝑃) / 2) = (𝑄 · (𝑃 / 2))) |
234 | | div23 10892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → ((𝑄 · 𝑃) / 2) = ((𝑄 / 2) · 𝑃)) |
235 | 233, 234 | eqtr3d 2792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → (𝑄 · (𝑃 / 2)) = ((𝑄 / 2) · 𝑃)) |
236 | 218, 220,
230, 232, 235 | syl112anc 1481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (𝑃 / 2)) = ((𝑄 / 2) · 𝑃)) |
237 | 229, 236 | breqtrd 4826 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) |
238 | 225 | rehalfcld 11467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 / 2) ∈
ℝ) |
239 | 238, 145 | remulcld 10258 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 2) · 𝑃) ∈ ℝ) |
240 | | lttr 10302 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑦 · 𝑃) ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ ((𝑄 / 2) · 𝑃) ∈ ℝ) → (((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃))) |
241 | 137, 141,
239, 240 | syl3anc 1477 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃))) |
242 | 237, 241 | mpan2d 712 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃))) |
243 | | ltmul1 11061 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ (𝑄 / 2) ∈ ℝ ∧
(𝑃 ∈ ℝ ∧ 0
< 𝑃)) → (𝑦 < (𝑄 / 2) ↔ (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃))) |
244 | 213, 238,
145, 214, 243 | syl112anc 1481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 / 2) ↔ (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃))) |
245 | 242, 244 | sylibrd 249 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 < (𝑄 / 2))) |
246 | | peano2rem 10536 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑄 ∈ ℝ → (𝑄 − 1) ∈
ℝ) |
247 | 225, 246 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − 1) ∈
ℝ) |
248 | 247 | recnd 10256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − 1) ∈
ℂ) |
249 | 218, 248,
230, 232 | divsubdird 11028 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = ((𝑄 / 2) − ((𝑄 − 1) / 2))) |
250 | | lgsquad.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝑁 = ((𝑄 − 1) / 2) |
251 | 250 | oveq2i 6820 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑄 / 2) − 𝑁) = ((𝑄 / 2) − ((𝑄 − 1) / 2)) |
252 | 249, 251 | syl6eqr 2808 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = ((𝑄 / 2) − 𝑁)) |
253 | | ax-1cn 10182 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 1 ∈
ℂ |
254 | | nncan 10498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑄 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑄 −
(𝑄 − 1)) =
1) |
255 | 218, 253,
254 | sylancl 697 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − (𝑄 − 1)) = 1) |
256 | 255 | oveq1d 6824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = (1 /
2)) |
257 | | halflt1 11438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (1 / 2)
< 1 |
258 | 256, 257 | syl6eqbr 4839 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) < 1) |
259 | 252, 258 | eqbrtrrd 4824 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 2) − 𝑁) < 1) |
260 | | oddprm 15713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑄 ∈ (ℙ ∖ {2})
→ ((𝑄 − 1) / 2)
∈ ℕ) |
261 | 2, 260 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → ((𝑄 − 1) / 2) ∈
ℕ) |
262 | 250, 261 | syl5eqel 2839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑁 ∈ ℕ) |
263 | 262 | ad2antrr 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈
ℕ) |
264 | 263 | nnred 11223 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈
ℝ) |
265 | | 1red 10243 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 1 ∈
ℝ) |
266 | 238, 264,
265 | ltsubadd2d 10813 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (((𝑄 / 2) − 𝑁) < 1 ↔ (𝑄 / 2) < (𝑁 + 1))) |
267 | 259, 266 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 / 2) < (𝑁 + 1)) |
268 | | peano2re 10397 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈
ℝ) |
269 | 264, 268 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑁 + 1) ∈
ℝ) |
270 | | lttr 10302 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ (𝑄 / 2) ∈ ℝ ∧
(𝑁 + 1) ∈ ℝ)
→ ((𝑦 < (𝑄 / 2) ∧ (𝑄 / 2) < (𝑁 + 1)) → 𝑦 < (𝑁 + 1))) |
271 | 213, 238,
269, 270 | syl3anc 1477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 < (𝑄 / 2) ∧ (𝑄 / 2) < (𝑁 + 1)) → 𝑦 < (𝑁 + 1))) |
272 | 267, 271 | mpan2d 712 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 / 2) → 𝑦 < (𝑁 + 1))) |
273 | 245, 272 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 < (𝑁 + 1))) |
274 | | nnleltp1 11620 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑦 ≤ 𝑁 ↔ 𝑦 < (𝑁 + 1))) |
275 | 134, 263,
274 | syl2anc 696 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ 𝑁 ↔ 𝑦 < (𝑁 + 1))) |
276 | 273, 275 | sylibrd 249 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 ≤ 𝑁)) |
277 | 276 | pm4.71rd 670 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))))) |
278 | 96, 71 | syldan 488 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) |
279 | | flge 12796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑦 ∈ ℤ) → (𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
280 | 278, 202,
279 | syl2an 495 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
281 | 224, 277,
280 | 3bitr3d 298 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
282 | 281 | pm5.32da 676 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
283 | 133, 282 | syl5bb 272 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
284 | 283 | adantr 472 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
285 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑥 = (2 · 𝑢)) |
286 | | nnuz 11912 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ℕ =
(ℤ≥‘1) |
287 | 119, 286 | syl6eleq 2845 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 ·
𝑢) ∈
(ℤ≥‘1)) |
288 | 26 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑀 ∈
ℤ) |
289 | | elfz5 12523 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((2
· 𝑢) ∈
(ℤ≥‘1) ∧ 𝑀 ∈ ℤ) → ((2 · 𝑢) ∈ (1...𝑀) ↔ (2 · 𝑢) ≤ 𝑀)) |
290 | 287, 288,
289 | syl2anc 696 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 ·
𝑢) ∈ (1...𝑀) ↔ (2 · 𝑢) ≤ 𝑀)) |
291 | 166, 290 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 ·
𝑢) ∈ (1...𝑀)) |
292 | 291 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (2 · 𝑢) ∈ (1...𝑀)) |
293 | 285, 292 | eqeltrd 2835 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑥 ∈ (1...𝑀)) |
294 | 293 | biantrurd 530 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...𝑁) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)))) |
295 | 262 | nnzd 11669 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℤ) |
296 | 295 | ad2antrr 764 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑁 ∈ ℤ) |
297 | | fznn 12597 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℤ → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁))) |
298 | 296, 297 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁))) |
299 | 294, 298 | bitr3d 270 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁))) |
300 | | oveq1 6816 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (2 · 𝑢) → (𝑥 · 𝑄) = ((2 · 𝑢) · 𝑄)) |
301 | 119 | nncnd 11224 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 ·
𝑢) ∈
ℂ) |
302 | 138 | nncnd 11224 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑄 ∈
ℂ) |
303 | 301, 302 | mulcomd 10249 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 ·
𝑢) · 𝑄) = (𝑄 · (2 · 𝑢))) |
304 | 300, 303 | sylan9eqr 2812 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑥 · 𝑄) = (𝑄 · (2 · 𝑢))) |
305 | 304 | breq2d 4812 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → ((𝑦 · 𝑃) < (𝑥 · 𝑄) ↔ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))) |
306 | 299, 305 | anbi12d 749 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ ((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))))) |
307 | 278 | flcld 12789 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℤ) |
308 | | fznn 12597 |
. . . . . . . . . . . . . . . . . 18
⊢
((⌊‘((𝑄
/ 𝑃) · (2 ·
𝑢))) ∈ ℤ →
(𝑦 ∈
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
309 | 307, 308 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑦 ∈
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
310 | 309 | adantr 472 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
311 | 284, 306,
310 | 3bitr4d 300 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
312 | 132, 311 | syl5bb 272 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (〈𝑥, 𝑦〉 ∈ 𝑆 ↔ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
313 | 312 | pm5.32da 676 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑥 = (2 · 𝑢) ∧ 〈𝑥, 𝑦〉 ∈ 𝑆) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
314 | | vex 3339 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑥 ∈ V |
315 | | vex 3339 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑦 ∈ V |
316 | 314, 315 | op1std 7339 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) |
317 | 316 | eqeq2d 2766 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((2 · 𝑢) = (1st ‘𝑧) ↔ (2 · 𝑢) = 𝑥)) |
318 | | eqcom 2763 |
. . . . . . . . . . . . . . . 16
⊢ ((2
· 𝑢) = 𝑥 ↔ 𝑥 = (2 · 𝑢)) |
319 | 317, 318 | syl6bb 276 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((2 · 𝑢) = (1st ‘𝑧) ↔ 𝑥 = (2 · 𝑢))) |
320 | 319 | elrab 3500 |
. . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑦〉 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ↔ (〈𝑥, 𝑦〉 ∈ 𝑆 ∧ 𝑥 = (2 · 𝑢))) |
321 | | ancom 465 |
. . . . . . . . . . . . . 14
⊢
((〈𝑥, 𝑦〉 ∈ 𝑆 ∧ 𝑥 = (2 · 𝑢)) ↔ (𝑥 = (2 · 𝑢) ∧ 〈𝑥, 𝑦〉 ∈ 𝑆)) |
322 | 320, 321 | bitri 264 |
. . . . . . . . . . . . 13
⊢
(〈𝑥, 𝑦〉 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ↔ (𝑥 = (2 · 𝑢) ∧ 〈𝑥, 𝑦〉 ∈ 𝑆)) |
323 | | opelxp 5299 |
. . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑦〉 ∈ ({(2 ·
𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) ↔ (𝑥 ∈ {(2 · 𝑢)} ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
324 | | velsn 4333 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ {(2 · 𝑢)} ↔ 𝑥 = (2 · 𝑢)) |
325 | 324 | anbi1i 733 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ {(2 · 𝑢)} ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
326 | 323, 325 | bitri 264 |
. . . . . . . . . . . . 13
⊢
(〈𝑥, 𝑦〉 ∈ ({(2 ·
𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
327 | 313, 322,
326 | 3bitr4g 303 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (〈𝑥, 𝑦〉 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ↔ 〈𝑥, 𝑦〉 ∈ ({(2 · 𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))))) |
328 | 128, 129,
327 | eqrelrdv 5369 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} = ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
329 | 328 | eqcomd 2762 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 ·
𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) = {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}) |
330 | 329 | fveq2d 6352 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (♯‘{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) |
331 | | hashfz1 13324 |
. . . . . . . . . 10
⊢
((⌊‘((𝑄
/ 𝑃) · (2 ·
𝑢))) ∈
ℕ0 → (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) |
332 | 97, 331 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) |
333 | 124, 330,
332 | 3eqtr3rd 2799 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (♯‘{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) |
334 | 333 | sumeq2dv 14628 |
. . . . . . 7
⊢ (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(♯‘{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) |
335 | 107 | adantr 472 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑆 ∈ Fin) |
336 | | ssfi 8341 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Fin ∧ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ⊆ 𝑆) → {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ∈ Fin) |
337 | 335, 125,
336 | sylancl 697 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ∈ Fin) |
338 | | fveq2 6348 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑣 → (1st ‘𝑧) = (1st ‘𝑣)) |
339 | 338 | eqeq2d 2766 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑣 → ((2 · 𝑢) = (1st ‘𝑧) ↔ (2 · 𝑢) = (1st ‘𝑣))) |
340 | 339 | elrab 3500 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ↔ (𝑣 ∈ 𝑆 ∧ (2 · 𝑢) = (1st ‘𝑣))) |
341 | 340 | simprbi 483 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} → (2 · 𝑢) = (1st ‘𝑣)) |
342 | 341 | ad2antll 767 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → (2 · 𝑢) = (1st ‘𝑣)) |
343 | 342 | oveq1d 6824 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → ((2 · 𝑢) / 2) = ((1st ‘𝑣) / 2)) |
344 | 158 | nncnd 11224 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈
ℂ) |
345 | 344 | adantrr 755 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → 𝑢 ∈ ℂ) |
346 | | 2cnd 11281 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → 2 ∈
ℂ) |
347 | 231 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → 2 ≠ 0) |
348 | 345, 346,
347 | divcan3d 10994 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → ((2 · 𝑢) / 2) = 𝑢) |
349 | 343, 348 | eqtr3d 2792 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → ((1st ‘𝑣) / 2) = 𝑢) |
350 | 349 | ralrimivva 3105 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑢 ∈ (1...(⌊‘(𝑀 / 2)))∀𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ((1st ‘𝑣) / 2) = 𝑢) |
351 | | invdisj 4786 |
. . . . . . . . 9
⊢
(∀𝑢 ∈
(1...(⌊‘(𝑀 /
2)))∀𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ((1st ‘𝑣) / 2) = 𝑢 → Disj 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}) |
352 | 350, 351 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → Disj 𝑢 ∈
(1...(⌊‘(𝑀 /
2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}) |
353 | 93, 337, 352 | hashiun 14749 |
. . . . . . 7
⊢ (𝜑 → (♯‘∪ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}) = Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(♯‘{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) |
354 | | iunrab 4715 |
. . . . . . . . 9
⊢ ∪ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} = {𝑧 ∈ 𝑆 ∣ ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧)} |
355 | | 2cn 11279 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
356 | | zcn 11570 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ℤ → 𝑢 ∈
ℂ) |
357 | 356 | adantl 473 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ ℤ) → 𝑢 ∈ ℂ) |
358 | | mulcom 10210 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℂ ∧ 𝑢
∈ ℂ) → (2 · 𝑢) = (𝑢 · 2)) |
359 | 355, 357,
358 | sylancr 698 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ ℤ) → (2 · 𝑢) = (𝑢 · 2)) |
360 | 359 | eqeq1d 2758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ ℤ) → ((2 · 𝑢) = (1st ‘𝑧) ↔ (𝑢 · 2) = (1st ‘𝑧))) |
361 | 360 | rexbidva 3183 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ ℤ (2 · 𝑢) = (1st ‘𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st
‘𝑧))) |
362 | 152 | anim1i 593 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈
(1...(⌊‘(𝑀 /
2))) ∧ (2 · 𝑢) =
(1st ‘𝑧))
→ (𝑢 ∈ ℤ
∧ (2 · 𝑢) =
(1st ‘𝑧))) |
363 | 362 | reximi2 3144 |
. . . . . . . . . . . 12
⊢
(∃𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(2 · 𝑢) =
(1st ‘𝑧)
→ ∃𝑢 ∈
ℤ (2 · 𝑢) =
(1st ‘𝑧)) |
364 | | simprr 813 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (2 · 𝑢) = (1st ‘𝑧)) |
365 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆) |
366 | 105, 365 | sseldi 3738 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ ((1...𝑀) × (1...𝑁))) |
367 | | xp1st 7361 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ ((1...𝑀) × (1...𝑁)) → (1st ‘𝑧) ∈ (1...𝑀)) |
368 | 366, 367 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (1st ‘𝑧) ∈ (1...𝑀)) |
369 | 368 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (1st
‘𝑧) ∈ (1...𝑀)) |
370 | | elfzle2 12534 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑧) ∈ (1...𝑀) → (1st ‘𝑧) ≤ 𝑀) |
371 | 369, 370 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (1st
‘𝑧) ≤ 𝑀) |
372 | 364, 371 | eqbrtrd 4822 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (2 · 𝑢) ≤ 𝑀) |
373 | | zre 11569 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ ℤ → 𝑢 ∈
ℝ) |
374 | 373 | ad2antrl 766 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈ ℝ) |
375 | 11 | ad2antrr 764 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑀 ∈ ℝ) |
376 | 160 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 2 ∈
ℝ) |
377 | 162 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 0 <
2) |
378 | 374, 375,
376, 377, 164 | syl112anc 1481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → ((2 · 𝑢) ≤ 𝑀 ↔ 𝑢 ≤ (𝑀 / 2))) |
379 | 372, 378 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ≤ (𝑀 / 2)) |
380 | 12 | ad2antrr 764 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (𝑀 / 2) ∈ ℝ) |
381 | | simprl 811 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈ ℤ) |
382 | 380, 381,
154 | syl2anc 696 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2)))) |
383 | 379, 382 | mpbid 222 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ≤ (⌊‘(𝑀 / 2))) |
384 | | 2t0e0 11371 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
· 0) = 0 |
385 | | elfznn 12559 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((1st ‘𝑧) ∈ (1...𝑀) → (1st ‘𝑧) ∈
ℕ) |
386 | 369, 385 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (1st
‘𝑧) ∈
ℕ) |
387 | 364, 386 | eqeltrd 2835 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (2 · 𝑢) ∈
ℕ) |
388 | 387 | nngt0d 11252 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 0 < (2 ·
𝑢)) |
389 | 384, 388 | syl5eqbr 4835 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (2 · 0) <
(2 · 𝑢)) |
390 | | 0red 10229 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 0 ∈
ℝ) |
391 | | ltmul2 11062 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0
∈ ℝ ∧ 𝑢
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (0 < 𝑢 ↔ (2 · 0) < (2
· 𝑢))) |
392 | 390, 374,
376, 377, 391 | syl112anc 1481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (0 < 𝑢 ↔ (2 · 0) < (2
· 𝑢))) |
393 | 389, 392 | mpbird 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 0 < 𝑢) |
394 | | elnnz 11575 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ ℕ ↔ (𝑢 ∈ ℤ ∧ 0 <
𝑢)) |
395 | 381, 393,
394 | sylanbrc 701 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈ ℕ) |
396 | 395, 286 | syl6eleq 2845 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈
(ℤ≥‘1)) |
397 | 13 | ad2antrr 764 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (⌊‘(𝑀 / 2)) ∈
ℤ) |
398 | | elfz5 12523 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈
(ℤ≥‘1) ∧ (⌊‘(𝑀 / 2)) ∈ ℤ) → (𝑢 ∈
(1...(⌊‘(𝑀 /
2))) ↔ 𝑢 ≤
(⌊‘(𝑀 /
2)))) |
399 | 396, 397,
398 | syl2anc 696 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2)))) |
400 | 383, 399 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) |
401 | 400, 364 | jca 555 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st ‘𝑧))) |
402 | 401 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧)) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st ‘𝑧)))) |
403 | 402 | reximdv2 3148 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ ℤ (2 · 𝑢) = (1st ‘𝑧) → ∃𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(2 · 𝑢) =
(1st ‘𝑧))) |
404 | 363, 403 | impbid2 216 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧) ↔ ∃𝑢 ∈ ℤ (2 ·
𝑢) = (1st
‘𝑧))) |
405 | | 2z 11597 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℤ |
406 | | elfzelz 12531 |
. . . . . . . . . . . . 13
⊢
((1st ‘𝑧) ∈ (1...𝑀) → (1st ‘𝑧) ∈
ℤ) |
407 | 368, 406 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (1st ‘𝑧) ∈
ℤ) |
408 | | divides 15180 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℤ ∧ (1st ‘𝑧) ∈ ℤ) → (2 ∥
(1st ‘𝑧)
↔ ∃𝑢 ∈
ℤ (𝑢 · 2) =
(1st ‘𝑧))) |
409 | 405, 407,
408 | sylancr 698 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (2 ∥ (1st
‘𝑧) ↔
∃𝑢 ∈ ℤ
(𝑢 · 2) =
(1st ‘𝑧))) |
410 | 361, 404,
409 | 3bitr4d 300 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧) ↔ 2 ∥
(1st ‘𝑧))) |
411 | 410 | rabbidva 3324 |
. . . . . . . . 9
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧)} = {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)}) |
412 | 354, 411 | syl5eq 2802 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} = {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)}) |
413 | 412 | fveq2d 6352 |
. . . . . . 7
⊢ (𝜑 → (♯‘∪ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}) = (♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)})) |
414 | 334, 353,
413 | 3eqtr2d 2796 |
. . . . . 6
⊢ (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)})) |
415 | 414 | oveq2d 6825 |
. . . . 5
⊢ (𝜑 → (-1↑Σ𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) =
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)}))) |
416 | 1, 2, 3, 5, 250, 103 | lgsquadlem1 25300 |
. . . . 5
⊢ (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) |
417 | 415, 416 | oveq12d 6827 |
. . . 4
⊢ (𝜑 → ((-1↑Σ𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) ·
(-1↑Σ𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = ((-1↑(♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)})) ·
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})))) |
418 | 118, 417 | eqtr4d 2793 |
. . 3
⊢ (𝜑 →
(-1↑((♯‘{𝑧
∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)})
+ (♯‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)}))) = ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
419 | | unrab 4037 |
. . . . . . 7
⊢ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) = {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∨ ¬ 2
∥ (1st ‘𝑧))} |
420 | | exmid 430 |
. . . . . . . . 9
⊢ (2
∥ (1st ‘𝑧) ∨ ¬ 2 ∥ (1st
‘𝑧)) |
421 | 420 | rgenw 3058 |
. . . . . . . 8
⊢
∀𝑧 ∈
𝑆 (2 ∥
(1st ‘𝑧)
∨ ¬ 2 ∥ (1st ‘𝑧)) |
422 | | rabid2 3253 |
. . . . . . . 8
⊢ (𝑆 = {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∨ ¬ 2
∥ (1st ‘𝑧))} ↔ ∀𝑧 ∈ 𝑆 (2 ∥ (1st ‘𝑧) ∨ ¬ 2 ∥
(1st ‘𝑧))) |
423 | 421, 422 | mpbir 221 |
. . . . . . 7
⊢ 𝑆 = {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∨ ¬ 2
∥ (1st ‘𝑧))} |
424 | 419, 423 | eqtr4i 2781 |
. . . . . 6
⊢ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) = 𝑆 |
425 | 424 | fveq2i 6351 |
. . . . 5
⊢
(♯‘({𝑧
∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)}
∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)})) = (♯‘𝑆) |
426 | | inrab 4038 |
. . . . . . 7
⊢ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∩ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) = {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∧ ¬ 2
∥ (1st ‘𝑧))} |
427 | | pm3.24 962 |
. . . . . . . . . 10
⊢ ¬ (2
∥ (1st ‘𝑧) ∧ ¬ 2 ∥ (1st
‘𝑧)) |
428 | 427 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ¬ (2 ∥
(1st ‘𝑧)
∧ ¬ 2 ∥ (1st ‘𝑧))) |
429 | 428 | ralrimivw 3101 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 ¬ (2 ∥ (1st
‘𝑧) ∧ ¬ 2
∥ (1st ‘𝑧))) |
430 | | rabeq0 4096 |
. . . . . . . 8
⊢ ({𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∧ ¬ 2
∥ (1st ‘𝑧))} = ∅ ↔ ∀𝑧 ∈ 𝑆 ¬ (2 ∥ (1st
‘𝑧) ∧ ¬ 2
∥ (1st ‘𝑧))) |
431 | 429, 430 | sylibr 224 |
. . . . . . 7
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∧ ¬ 2
∥ (1st ‘𝑧))} = ∅) |
432 | 426, 431 | syl5eq 2802 |
. . . . . 6
⊢ (𝜑 → ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∩ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) =
∅) |
433 | | hashun 13359 |
. . . . . 6
⊢ (({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∈ Fin ∧
{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈ Fin ∧
({𝑧 ∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)}
∩ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)})
= ∅) → (♯‘({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) =
((♯‘{𝑧 ∈
𝑆 ∣ 2 ∥
(1st ‘𝑧)})
+ (♯‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)}))) |
434 | 115, 110,
432, 433 | syl3anc 1477 |
. . . . 5
⊢ (𝜑 → (♯‘({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) =
((♯‘{𝑧 ∈
𝑆 ∣ 2 ∥
(1st ‘𝑧)})
+ (♯‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)}))) |
435 | 425, 434 | syl5reqr 2805 |
. . . 4
⊢ (𝜑 → ((♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)}) +
(♯‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)})) = (♯‘𝑆)) |
436 | 435 | oveq2d 6825 |
. . 3
⊢ (𝜑 →
(-1↑((♯‘{𝑧
∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)})
+ (♯‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)}))) = (-1↑(♯‘𝑆))) |
437 | 99, 418, 436 | 3eqtr2d 2796 |
. 2
⊢ (𝜑 → (-1↑(Σ𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (-1↑(♯‘𝑆))) |
438 | 4, 84, 437 | 3eqtrd 2794 |
1
⊢ (𝜑 → (𝑄 /L 𝑃) = (-1↑(♯‘𝑆))) |