Step | Hyp | Ref
| Expression |
1 | | lgseisen.1 |
. . 3
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
2 | | lgseisen.2 |
. . 3
⊢ (𝜑 → 𝑄 ∈ (ℙ ∖
{2})) |
3 | | lgseisen.3 |
. . 3
⊢ (𝜑 → 𝑃 ≠ 𝑄) |
4 | 1, 2, 3 | lgseisen 25104 |
. 2
⊢ (𝜑 → (𝑄 /L 𝑃) = (-1↑Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
5 | | lgsquad.4 |
. . . . . 6
⊢ 𝑀 = ((𝑃 − 1) / 2) |
6 | 5 | oveq2i 6661 |
. . . . 5
⊢
(1...𝑀) =
(1...((𝑃 − 1) /
2)) |
7 | 6 | sumeq1i 14428 |
. . . 4
⊢
Σ𝑢 ∈
(1...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) |
8 | | oddprm 15515 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
9 | 1, 8 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ) |
10 | 5, 9 | syl5eqel 2705 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℕ) |
11 | 10 | nnred 11035 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℝ) |
12 | 11 | rehalfcld 11279 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 / 2) ∈ ℝ) |
13 | 12 | flcld 12599 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈
ℤ) |
14 | 13 | zred 11482 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈
ℝ) |
15 | 14 | ltp1d 10954 |
. . . . . 6
⊢ (𝜑 → (⌊‘(𝑀 / 2)) <
((⌊‘(𝑀 / 2)) +
1)) |
16 | | fzdisj 12368 |
. . . . . 6
⊢
((⌊‘(𝑀 /
2)) < ((⌊‘(𝑀
/ 2)) + 1) → ((1...(⌊‘(𝑀 / 2))) ∩ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = ∅) |
17 | 15, 16 | syl 17 |
. . . . 5
⊢ (𝜑 →
((1...(⌊‘(𝑀 /
2))) ∩ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = ∅) |
18 | 10 | nnrpd 11870 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈
ℝ+) |
19 | 18 | rphalfcld 11884 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 / 2) ∈
ℝ+) |
20 | 19 | rpge0d 11876 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (𝑀 / 2)) |
21 | | flge0nn0 12621 |
. . . . . . . . 9
⊢ (((𝑀 / 2) ∈ ℝ ∧ 0
≤ (𝑀 / 2)) →
(⌊‘(𝑀 / 2))
∈ ℕ0) |
22 | 12, 20, 21 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈
ℕ0) |
23 | 10 | nnnn0d 11351 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
24 | | rphalflt 11860 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℝ+
→ (𝑀 / 2) < 𝑀) |
25 | 18, 24 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 / 2) < 𝑀) |
26 | 10 | nnzd 11481 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) |
27 | | fllt 12607 |
. . . . . . . . . . 11
⊢ (((𝑀 / 2) ∈ ℝ ∧ 𝑀 ∈ ℤ) → ((𝑀 / 2) < 𝑀 ↔ (⌊‘(𝑀 / 2)) < 𝑀)) |
28 | 12, 26, 27 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 / 2) < 𝑀 ↔ (⌊‘(𝑀 / 2)) < 𝑀)) |
29 | 25, 28 | mpbid 222 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘(𝑀 / 2)) < 𝑀) |
30 | 14, 11, 29 | ltled 10185 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ≤ 𝑀) |
31 | | elfz2nn0 12431 |
. . . . . . . 8
⊢
((⌊‘(𝑀 /
2)) ∈ (0...𝑀) ↔
((⌊‘(𝑀 / 2))
∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧
(⌊‘(𝑀 / 2))
≤ 𝑀)) |
32 | 22, 23, 30, 31 | syl3anbrc 1246 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈ (0...𝑀)) |
33 | | nn0uz 11722 |
. . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) |
34 | 23, 33 | syl6eleq 2711 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
35 | | elfzp12 12419 |
. . . . . . . 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 6658 |
. . . . . . . . . 10
⊢
((⌊‘(𝑀 /
2)) = 0 → (1...(⌊‘(𝑀 / 2))) = (1...0)) |
39 | | fz10 12362 |
. . . . . . . . . 10
⊢ (1...0) =
∅ |
40 | 38, 39 | syl6eq 2672 |
. . . . . . . . 9
⊢
((⌊‘(𝑀 /
2)) = 0 → (1...(⌊‘(𝑀 / 2))) = ∅) |
41 | | oveq1 6657 |
. . . . . . . . . . 11
⊢
((⌊‘(𝑀 /
2)) = 0 → ((⌊‘(𝑀 / 2)) + 1) = (0 + 1)) |
42 | | 0p1e1 11132 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
43 | 41, 42 | syl6eq 2672 |
. . . . . . . . . 10
⊢
((⌊‘(𝑀 /
2)) = 0 → ((⌊‘(𝑀 / 2)) + 1) = 1) |
44 | 43 | oveq1d 6665 |
. . . . . . . . 9
⊢
((⌊‘(𝑀 /
2)) = 0 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) = (1...𝑀)) |
45 | 40, 44 | uneq12d 3768 |
. . . . . . . 8
⊢
((⌊‘(𝑀 /
2)) = 0 → ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = (∅ ∪ (1...𝑀))) |
46 | | un0 3967 |
. . . . . . . . 9
⊢
((1...𝑀) ∪
∅) = (1...𝑀) |
47 | | uncom 3757 |
. . . . . . . . 9
⊢
((1...𝑀) ∪
∅) = (∅ ∪ (1...𝑀)) |
48 | 46, 47 | eqtr3i 2646 |
. . . . . . . 8
⊢
(1...𝑀) = (∅
∪ (1...𝑀)) |
49 | 45, 48 | syl6reqr 2675 |
. . . . . . 7
⊢
((⌊‘(𝑀 /
2)) = 0 → (1...𝑀) =
((1...(⌊‘(𝑀 /
2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))) |
50 | | fzsplit 12367 |
. . . . . . . 8
⊢
((⌊‘(𝑀 /
2)) ∈ (1...𝑀) →
(1...𝑀) =
((1...(⌊‘(𝑀 /
2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))) |
51 | 42 | oveq1i 6660 |
. . . . . . . 8
⊢ ((0 +
1)...𝑀) = (1...𝑀) |
52 | 50, 51 | eleq2s 2719 |
. . . . . . 7
⊢
((⌊‘(𝑀 /
2)) ∈ ((0 + 1)...𝑀)
→ (1...𝑀) =
((1...(⌊‘(𝑀 /
2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))) |
53 | 49, 52 | jaoi 394 |
. . . . . 6
⊢
(((⌊‘(𝑀
/ 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀)) → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))) |
54 | 37, 53 | syl 17 |
. . . . 5
⊢ (𝜑 → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))) |
55 | | fzfid 12772 |
. . . . 5
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
56 | 2 | eldifad 3586 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∈ ℙ) |
57 | | prmnn 15388 |
. . . . . . . . . . . 12
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℕ) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ ℕ) |
59 | 58 | nnred 11035 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄 ∈ ℝ) |
60 | 1 | eldifad 3586 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ ℙ) |
61 | | prmnn 15388 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
62 | 60, 61 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℕ) |
63 | 59, 62 | nndivred 11069 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄 / 𝑃) ∈ ℝ) |
64 | 63 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (𝑄 / 𝑃) ∈ ℝ) |
65 | | 2nn 11185 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
66 | | elfznn 12370 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (1...𝑀) → 𝑢 ∈ ℕ) |
67 | 66 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → 𝑢 ∈ ℕ) |
68 | | nnmulcl 11043 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ 𝑢
∈ ℕ) → (2 · 𝑢) ∈ ℕ) |
69 | 65, 67, 68 | sylancr 695 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℕ) |
70 | 69 | nnred 11035 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℝ) |
71 | 64, 70 | remulcld 10070 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) |
72 | 58 | nnrpd 11870 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈
ℝ+) |
73 | 62 | nnrpd 11870 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈
ℝ+) |
74 | 72, 73 | rpdivcld 11889 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑄 / 𝑃) ∈
ℝ+) |
75 | 74 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (𝑄 / 𝑃) ∈
ℝ+) |
76 | 69 | nnrpd 11870 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈
ℝ+) |
77 | 75, 76 | rpmulcld 11888 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈
ℝ+) |
78 | 77 | rpge0d 11876 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → 0 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))) |
79 | | flge0nn0 12621 |
. . . . . . 7
⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 0 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
80 | 71, 78, 79 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
81 | 80 | nn0cnd 11353 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ) |
82 | 17, 54, 55, 81 | fsumsplit 14471 |
. . . 4
⊢ (𝜑 → Σ𝑢 ∈ (1...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
83 | 7, 82 | syl5eqr 2670 |
. . 3
⊢ (𝜑 → Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
84 | 83 | oveq2d 6666 |
. 2
⊢ (𝜑 → (-1↑Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
85 | | neg1cn 11124 |
. . . . 5
⊢ -1 ∈
ℂ |
86 | 85 | a1i 11 |
. . . 4
⊢ (𝜑 → -1 ∈
ℂ) |
87 | | fzfid 12772 |
. . . . 5
⊢ (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin) |
88 | | ssun2 3777 |
. . . . . . . 8
⊢
(((⌊‘(𝑀
/ 2)) + 1)...𝑀) ⊆
((1...(⌊‘(𝑀 /
2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) |
89 | 88, 54 | syl5sseqr 3654 |
. . . . . . 7
⊢ (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ⊆ (1...𝑀)) |
90 | 89 | sselda 3603 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ (1...𝑀)) |
91 | 90, 80 | syldan 487 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
92 | 87, 91 | fsumnn0cl 14467 |
. . . 4
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
93 | | fzfid 12772 |
. . . . 5
⊢ (𝜑 → (1...(⌊‘(𝑀 / 2))) ∈
Fin) |
94 | | ssun1 3776 |
. . . . . . . 8
⊢
(1...(⌊‘(𝑀 / 2))) ⊆ ((1...(⌊‘(𝑀 / 2))) ∪
(((⌊‘(𝑀 / 2)) +
1)...𝑀)) |
95 | 94, 54 | syl5sseqr 3654 |
. . . . . . 7
⊢ (𝜑 → (1...(⌊‘(𝑀 / 2))) ⊆ (1...𝑀)) |
96 | 95 | sselda 3603 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ (1...𝑀)) |
97 | 96, 80 | syldan 487 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
98 | 93, 97 | fsumnn0cl 14467 |
. . . 4
⊢ (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℕ0) |
99 | 86, 92, 98 | expaddd 13010 |
. . 3
⊢ (𝜑 → (-1↑(Σ𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
100 | | fzfid 12772 |
. . . . . . . . 9
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
101 | | xpfi 8231 |
. . . . . . . . 9
⊢
(((1...𝑀) ∈ Fin
∧ (1...𝑁) ∈ Fin)
→ ((1...𝑀) ×
(1...𝑁)) ∈
Fin) |
102 | 55, 100, 101 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → ((1...𝑀) × (1...𝑁)) ∈ Fin) |
103 | | lgsquad.6 |
. . . . . . . . 9
⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} |
104 | | opabssxp 5193 |
. . . . . . . . 9
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁)) |
105 | 103, 104 | eqsstri 3635 |
. . . . . . . 8
⊢ 𝑆 ⊆ ((1...𝑀) × (1...𝑁)) |
106 | | ssfi 8180 |
. . . . . . . 8
⊢
((((1...𝑀) ×
(1...𝑁)) ∈ Fin ∧
𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin) |
107 | 102, 105,
106 | sylancl 694 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ Fin) |
108 | | ssrab2 3687 |
. . . . . . 7
⊢ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ⊆ 𝑆 |
109 | | ssfi 8180 |
. . . . . . 7
⊢ ((𝑆 ∈ Fin ∧ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ⊆ 𝑆) → {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
110 | 107, 108,
109 | sylancl 694 |
. . . . . 6
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
111 | | hashcl 13147 |
. . . . . 6
⊢ ({𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈ Fin
→ (#‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)})
∈ ℕ0) |
112 | 110, 111 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) ∈
ℕ0) |
113 | | ssrab2 3687 |
. . . . . . 7
⊢ {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ⊆ 𝑆 |
114 | | ssfi 8180 |
. . . . . . 7
⊢ ((𝑆 ∈ Fin ∧ {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ⊆ 𝑆) → {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
115 | 107, 113,
114 | sylancl 694 |
. . . . . 6
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
116 | | hashcl 13147 |
. . . . . 6
⊢ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∈ Fin
→ (#‘{𝑧 ∈
𝑆 ∣ 2 ∥
(1st ‘𝑧)})
∈ ℕ0) |
117 | 115, 116 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)}) ∈
ℕ0) |
118 | 86, 112, 117 | expaddd 13010 |
. . . 4
⊢ (𝜑 → (-1↑((#‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)}) +
(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)}))) = ((-1↑(#‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)})) ·
(-1↑(#‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)})))) |
119 | 96, 69 | syldan 487 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 ·
𝑢) ∈
ℕ) |
120 | | fzfid 12772 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) ∈
Fin) |
121 | | xpsnen2g 8053 |
. . . . . . . . . . 11
⊢ (((2
· 𝑢) ∈ ℕ
∧ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ Fin) → ({(2 · 𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) ≈
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) |
122 | 119, 120,
121 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 ·
𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) ≈
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) |
123 | | hasheni 13136 |
. . . . . . . . . 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 3687 |
. . . . . . . . . . . . 13
⊢ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ⊆ 𝑆 |
126 | 103 | relopabi 5245 |
. . . . . . . . . . . . 13
⊢ Rel 𝑆 |
127 | | relss 5206 |
. . . . . . . . . . . . 13
⊢ ({𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ⊆ 𝑆 → (Rel 𝑆 → Rel {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) |
128 | 125, 126,
127 | mp2 9 |
. . . . . . . . . . . 12
⊢ Rel
{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} |
129 | | relxp 5227 |
. . . . . . . . . . . 12
⊢ Rel ({(2
· 𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) |
130 | 103 | eleq2i 2693 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ 𝑆 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}) |
131 | | opabid 4982 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) |
132 | 130, 131 | bitri 264 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ 𝑆 ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) |
133 | | anass 681 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))))) |
134 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈
ℕ) |
135 | 62 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℕ) |
136 | 134, 135 | nnmulcld 11068 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℕ) |
137 | 136 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℝ) |
138 | 58 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑄 ∈
ℕ) |
139 | 138, 119 | nnmulcld 11068 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑄 · (2 · 𝑢)) ∈
ℕ) |
140 | 139 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈
ℕ) |
141 | 140 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈
ℝ) |
142 | 137, 141 | ltlend 10182 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃)))) |
143 | 119 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) ∈
ℕ) |
144 | 143 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) ∈
ℝ) |
145 | 135 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℝ) |
146 | 145 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 / 2) ∈
ℝ) |
147 | 11 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑀 ∈
ℝ) |
148 | 147 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑀 ∈
ℝ) |
149 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑢 ∈
(1...(⌊‘(𝑀 /
2))) → 𝑢 ≤
(⌊‘(𝑀 /
2))) |
150 | 149 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ≤ (⌊‘(𝑀 / 2))) |
151 | 147 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑀 / 2) ∈
ℝ) |
152 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑢 ∈
(1...(⌊‘(𝑀 /
2))) → 𝑢 ∈
ℤ) |
153 | 152 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈
ℤ) |
154 | | flge 12606 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑀 / 2) ∈ ℝ ∧ 𝑢 ∈ ℤ) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2)))) |
155 | 151, 153,
154 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2)))) |
156 | 150, 155 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ≤ (𝑀 / 2)) |
157 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑢 ∈
(1...(⌊‘(𝑀 /
2))) → 𝑢 ∈
ℕ) |
158 | 157 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈
ℕ) |
159 | 158 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈
ℝ) |
160 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 2 ∈
ℝ |
161 | 160 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 2 ∈
ℝ) |
162 | | 2pos 11112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 0 <
2 |
163 | 162 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 0 <
2) |
164 | | lemuldiv2 10904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑢 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → ((2 · 𝑢) ≤ 𝑀 ↔ 𝑢 ≤ (𝑀 / 2))) |
165 | 159, 147,
161, 163, 164 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 ·
𝑢) ≤ 𝑀 ↔ 𝑢 ≤ (𝑀 / 2))) |
166 | 156, 165 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 ·
𝑢) ≤ 𝑀) |
167 | 166 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) ≤ 𝑀) |
168 | 145 | ltm1d 10956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 − 1) < 𝑃) |
169 | | peano2rem 10348 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 10887 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑃 − 1) ∈ ℝ ∧
𝑃 ∈ ℝ ∧ (2
∈ ℝ ∧ 0 < 2)) → ((𝑃 − 1) < 𝑃 ↔ ((𝑃 − 1) / 2) < (𝑃 / 2))) |
174 | 170, 145,
171, 172, 173 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 − 1) < 𝑃 ↔ ((𝑃 − 1) / 2) < (𝑃 / 2))) |
175 | 168, 174 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 − 1) / 2) < (𝑃 / 2)) |
176 | 5, 175 | syl5eqbr 4688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑀 < (𝑃 / 2)) |
177 | 144, 148,
146, 167, 176 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) < (𝑃 / 2)) |
178 | 135 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℝ+) |
179 | | rphalflt 11860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℝ+
→ (𝑃 / 2) < 𝑃) |
180 | 178, 179 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 / 2) < 𝑃) |
181 | 144, 146,
145, 177, 180 | lttrd 10198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) < 𝑃) |
182 | 144, 145 | ltnled 10184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((2
· 𝑢) < 𝑃 ↔ ¬ 𝑃 ≤ (2 · 𝑢))) |
183 | 181, 182 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬
𝑃 ≤ (2 · 𝑢)) |
184 | 60 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℙ) |
185 | | prmz 15389 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
186 | 184, 185 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℤ) |
187 | | dvdsle 15032 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ ℤ ∧ (2
· 𝑢) ∈ ℕ)
→ (𝑃 ∥ (2
· 𝑢) → 𝑃 ≤ (2 · 𝑢))) |
188 | 186, 143,
187 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ (2 · 𝑢) → 𝑃 ≤ (2 · 𝑢))) |
189 | 183, 188 | mtod 189 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬
𝑃 ∥ (2 · 𝑢)) |
190 | | prmrp 15424 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄)) |
191 | 60, 56, 190 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄)) |
192 | 3, 191 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝑃 gcd 𝑄) = 1) |
193 | 192 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 gcd 𝑄) = 1) |
194 | 56 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈
ℙ) |
195 | | prmz 15389 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℤ) |
196 | 194, 195 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈
ℤ) |
197 | 143 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) ∈
ℤ) |
198 | | coprmdvds 15366 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ (2
· 𝑢) ∈ ℤ)
→ ((𝑃 ∥ (𝑄 · (2 · 𝑢)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑢))) |
199 | 186, 196,
197, 198 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 ∥ (𝑄 · (2 · 𝑢)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑢))) |
200 | 193, 199 | mpan2d 710 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ (𝑄 · (2 · 𝑢)) → 𝑃 ∥ (2 · 𝑢))) |
201 | 189, 200 | mtod 189 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬
𝑃 ∥ (𝑄 · (2 · 𝑢))) |
202 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
203 | 202 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈
ℤ) |
204 | | dvdsmul2 15004 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑃 ∥ (𝑦 · 𝑃)) |
205 | 203, 186,
204 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∥ (𝑦 · 𝑃)) |
206 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑄 · (2 · 𝑢)) = (𝑦 · 𝑃) → (𝑃 ∥ (𝑄 · (2 · 𝑢)) ↔ 𝑃 ∥ (𝑦 · 𝑃))) |
207 | 205, 206 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 · (2 · 𝑢)) = (𝑦 · 𝑃) → 𝑃 ∥ (𝑄 · (2 · 𝑢)))) |
208 | 207 | necon3bd 2808 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (¬
𝑃 ∥ (𝑄 · (2 · 𝑢)) → (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃))) |
209 | 201, 208 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃)) |
210 | 209 | biantrud 528 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃)))) |
211 | 142, 210 | bitr4d 271 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ (𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)))) |
212 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
213 | 212 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈
ℝ) |
214 | 135 | nngt0d 11064 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 <
𝑃) |
215 | | lemuldiv 10903 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 <
𝑃)) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))) |
216 | 213, 141,
145, 214, 215 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))) |
217 | 138 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈
ℕ) |
218 | 217 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈
ℂ) |
219 | 143 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2
· 𝑢) ∈
ℂ) |
220 | 135 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℂ) |
221 | 135 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ≠ 0) |
222 | 218, 219,
220, 221 | div23d 10838 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 · (2 · 𝑢)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑢))) |
223 | 222 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃) ↔ 𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))) |
224 | 211, 216,
223 | 3bitrd 294 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))) |
225 | 217 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈
ℝ) |
226 | 217 | nngt0d 11064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 <
𝑄) |
227 | | ltmul2 10874 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((2
· 𝑢) ∈ ℝ
∧ (𝑃 / 2) ∈
ℝ ∧ (𝑄 ∈
ℝ ∧ 0 < 𝑄))
→ ((2 · 𝑢) <
(𝑃 / 2) ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2)))) |
228 | 144, 146,
225, 226, 227 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((2
· 𝑢) < (𝑃 / 2) ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2)))) |
229 | 177, 228 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2))) |
230 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ∈
ℂ) |
231 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 2 ≠
0 |
232 | 231 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ≠
0) |
233 | | divass 10703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → ((𝑄 · 𝑃) / 2) = (𝑄 · (𝑃 / 2))) |
234 | | div23 10704 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → ((𝑄 · 𝑃) / 2) = ((𝑄 / 2) · 𝑃)) |
235 | 233, 234 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → (𝑄 · (𝑃 / 2)) = ((𝑄 / 2) · 𝑃)) |
236 | 218, 220,
230, 232, 235 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (𝑃 / 2)) = ((𝑄 / 2) · 𝑃)) |
237 | 229, 236 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) |
238 | 225 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 / 2) ∈
ℝ) |
239 | 238, 145 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 2) · 𝑃) ∈ ℝ) |
240 | | lttr 10114 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑦 · 𝑃) ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ ((𝑄 / 2) · 𝑃) ∈ ℝ) → (((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃))) |
241 | 137, 141,
239, 240 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃))) |
242 | 237, 241 | mpan2d 710 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃))) |
243 | | ltmul1 10873 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ (𝑄 / 2) ∈ ℝ ∧
(𝑃 ∈ ℝ ∧ 0
< 𝑃)) → (𝑦 < (𝑄 / 2) ↔ (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃))) |
244 | 213, 238,
145, 214, 243 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 / 2) ↔ (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃))) |
245 | 242, 244 | sylibrd 249 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 < (𝑄 / 2))) |
246 | | peano2rem 10348 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑄 ∈ ℝ → (𝑄 − 1) ∈
ℝ) |
247 | 225, 246 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − 1) ∈
ℝ) |
248 | 247 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − 1) ∈
ℂ) |
249 | 218, 248,
230, 232 | divsubdird 10840 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = ((𝑄 / 2) − ((𝑄 − 1) / 2))) |
250 | | lgsquad.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝑁 = ((𝑄 − 1) / 2) |
251 | 250 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑄 / 2) − 𝑁) = ((𝑄 / 2) − ((𝑄 − 1) / 2)) |
252 | 249, 251 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = ((𝑄 / 2) − 𝑁)) |
253 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 1 ∈
ℂ |
254 | | nncan 10310 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑄 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑄 −
(𝑄 − 1)) =
1) |
255 | 218, 253,
254 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − (𝑄 − 1)) = 1) |
256 | 255 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = (1 /
2)) |
257 | | halflt1 11250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (1 / 2)
< 1 |
258 | 256, 257 | syl6eqbr 4692 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) < 1) |
259 | 252, 258 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 2) − 𝑁) < 1) |
260 | | oddprm 15515 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑄 ∈ (ℙ ∖ {2})
→ ((𝑄 − 1) / 2)
∈ ℕ) |
261 | 2, 260 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → ((𝑄 − 1) / 2) ∈
ℕ) |
262 | 250, 261 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑁 ∈ ℕ) |
263 | 262 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈
ℕ) |
264 | 263 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈
ℝ) |
265 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 1 ∈
ℝ) |
266 | 238, 264,
265 | ltsubadd2d 10625 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (((𝑄 / 2) − 𝑁) < 1 ↔ (𝑄 / 2) < (𝑁 + 1))) |
267 | 259, 266 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 / 2) < (𝑁 + 1)) |
268 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈
ℝ) |
269 | 264, 268 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑁 + 1) ∈
ℝ) |
270 | | lttr 10114 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ (𝑄 / 2) ∈ ℝ ∧
(𝑁 + 1) ∈ ℝ)
→ ((𝑦 < (𝑄 / 2) ∧ (𝑄 / 2) < (𝑁 + 1)) → 𝑦 < (𝑁 + 1))) |
271 | 213, 238,
269, 270 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 < (𝑄 / 2) ∧ (𝑄 / 2) < (𝑁 + 1)) → 𝑦 < (𝑁 + 1))) |
272 | 267, 271 | mpan2d 710 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 / 2) → 𝑦 < (𝑁 + 1))) |
273 | 245, 272 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 < (𝑁 + 1))) |
274 | | nnleltp1 11432 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑦 ≤ 𝑁 ↔ 𝑦 < (𝑁 + 1))) |
275 | 134, 263,
274 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ 𝑁 ↔ 𝑦 < (𝑁 + 1))) |
276 | 273, 275 | sylibrd 249 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 ≤ 𝑁)) |
277 | 276 | pm4.71rd 667 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))))) |
278 | 96, 71 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) |
279 | | flge 12606 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑦 ∈ ℤ) → (𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
280 | 278, 202,
279 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
281 | 224, 277,
280 | 3bitr3d 298 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
282 | 281 | pm5.32da 673 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
283 | 133, 282 | syl5bb 272 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
284 | 283 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
285 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑥 = (2 · 𝑢)) |
286 | | nnuz 11723 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ℕ =
(ℤ≥‘1) |
287 | 119, 286 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 ·
𝑢) ∈
(ℤ≥‘1)) |
288 | 26 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑀 ∈
ℤ) |
289 | | elfz5 12334 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((2
· 𝑢) ∈
(ℤ≥‘1) ∧ 𝑀 ∈ ℤ) → ((2 · 𝑢) ∈ (1...𝑀) ↔ (2 · 𝑢) ≤ 𝑀)) |
290 | 287, 288,
289 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 ·
𝑢) ∈ (1...𝑀) ↔ (2 · 𝑢) ≤ 𝑀)) |
291 | 166, 290 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 ·
𝑢) ∈ (1...𝑀)) |
292 | 291 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (2 · 𝑢) ∈ (1...𝑀)) |
293 | 285, 292 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑥 ∈ (1...𝑀)) |
294 | 293 | biantrurd 529 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...𝑁) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)))) |
295 | 262 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℤ) |
296 | 295 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑁 ∈ ℤ) |
297 | | fznn 12408 |
. . . . . . . . . . . . . . . . . . 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 6657 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (2 · 𝑢) → (𝑥 · 𝑄) = ((2 · 𝑢) · 𝑄)) |
301 | 119 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 ·
𝑢) ∈
ℂ) |
302 | 138 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑄 ∈
ℂ) |
303 | 301, 302 | mulcomd 10061 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 ·
𝑢) · 𝑄) = (𝑄 · (2 · 𝑢))) |
304 | 300, 303 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑥 · 𝑄) = (𝑄 · (2 · 𝑢))) |
305 | 304 | breq2d 4665 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → ((𝑦 · 𝑃) < (𝑥 · 𝑄) ↔ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))) |
306 | 299, 305 | anbi12d 747 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ ((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))))) |
307 | 278 | flcld 12599 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℤ) |
308 | | fznn 12408 |
. . . . . . . . . . . . . . . . . 18
⊢
((⌊‘((𝑄
/ 𝑃) · (2 ·
𝑢))) ∈ ℤ →
(𝑦 ∈
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
309 | 307, 308 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑦 ∈
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
310 | 309 | adantr 481 |
. . . . . . . . . . . . . . . 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 673 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑥 = (2 · 𝑢) ∧ 〈𝑥, 𝑦〉 ∈ 𝑆) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
314 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑥 ∈ V |
315 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑦 ∈ V |
316 | 314, 315 | op1std 7178 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) |
317 | 316 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((2 · 𝑢) = (1st ‘𝑧) ↔ (2 · 𝑢) = 𝑥)) |
318 | | eqcom 2629 |
. . . . . . . . . . . . . . . 16
⊢ ((2
· 𝑢) = 𝑥 ↔ 𝑥 = (2 · 𝑢)) |
319 | 317, 318 | syl6bb 276 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((2 · 𝑢) = (1st ‘𝑧) ↔ 𝑥 = (2 · 𝑢))) |
320 | 319 | elrab 3363 |
. . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑦〉 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ↔ (〈𝑥, 𝑦〉 ∈ 𝑆 ∧ 𝑥 = (2 · 𝑢))) |
321 | | ancom 466 |
. . . . . . . . . . . . . 14
⊢
((〈𝑥, 𝑦〉 ∈ 𝑆 ∧ 𝑥 = (2 · 𝑢)) ↔ (𝑥 = (2 · 𝑢) ∧ 〈𝑥, 𝑦〉 ∈ 𝑆)) |
322 | 320, 321 | bitri 264 |
. . . . . . . . . . . . 13
⊢
(〈𝑥, 𝑦〉 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ↔ (𝑥 = (2 · 𝑢) ∧ 〈𝑥, 𝑦〉 ∈ 𝑆)) |
323 | | opelxp 5146 |
. . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑦〉 ∈ ({(2 ·
𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) ↔ (𝑥 ∈ {(2 · 𝑢)} ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
324 | | velsn 4193 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ {(2 · 𝑢)} ↔ 𝑥 = (2 · 𝑢)) |
325 | 324 | anbi1i 731 |
. . . . . . . . . . . . . 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 5216 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} = ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
329 | 328 | eqcomd 2628 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 ·
𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))))) = {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}) |
330 | 329 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (#‘({(2
· 𝑢)} ×
(1...(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))))) = (#‘{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) |
331 | | hashfz1 13134 |
. . . . . . . . . 10
⊢
((⌊‘((𝑄
/ 𝑃) · (2 ·
𝑢))) ∈
ℕ0 → (#‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) |
332 | 97, 331 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(#‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) |
333 | 124, 330,
332 | 3eqtr3rd 2665 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (#‘{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) |
334 | 333 | sumeq2dv 14433 |
. . . . . . 7
⊢ (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(#‘{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) |
335 | 107 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑆 ∈ Fin) |
336 | | ssfi 8180 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Fin ∧ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ⊆ 𝑆) → {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ∈ Fin) |
337 | 335, 125,
336 | sylancl 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ∈ Fin) |
338 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑣 → (1st ‘𝑧) = (1st ‘𝑣)) |
339 | 338 | eqeq2d 2632 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑣 → ((2 · 𝑢) = (1st ‘𝑧) ↔ (2 · 𝑢) = (1st ‘𝑣))) |
340 | 339 | elrab 3363 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ↔ (𝑣 ∈ 𝑆 ∧ (2 · 𝑢) = (1st ‘𝑣))) |
341 | 340 | simprbi 480 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} → (2 · 𝑢) = (1st ‘𝑣)) |
342 | 341 | ad2antll 765 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → (2 · 𝑢) = (1st ‘𝑣)) |
343 | 342 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → ((2 · 𝑢) / 2) = ((1st ‘𝑣) / 2)) |
344 | 158 | nncnd 11036 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈
ℂ) |
345 | 344 | adantrr 753 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → 𝑢 ∈ ℂ) |
346 | | 2cnd 11093 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → 2 ∈
ℂ) |
347 | 231 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → 2 ≠ 0) |
348 | 345, 346,
347 | divcan3d 10806 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → ((2 · 𝑢) / 2) = 𝑢) |
349 | 343, 348 | eqtr3d 2658 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → ((1st ‘𝑣) / 2) = 𝑢) |
350 | 349 | ralrimivva 2971 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑢 ∈ (1...(⌊‘(𝑀 / 2)))∀𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ((1st ‘𝑣) / 2) = 𝑢) |
351 | | invdisj 4638 |
. . . . . . . . 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 14554 |
. . . . . . 7
⊢ (𝜑 → (#‘∪ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}) = Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(#‘{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) |
354 | | iunrab 4567 |
. . . . . . . . 9
⊢ ∪ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} = {𝑧 ∈ 𝑆 ∣ ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧)} |
355 | | 2cn 11091 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
356 | | zcn 11382 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ℤ → 𝑢 ∈
ℂ) |
357 | 356 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ ℤ) → 𝑢 ∈ ℂ) |
358 | | mulcom 10022 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℂ ∧ 𝑢
∈ ℂ) → (2 · 𝑢) = (𝑢 · 2)) |
359 | 355, 357,
358 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ ℤ) → (2 · 𝑢) = (𝑢 · 2)) |
360 | 359 | eqeq1d 2624 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ ℤ) → ((2 · 𝑢) = (1st ‘𝑧) ↔ (𝑢 · 2) = (1st ‘𝑧))) |
361 | 360 | rexbidva 3049 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ ℤ (2 · 𝑢) = (1st ‘𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st
‘𝑧))) |
362 | 152 | anim1i 592 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈
(1...(⌊‘(𝑀 /
2))) ∧ (2 · 𝑢) =
(1st ‘𝑧))
→ (𝑢 ∈ ℤ
∧ (2 · 𝑢) =
(1st ‘𝑧))) |
363 | 362 | reximi2 3010 |
. . . . . . . . . . . 12
⊢
(∃𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(2 · 𝑢) =
(1st ‘𝑧)
→ ∃𝑢 ∈
ℤ (2 · 𝑢) =
(1st ‘𝑧)) |
364 | | simprr 796 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (2 · 𝑢) = (1st ‘𝑧)) |
365 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆) |
366 | 105, 365 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ ((1...𝑀) × (1...𝑁))) |
367 | | xp1st 7198 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ ((1...𝑀) × (1...𝑁)) → (1st ‘𝑧) ∈ (1...𝑀)) |
368 | 366, 367 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (1st ‘𝑧) ∈ (1...𝑀)) |
369 | 368 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (1st
‘𝑧) ∈ (1...𝑀)) |
370 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑧) ∈ (1...𝑀) → (1st ‘𝑧) ≤ 𝑀) |
371 | 369, 370 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (1st
‘𝑧) ≤ 𝑀) |
372 | 364, 371 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (2 · 𝑢) ≤ 𝑀) |
373 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ ℤ → 𝑢 ∈
ℝ) |
374 | 373 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈ ℝ) |
375 | 11 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 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 1330 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → ((2 · 𝑢) ≤ 𝑀 ↔ 𝑢 ≤ (𝑀 / 2))) |
379 | 372, 378 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ≤ (𝑀 / 2)) |
380 | 12 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (𝑀 / 2) ∈ ℝ) |
381 | | simprl 794 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈ ℤ) |
382 | 380, 381,
154 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2)))) |
383 | 379, 382 | mpbid 222 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ≤ (⌊‘(𝑀 / 2))) |
384 | | 2t0e0 11183 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
· 0) = 0 |
385 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((1st ‘𝑧) ∈ (1...𝑀) → (1st ‘𝑧) ∈
ℕ) |
386 | 369, 385 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (1st
‘𝑧) ∈
ℕ) |
387 | 364, 386 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (2 · 𝑢) ∈
ℕ) |
388 | 387 | nngt0d 11064 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 0 < (2 ·
𝑢)) |
389 | 384, 388 | syl5eqbr 4688 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (2 · 0) <
(2 · 𝑢)) |
390 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 0 ∈
ℝ) |
391 | | ltmul2 10874 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0
∈ ℝ ∧ 𝑢
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (0 < 𝑢 ↔ (2 · 0) < (2
· 𝑢))) |
392 | 390, 374,
376, 377, 391 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (0 < 𝑢 ↔ (2 · 0) < (2
· 𝑢))) |
393 | 389, 392 | mpbird 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 0 < 𝑢) |
394 | | elnnz 11387 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ ℕ ↔ (𝑢 ∈ ℤ ∧ 0 <
𝑢)) |
395 | 381, 393,
394 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈ ℕ) |
396 | 395, 286 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈
(ℤ≥‘1)) |
397 | 13 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (⌊‘(𝑀 / 2)) ∈
ℤ) |
398 | | elfz5 12334 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈
(ℤ≥‘1) ∧ (⌊‘(𝑀 / 2)) ∈ ℤ) → (𝑢 ∈
(1...(⌊‘(𝑀 /
2))) ↔ 𝑢 ≤
(⌊‘(𝑀 /
2)))) |
399 | 396, 397,
398 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2)))) |
400 | 383, 399 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) |
401 | 400, 364 | jca 554 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st ‘𝑧))) |
402 | 401 | ex 450 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧)) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st ‘𝑧)))) |
403 | 402 | reximdv2 3014 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ ℤ (2 · 𝑢) = (1st ‘𝑧) → ∃𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(2 · 𝑢) =
(1st ‘𝑧))) |
404 | 363, 403 | impbid2 216 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧) ↔ ∃𝑢 ∈ ℤ (2 ·
𝑢) = (1st
‘𝑧))) |
405 | | 2z 11409 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℤ |
406 | | elfzelz 12342 |
. . . . . . . . . . . . 13
⊢
((1st ‘𝑧) ∈ (1...𝑀) → (1st ‘𝑧) ∈
ℤ) |
407 | 368, 406 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (1st ‘𝑧) ∈
ℤ) |
408 | | divides 14985 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℤ ∧ (1st ‘𝑧) ∈ ℤ) → (2 ∥
(1st ‘𝑧)
↔ ∃𝑢 ∈
ℤ (𝑢 · 2) =
(1st ‘𝑧))) |
409 | 405, 407,
408 | sylancr 695 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (2 ∥ (1st
‘𝑧) ↔
∃𝑢 ∈ ℤ
(𝑢 · 2) =
(1st ‘𝑧))) |
410 | 361, 404,
409 | 3bitr4d 300 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧) ↔ 2 ∥
(1st ‘𝑧))) |
411 | 410 | rabbidva 3188 |
. . . . . . . . 9
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧)} = {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)}) |
412 | 354, 411 | syl5eq 2668 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} = {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)}) |
413 | 412 | fveq2d 6195 |
. . . . . . 7
⊢ (𝜑 → (#‘∪ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}) = (#‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)})) |
414 | 334, 353,
413 | 3eqtr2d 2662 |
. . . . . 6
⊢ (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (#‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)})) |
415 | 414 | oveq2d 6666 |
. . . . 5
⊢ (𝜑 → (-1↑Σ𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) =
(-1↑(#‘{𝑧 ∈
𝑆 ∣ 2 ∥
(1st ‘𝑧)}))) |
416 | 1, 2, 3, 5, 250, 103 | lgsquadlem1 25105 |
. . . . 5
⊢ (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) |
417 | 415, 416 | oveq12d 6668 |
. . . 4
⊢ (𝜑 → ((-1↑Σ𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢)))) ·
(-1↑Σ𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = ((-1↑(#‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)})) ·
(-1↑(#‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)})))) |
418 | 118, 417 | eqtr4d 2659 |
. . 3
⊢ (𝜑 → (-1↑((#‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)}) +
(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)}))) = ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
419 | | unrab 3898 |
. . . . . . 7
⊢ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) = {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∨ ¬ 2
∥ (1st ‘𝑧))} |
420 | | exmid 431 |
. . . . . . . . 9
⊢ (2
∥ (1st ‘𝑧) ∨ ¬ 2 ∥ (1st
‘𝑧)) |
421 | 420 | rgenw 2924 |
. . . . . . . 8
⊢
∀𝑧 ∈
𝑆 (2 ∥
(1st ‘𝑧)
∨ ¬ 2 ∥ (1st ‘𝑧)) |
422 | | rabid2 3118 |
. . . . . . . 8
⊢ (𝑆 = {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∨ ¬ 2
∥ (1st ‘𝑧))} ↔ ∀𝑧 ∈ 𝑆 (2 ∥ (1st ‘𝑧) ∨ ¬ 2 ∥
(1st ‘𝑧))) |
423 | 421, 422 | mpbir 221 |
. . . . . . 7
⊢ 𝑆 = {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∨ ¬ 2
∥ (1st ‘𝑧))} |
424 | 419, 423 | eqtr4i 2647 |
. . . . . 6
⊢ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) = 𝑆 |
425 | 424 | fveq2i 6194 |
. . . . 5
⊢
(#‘({𝑧 ∈
𝑆 ∣ 2 ∥
(1st ‘𝑧)}
∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)})) = (#‘𝑆) |
426 | | inrab 3899 |
. . . . . . 7
⊢ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∩ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) = {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∧ ¬ 2
∥ (1st ‘𝑧))} |
427 | | pm3.24 926 |
. . . . . . . . . 10
⊢ ¬ (2
∥ (1st ‘𝑧) ∧ ¬ 2 ∥ (1st
‘𝑧)) |
428 | 427 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ¬ (2 ∥
(1st ‘𝑧)
∧ ¬ 2 ∥ (1st ‘𝑧))) |
429 | 428 | ralrimivw 2967 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 ¬ (2 ∥ (1st
‘𝑧) ∧ ¬ 2
∥ (1st ‘𝑧))) |
430 | | rabeq0 3957 |
. . . . . . . 8
⊢ ({𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∧ ¬ 2
∥ (1st ‘𝑧))} = ∅ ↔ ∀𝑧 ∈ 𝑆 ¬ (2 ∥ (1st
‘𝑧) ∧ ¬ 2
∥ (1st ‘𝑧))) |
431 | 429, 430 | sylibr 224 |
. . . . . . 7
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st
‘𝑧) ∧ ¬ 2
∥ (1st ‘𝑧))} = ∅) |
432 | 426, 431 | syl5eq 2668 |
. . . . . 6
⊢ (𝜑 → ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∩ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) =
∅) |
433 | | hashun 13171 |
. . . . . 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 1326 |
. . . . 5
⊢ (𝜑 → (#‘({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)} ∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) =
((#‘{𝑧 ∈ 𝑆 ∣ 2 ∥
(1st ‘𝑧)})
+ (#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)}))) |
435 | 425, 434 | syl5reqr 2671 |
. . . 4
⊢ (𝜑 → ((#‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)}) +
(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)})) = (#‘𝑆)) |
436 | 435 | oveq2d 6666 |
. . 3
⊢ (𝜑 → (-1↑((#‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st
‘𝑧)}) +
(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)}))) = (-1↑(#‘𝑆))) |
437 | 99, 418, 436 | 3eqtr2d 2662 |
. 2
⊢ (𝜑 → (-1↑(Σ𝑢 ∈
(1...(⌊‘(𝑀 /
2)))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (-1↑(#‘𝑆))) |
438 | 4, 84, 437 | 3eqtrd 2660 |
1
⊢ (𝜑 → (𝑄 /L 𝑃) = (-1↑(#‘𝑆))) |