| Step | Hyp | Ref
| Expression |
| 1 | | neg1cn 12380 |
. . . 4
⊢ -1 ∈
ℂ |
| 2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → -1 ∈
ℂ) |
| 3 | | neg1ne0 12382 |
. . . 4
⊢ -1 ≠
0 |
| 4 | 3 | a1i 11 |
. . 3
⊢ (𝜑 → -1 ≠
0) |
| 5 | | fzfid 14014 |
. . . 4
⊢ (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin) |
| 6 | | lgseisen.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄 ∈ (ℙ ∖
{2})) |
| 7 | 6 | gausslemma2dlem0a 27400 |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 ∈ ℕ) |
| 8 | 7 | nnred 12281 |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ ℝ) |
| 9 | | lgseisen.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
| 10 | 9 | gausslemma2dlem0a 27400 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℕ) |
| 11 | 8, 10 | nndivred 12320 |
. . . . . . 7
⊢ (𝜑 → (𝑄 / 𝑃) ∈ ℝ) |
| 12 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℝ) |
| 13 | | 2z 12649 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
| 14 | | elfzelz 13564 |
. . . . . . . . 9
⊢ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → 𝑢 ∈ ℤ) |
| 15 | 14 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℤ) |
| 16 | | zmulcl 12666 |
. . . . . . . 8
⊢ ((2
∈ ℤ ∧ 𝑢
∈ ℤ) → (2 · 𝑢) ∈ ℤ) |
| 17 | 13, 15, 16 | sylancr 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℤ) |
| 18 | 17 | zred 12722 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℝ) |
| 19 | 12, 18 | remulcld 11291 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) |
| 20 | 19 | flcld 13838 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ) |
| 21 | 5, 20 | fsumzcl 15771 |
. . 3
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ) |
| 22 | 2, 4, 21 | expclzd 14191 |
. 2
⊢ (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℂ) |
| 23 | | fzfid 14014 |
. . . . . . 7
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
| 24 | | fzfid 14014 |
. . . . . . 7
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
| 25 | | xpfi 9358 |
. . . . . . 7
⊢
(((1...𝑀) ∈ Fin
∧ (1...𝑁) ∈ Fin)
→ ((1...𝑀) ×
(1...𝑁)) ∈
Fin) |
| 26 | 23, 24, 25 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((1...𝑀) × (1...𝑁)) ∈ Fin) |
| 27 | | lgsquad.6 |
. . . . . . 7
⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} |
| 28 | | opabssxp 5778 |
. . . . . . 7
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁)) |
| 29 | 27, 28 | eqsstri 4030 |
. . . . . 6
⊢ 𝑆 ⊆ ((1...𝑀) × (1...𝑁)) |
| 30 | | ssfi 9213 |
. . . . . 6
⊢
((((1...𝑀) ×
(1...𝑁)) ∈ Fin ∧
𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin) |
| 31 | 26, 29, 30 | sylancl 586 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ Fin) |
| 32 | | ssrab2 4080 |
. . . . 5
⊢ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ⊆ 𝑆 |
| 33 | | ssfi 9213 |
. . . . 5
⊢ ((𝑆 ∈ Fin ∧ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ⊆ 𝑆) → {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
| 34 | 31, 32, 33 | sylancl 586 |
. . . 4
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
| 35 | | hashcl 14395 |
. . . 4
⊢ ({𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈ Fin
→ (♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)}) ∈
ℕ0) |
| 36 | 34, 35 | syl 17 |
. . 3
⊢ (𝜑 → (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) ∈
ℕ0) |
| 37 | | expcl 14120 |
. . 3
⊢ ((-1
∈ ℂ ∧ (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) ∈
ℕ0) → (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) ∈
ℂ) |
| 38 | 1, 36, 37 | sylancr 587 |
. 2
⊢ (𝜑 →
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) ∈ ℂ) |
| 39 | 36 | nn0zd 12639 |
. . 3
⊢ (𝜑 → (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) ∈
ℤ) |
| 40 | 2, 4, 39 | expne0d 14192 |
. 2
⊢ (𝜑 →
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) ≠ 0) |
| 41 | 38, 40 | recidd 12038 |
. . . 4
⊢ (𝜑 →
((-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) · (1 /
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})))) = 1) |
| 42 | | 1div1e1 11958 |
. . . . . . . . 9
⊢ (1 / 1) =
1 |
| 43 | 42 | negeqi 11501 |
. . . . . . . 8
⊢ -(1 / 1)
= -1 |
| 44 | | ax-1cn 11213 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
| 45 | | ax-1ne0 11224 |
. . . . . . . . 9
⊢ 1 ≠
0 |
| 46 | | divneg2 11991 |
. . . . . . . . 9
⊢ ((1
∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → -(1 / 1) = (1 /
-1)) |
| 47 | 44, 44, 45, 46 | mp3an 1463 |
. . . . . . . 8
⊢ -(1 / 1)
= (1 / -1) |
| 48 | 43, 47 | eqtr3i 2767 |
. . . . . . 7
⊢ -1 = (1 /
-1) |
| 49 | 48 | oveq1i 7441 |
. . . . . 6
⊢
(-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) = ((1 /
-1)↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) |
| 50 | 2, 4, 39 | exprecd 14194 |
. . . . . 6
⊢ (𝜑 → ((1 /
-1)↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) = (1 / (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})))) |
| 51 | 49, 50 | eqtrid 2789 |
. . . . 5
⊢ (𝜑 →
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) = (1 / (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})))) |
| 52 | 51 | oveq2d 7447 |
. . . 4
⊢ (𝜑 →
((-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) =
((-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) · (1 /
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)}))))) |
| 53 | 31 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑆 ∈ Fin) |
| 54 | | ssrab2 4080 |
. . . . . . . . . . . 12
⊢ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆 |
| 55 | | ssfi 9213 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Fin ∧ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆) → {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ∈ Fin) |
| 56 | 53, 54, 55 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ∈ Fin) |
| 57 | | fveqeq2 6915 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑣 → ((1st ‘𝑧) = (𝑃 − (2 · 𝑢)) ↔ (1st ‘𝑣) = (𝑃 − (2 · 𝑢)))) |
| 58 | 57 | elrab 3692 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ↔ (𝑣 ∈ 𝑆 ∧ (1st ‘𝑣) = (𝑃 − (2 · 𝑢)))) |
| 59 | 58 | simprbi 496 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} → (1st ‘𝑣) = (𝑃 − (2 · 𝑢))) |
| 60 | 59 | ad2antll 729 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (1st ‘𝑣) = (𝑃 − (2 · 𝑢))) |
| 61 | 60 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (1st ‘𝑣)) = (𝑃 − (𝑃 − (2 · 𝑢)))) |
| 62 | 10 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℕ) |
| 63 | 62 | nncnd 12282 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℂ) |
| 64 | 63 | adantrr 717 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → 𝑃 ∈ ℂ) |
| 65 | 17 | zcnd 12723 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℂ) |
| 66 | 65 | adantrr 717 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (2 · 𝑢) ∈ ℂ) |
| 67 | 64, 66 | nncand 11625 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (𝑃 − (2 · 𝑢))) = (2 · 𝑢)) |
| 68 | 61, 67 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (1st ‘𝑣)) = (2 · 𝑢)) |
| 69 | 68 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → ((𝑃 − (1st ‘𝑣)) / 2) = ((2 · 𝑢) / 2)) |
| 70 | 15 | zcnd 12723 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℂ) |
| 71 | 70 | adantrr 717 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → 𝑢 ∈ ℂ) |
| 72 | | 2cnd 12344 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → 2 ∈
ℂ) |
| 73 | | 2ne0 12370 |
. . . . . . . . . . . . . . . 16
⊢ 2 ≠
0 |
| 74 | 73 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → 2 ≠ 0) |
| 75 | 71, 72, 74 | divcan3d 12048 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → ((2 · 𝑢) / 2) = 𝑢) |
| 76 | 69, 75 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → ((𝑃 − (1st ‘𝑣)) / 2) = 𝑢) |
| 77 | 76 | ralrimivva 3202 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)∀𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ((𝑃 − (1st ‘𝑣)) / 2) = 𝑢) |
| 78 | | invdisj 5129 |
. . . . . . . . . . . 12
⊢
(∀𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)∀𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ((𝑃 − (1st ‘𝑣)) / 2) = 𝑢 → Disj 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))}) |
| 79 | 77, 78 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → Disj 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))}) |
| 80 | 5, 56, 79 | hashiun 15858 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘∪ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(♯‘{𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) |
| 81 | | iunrab 5052 |
. . . . . . . . . . . 12
⊢ ∪ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧 ∈ 𝑆 ∣ ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st ‘𝑧) = (𝑃 − (2 · 𝑢))} |
| 82 | | eldifsni 4790 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ≠
2) |
| 83 | 9, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑃 ≠ 2) |
| 84 | 83 | necomd 2996 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 2 ≠ 𝑃) |
| 85 | 84 | neneqd 2945 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ¬ 2 = 𝑃) |
| 86 | 85 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 = 𝑃) |
| 87 | | uzid 12893 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
| 88 | 13, 87 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
(ℤ≥‘2) |
| 89 | 9 | eldifad 3963 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑃 ∈ ℙ) |
| 90 | 89 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℙ) |
| 91 | | dvdsprm 16740 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (2 ∥ 𝑃 ↔ 2 = 𝑃)) |
| 92 | 88, 90, 91 | sylancr 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ 𝑃 ↔ 2 = 𝑃)) |
| 93 | 86, 92 | mtbird 325 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ 𝑃) |
| 94 | 10 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℕ) |
| 95 | 94 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℂ) |
| 96 | 17 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℤ) |
| 97 | 96 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℂ) |
| 98 | 95, 97 | npcand 11624 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)) = 𝑃) |
| 99 | 98 | breq2d 5155 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)) ↔ 2 ∥ 𝑃)) |
| 100 | 93, 99 | mtbird 325 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))) |
| 101 | 14 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℤ) |
| 102 | | dvdsmul1 16315 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℤ ∧ 𝑢
∈ ℤ) → 2 ∥ (2 · 𝑢)) |
| 103 | 13, 101, 102 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∥ (2 · 𝑢)) |
| 104 | 13 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℤ) |
| 105 | 94 | nnzd 12640 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ) |
| 106 | 105, 96 | zsubcld 12727 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ) |
| 107 | | dvds2add 16327 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℤ ∧ (𝑃
− (2 · 𝑢))
∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → ((2 ∥ (𝑃 − (2 · 𝑢)) ∧ 2 ∥ (2 ·
𝑢)) → 2 ∥
((𝑃 − (2 ·
𝑢)) + (2 · 𝑢)))) |
| 108 | 104, 106,
96, 107 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 ∥ (𝑃 − (2 · 𝑢)) ∧ 2 ∥ (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)))) |
| 109 | 103, 108 | mpan2d 694 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ (𝑃 − (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)))) |
| 110 | 100, 109 | mtod 198 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ (𝑃 − (2 · 𝑢))) |
| 111 | | breq2 5147 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑧) = (𝑃 − (2 · 𝑢)) → (2 ∥ (1st
‘𝑧) ↔ 2 ∥
(𝑃 − (2 ·
𝑢)))) |
| 112 | 111 | notbid 318 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑧) = (𝑃 − (2 · 𝑢)) → (¬ 2 ∥ (1st
‘𝑧) ↔ ¬ 2
∥ (𝑃 − (2
· 𝑢)))) |
| 113 | 110, 112 | syl5ibrcom 247 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((1st ‘𝑧) = (𝑃 − (2 · 𝑢)) → ¬ 2 ∥ (1st
‘𝑧))) |
| 114 | 113 | rexlimdva 3155 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st ‘𝑧) = (𝑃 − (2 · 𝑢)) → ¬ 2 ∥ (1st
‘𝑧))) |
| 115 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆) |
| 116 | 29, 115 | sselid 3981 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ ((1...𝑀) × (1...𝑁))) |
| 117 | | xp1st 8046 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ((1...𝑀) × (1...𝑁)) → (1st ‘𝑧) ∈ (1...𝑀)) |
| 118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (1st ‘𝑧) ∈ (1...𝑀)) |
| 119 | | elfzelz 13564 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑧) ∈ (1...𝑀) → (1st ‘𝑧) ∈
ℤ) |
| 120 | | odd2np1 16378 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑧) ∈ ℤ → (¬ 2 ∥
(1st ‘𝑧)
↔ ∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = (1st ‘𝑧))) |
| 121 | 118, 119,
120 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ 2 ∥ (1st
‘𝑧) ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) =
(1st ‘𝑧))) |
| 122 | | lgsquad.4 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑀 = ((𝑃 − 1) / 2) |
| 123 | 9, 122 | gausslemma2dlem0b 27401 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 124 | 123 | nnred 12281 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 125 | 124 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑀 ∈
ℝ) |
| 126 | 125 | rehalfcld 12513 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 / 2) ∈
ℝ) |
| 127 | 126 | flcld 13838 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
(⌊‘(𝑀 / 2))
∈ ℤ) |
| 128 | 127 | peano2zd 12725 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
((⌊‘(𝑀 / 2)) +
1) ∈ ℤ) |
| 129 | 123 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑀 ∈
ℕ) |
| 130 | 129 | nnzd 12640 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑀 ∈
ℤ) |
| 131 | | simprl 771 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑛 ∈
ℤ) |
| 132 | 130, 131 | zsubcld 12727 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 − 𝑛) ∈ ℤ) |
| 133 | | reflcl 13836 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 / 2) ∈ ℝ →
(⌊‘(𝑀 / 2))
∈ ℝ) |
| 134 | 126, 133 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
(⌊‘(𝑀 / 2))
∈ ℝ) |
| 135 | 132 | zred 12722 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 − 𝑛) ∈ ℝ) |
| 136 | | flle 13839 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 / 2) ∈ ℝ →
(⌊‘(𝑀 / 2))
≤ (𝑀 /
2)) |
| 137 | 126, 136 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
(⌊‘(𝑀 / 2))
≤ (𝑀 /
2)) |
| 138 | | zre 12617 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℝ) |
| 139 | 138 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑛 ∈
ℝ) |
| 140 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑛) + 1) =
(1st ‘𝑧)) |
| 141 | 118 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
(1st ‘𝑧)
∈ (1...𝑀)) |
| 142 | 140, 141 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑛) + 1) ∈
(1...𝑀)) |
| 143 | | elfzle2 13568 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((2
· 𝑛) + 1) ∈
(1...𝑀) → ((2 ·
𝑛) + 1) ≤ 𝑀) |
| 144 | 142, 143 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑛) + 1) ≤ 𝑀) |
| 145 | | zmulcl 12666 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((2
∈ ℤ ∧ 𝑛
∈ ℤ) → (2 · 𝑛) ∈ ℤ) |
| 146 | 13, 131, 145 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· 𝑛) ∈
ℤ) |
| 147 | | zltp1le 12667 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((2
· 𝑛) ∈ ℤ
∧ 𝑀 ∈ ℤ)
→ ((2 · 𝑛) <
𝑀 ↔ ((2 · 𝑛) + 1) ≤ 𝑀)) |
| 148 | 146, 130,
147 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑛) < 𝑀 ↔ ((2 · 𝑛) + 1) ≤ 𝑀)) |
| 149 | 144, 148 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· 𝑛) < 𝑀) |
| 150 | | 2re 12340 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ∈
ℝ |
| 151 | 150 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 2 ∈
ℝ) |
| 152 | | 2pos 12369 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 <
2 |
| 153 | 152 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 0 <
2) |
| 154 | | ltmuldiv2 12142 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → ((2 · 𝑛) < 𝑀 ↔ 𝑛 < (𝑀 / 2))) |
| 155 | 139, 125,
151, 153, 154 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑛) < 𝑀 ↔ 𝑛 < (𝑀 / 2))) |
| 156 | 149, 155 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑛 < (𝑀 / 2)) |
| 157 | 126 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 / 2) ∈
ℂ) |
| 158 | 123 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑀 ∈ ℂ) |
| 159 | 158 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑀 ∈
ℂ) |
| 160 | 159 | 2halvesd 12512 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((𝑀 / 2) + (𝑀 / 2)) = 𝑀) |
| 161 | 157, 157,
160 | mvlraddd 11673 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 / 2) = (𝑀 − (𝑀 / 2))) |
| 162 | 156, 161 | breqtrd 5169 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑛 < (𝑀 − (𝑀 / 2))) |
| 163 | 139, 125,
126, 162 | ltsub13d 11869 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 / 2) < (𝑀 − 𝑛)) |
| 164 | 134, 126,
135, 137, 163 | lelttrd 11419 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
(⌊‘(𝑀 / 2))
< (𝑀 − 𝑛)) |
| 165 | | zltp1le 12667 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((⌊‘(𝑀
/ 2)) ∈ ℤ ∧ (𝑀 − 𝑛) ∈ ℤ) →
((⌊‘(𝑀 / 2))
< (𝑀 − 𝑛) ↔ ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀 − 𝑛))) |
| 166 | 127, 132,
165 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
((⌊‘(𝑀 / 2))
< (𝑀 − 𝑛) ↔ ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀 − 𝑛))) |
| 167 | 164, 166 | mpbid 232 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
((⌊‘(𝑀 / 2)) +
1) ≤ (𝑀 − 𝑛)) |
| 168 | | 2t0e0 12435 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
· 0) = 0 |
| 169 | | 2cn 12341 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ∈
ℂ |
| 170 | | zcn 12618 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
| 171 | 170 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑛 ∈
ℂ) |
| 172 | | mulcl 11239 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((2
∈ ℂ ∧ 𝑛
∈ ℂ) → (2 · 𝑛) ∈ ℂ) |
| 173 | 169, 171,
172 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· 𝑛) ∈
ℂ) |
| 174 | | pncan 11514 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((2
· 𝑛) ∈ ℂ
∧ 1 ∈ ℂ) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛)) |
| 175 | 173, 44, 174 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (((2
· 𝑛) + 1) − 1)
= (2 · 𝑛)) |
| 176 | | elfznn 13593 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((2
· 𝑛) + 1) ∈
(1...𝑀) → ((2 ·
𝑛) + 1) ∈
ℕ) |
| 177 | | nnm1nn0 12567 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((2
· 𝑛) + 1) ∈
ℕ → (((2 · 𝑛) + 1) − 1) ∈
ℕ0) |
| 178 | 142, 176,
177 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (((2
· 𝑛) + 1) − 1)
∈ ℕ0) |
| 179 | 175, 178 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· 𝑛) ∈
ℕ0) |
| 180 | 179 | nn0ge0d 12590 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 0 ≤
(2 · 𝑛)) |
| 181 | 168, 180 | eqbrtrid 5178 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· 0) ≤ (2 · 𝑛)) |
| 182 | | 0red 11264 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 0 ∈
ℝ) |
| 183 | | lemul2 12120 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0
∈ ℝ ∧ 𝑛
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (0 ≤ 𝑛 ↔ (2 · 0) ≤ (2
· 𝑛))) |
| 184 | 182, 139,
151, 153, 183 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (0 ≤
𝑛 ↔ (2 · 0)
≤ (2 · 𝑛))) |
| 185 | 181, 184 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 0 ≤
𝑛) |
| 186 | 125, 139 | subge02d 11855 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (0 ≤
𝑛 ↔ (𝑀 − 𝑛) ≤ 𝑀)) |
| 187 | 185, 186 | mpbid 232 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 − 𝑛) ≤ 𝑀) |
| 188 | 128, 130,
132, 167, 187 | elfzd 13555 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 − 𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) |
| 189 | 89 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑃 ∈
ℙ) |
| 190 | | prmnn 16711 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 191 | 189, 190 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑃 ∈
ℕ) |
| 192 | 191 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑃 ∈
ℂ) |
| 193 | | peano2cn 11433 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
· 𝑛) ∈ ℂ
→ ((2 · 𝑛) + 1)
∈ ℂ) |
| 194 | 173, 193 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑛) + 1) ∈
ℂ) |
| 195 | 192, 194 | nncand 11625 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑃 − (𝑃 − ((2 · 𝑛) + 1))) = ((2 · 𝑛) + 1)) |
| 196 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 1 ∈
ℂ) |
| 197 | 192, 173,
196 | sub32d 11652 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((𝑃 − (2 · 𝑛)) − 1) = ((𝑃 − 1) − (2 ·
𝑛))) |
| 198 | 192, 173,
196 | subsub4d 11651 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((𝑃 − (2 · 𝑛)) − 1) = (𝑃 − ((2 · 𝑛) + 1))) |
| 199 | | 2cnd 12344 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 2 ∈
ℂ) |
| 200 | 199, 159,
171 | subdid 11719 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· (𝑀 − 𝑛)) = ((2 · 𝑀) − (2 · 𝑛))) |
| 201 | 122 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2
· 𝑀) = (2 ·
((𝑃 − 1) /
2)) |
| 202 | 10 | nnzd 12640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝑃 ∈ ℤ) |
| 203 | 202 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑃 ∈
ℤ) |
| 204 | | peano2zm 12660 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈
ℤ) |
| 205 | 203, 204 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑃 − 1) ∈
ℤ) |
| 206 | 205 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑃 − 1) ∈
ℂ) |
| 207 | 73 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 2 ≠
0) |
| 208 | 206, 199,
207 | divcan2d 12045 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· ((𝑃 − 1) /
2)) = (𝑃 −
1)) |
| 209 | 201, 208 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· 𝑀) = (𝑃 − 1)) |
| 210 | 209 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑀) − (2
· 𝑛)) = ((𝑃 − 1) − (2 ·
𝑛))) |
| 211 | 200, 210 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((𝑃 − 1) − (2 ·
𝑛)) = (2 · (𝑀 − 𝑛))) |
| 212 | 197, 198,
211 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑃 − ((2 · 𝑛) + 1)) = (2 · (𝑀 − 𝑛))) |
| 213 | 212 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑃 − (𝑃 − ((2 · 𝑛) + 1))) = (𝑃 − (2 · (𝑀 − 𝑛)))) |
| 214 | 195, 213,
140 | 3eqtr3rd 2786 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
(1st ‘𝑧) =
(𝑃 − (2 ·
(𝑀 − 𝑛)))) |
| 215 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = (𝑀 − 𝑛) → (2 · 𝑢) = (2 · (𝑀 − 𝑛))) |
| 216 | 215 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = (𝑀 − 𝑛) → (𝑃 − (2 · 𝑢)) = (𝑃 − (2 · (𝑀 − 𝑛)))) |
| 217 | 216 | rspceeqv 3645 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 − 𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ (1st ‘𝑧) = (𝑃 − (2 · (𝑀 − 𝑛)))) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st ‘𝑧) = (𝑃 − (2 · 𝑢))) |
| 218 | 188, 214,
217 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
∃𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(1st
‘𝑧) = (𝑃 − (2 · 𝑢))) |
| 219 | 218 | rexlimdvaa 3156 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (1st
‘𝑧) →
∃𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(1st
‘𝑧) = (𝑃 − (2 · 𝑢)))) |
| 220 | 121, 219 | sylbid 240 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ 2 ∥ (1st
‘𝑧) →
∃𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(1st
‘𝑧) = (𝑃 − (2 · 𝑢)))) |
| 221 | 114, 220 | impbid 212 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st ‘𝑧) = (𝑃 − (2 · 𝑢)) ↔ ¬ 2 ∥ (1st
‘𝑧))) |
| 222 | 221 | rabbidva 3443 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st ‘𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) |
| 223 | 81, 222 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) |
| 224 | 223 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘∪ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) |
| 225 | 27 | relopabiv 5830 |
. . . . . . . . . . . . . . 15
⊢ Rel 𝑆 |
| 226 | | relss 5791 |
. . . . . . . . . . . . . . 15
⊢ ({𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆 → (Rel 𝑆 → Rel {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) |
| 227 | 54, 225, 226 | mp2 9 |
. . . . . . . . . . . . . 14
⊢ Rel
{𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} |
| 228 | | relxp 5703 |
. . . . . . . . . . . . . 14
⊢ Rel
({(𝑃 − (2 ·
𝑢))} × (1...((2
· 𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 229 | 27 | eleq2i 2833 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑥, 𝑦〉 ∈ 𝑆 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}) |
| 230 | | opabidw 5529 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) |
| 231 | 229, 230 | bitri 275 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑥, 𝑦〉 ∈ 𝑆 ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) |
| 232 | | anass 468 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)))) |
| 233 | 20 | peano2zd 12725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℤ) |
| 234 | 233 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ) |
| 235 | 234 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) →
((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈
ℝ) |
| 236 | 8 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℝ) |
| 237 | | nnre 12273 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
| 238 | 237 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ) |
| 239 | | lesub 11742 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(((⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))) + 1) ≤ (𝑄 − 𝑦) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))) |
| 240 | 235, 236,
238, 239 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) →
(((⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))) + 1) ≤ (𝑄 − 𝑦) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))) |
| 241 | 8 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℝ) |
| 242 | 241 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℂ) |
| 243 | 63, 242 | mulcomd 11282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 · 𝑄) = (𝑄 · 𝑃)) |
| 244 | 65, 242 | mulcomd 11282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) · 𝑄) = (𝑄 · (2 · 𝑢))) |
| 245 | 62 | nnne0d 12316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ≠ 0) |
| 246 | 242, 63, 245 | divcan1d 12044 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · 𝑃) = 𝑄) |
| 247 | 246 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · 𝑃) · (2 · 𝑢)) = (𝑄 · (2 · 𝑢))) |
| 248 | 12 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℂ) |
| 249 | 248, 63, 65 | mul32d 11471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · 𝑃) · (2 · 𝑢)) = (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃)) |
| 250 | 244, 247,
249 | 3eqtr2d 2783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) · 𝑄) = (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃)) |
| 251 | 243, 250 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 · 𝑄) − ((2 · 𝑢) · 𝑄)) = ((𝑄 · 𝑃) − (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃))) |
| 252 | 63, 65, 242 | subdird 11720 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑃 · 𝑄) − ((2 · 𝑢) · 𝑄))) |
| 253 | 19 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℂ) |
| 254 | 242, 253,
63 | subdird 11720 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃) = ((𝑄 · 𝑃) − (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃))) |
| 255 | 251, 252,
254 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)) |
| 256 | 255 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)) |
| 257 | 256 | breq2d 5155 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))) |
| 258 | 19 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) |
| 259 | 236, 258 | resubcld 11691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ) |
| 260 | 62 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℕ) |
| 261 | 260 | nnred 12281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ) |
| 262 | 260 | nngt0d 12315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 0 < 𝑃) |
| 263 | | ltmul1 12117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))) |
| 264 | 238, 259,
261, 262, 263 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))) |
| 265 | | ltsub13 11744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦))) |
| 266 | 238, 236,
258, 265 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦))) |
| 267 | 257, 264,
266 | 3bitr2d 307 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦))) |
| 268 | 7 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℕ) |
| 269 | 268 | nnzd 12640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℤ) |
| 270 | | nnz 12634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
| 271 | | zsubcl 12659 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑄 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑄 − 𝑦) ∈ ℤ) |
| 272 | 269, 270,
271 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑄 − 𝑦) ∈ ℤ) |
| 273 | | fllt 13846 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ (𝑄 − 𝑦) ∈ ℤ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦) ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄 − 𝑦))) |
| 274 | 258, 272,
273 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦) ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄 − 𝑦))) |
| 275 | 20 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℤ) |
| 276 | | zltp1le 12667 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((⌊‘((𝑄
/ 𝑃) · (2 ·
𝑢))) ∈ ℤ ∧
(𝑄 − 𝑦) ∈ ℤ) →
((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄 − 𝑦) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄 − 𝑦))) |
| 277 | 275, 272,
276 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) →
((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄 − 𝑦) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄 − 𝑦))) |
| 278 | 267, 274,
277 | 3bitrd 305 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄 − 𝑦))) |
| 279 | | lgsquad.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 𝑁 = ((𝑄 − 1) / 2) |
| 280 | 279 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (2
· 𝑁) = (2 ·
((𝑄 − 1) /
2)) |
| 281 | | peano2rem 11576 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑄 ∈ ℝ → (𝑄 − 1) ∈
ℝ) |
| 282 | 241, 281 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) ∈ ℝ) |
| 283 | 282 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) ∈ ℂ) |
| 284 | | 2cnd 12344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℂ) |
| 285 | 73 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ≠ 0) |
| 286 | 283, 284,
285 | divcan2d 12045 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · ((𝑄 − 1) / 2)) = (𝑄 − 1)) |
| 287 | 280, 286 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) = (𝑄 − 1)) |
| 288 | 287 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = ((𝑄 − 1) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 289 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 1 ∈ ℂ) |
| 290 | 20 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ) |
| 291 | 242, 289,
290 | sub32d 11652 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = ((𝑄 − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) − 1)) |
| 292 | 242, 290,
289 | subsub4d 11651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) − 1) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))) |
| 293 | 288, 291,
292 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))) |
| 294 | 293 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))) |
| 295 | 294 | breq2d 5155 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))) |
| 296 | 240, 278,
295 | 3bitr4d 311 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 297 | 296 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ≤ 𝑁 ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 298 | | 2nn 12339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 2 ∈
ℕ |
| 299 | 6, 279 | gausslemma2dlem0b 27401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 300 | | nnmulcl 12290 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((2
∈ ℕ ∧ 𝑁
∈ ℕ) → (2 · 𝑁) ∈ ℕ) |
| 301 | 298, 299,
300 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (2 · 𝑁) ∈
ℕ) |
| 302 | 301 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℕ) |
| 303 | 302 | nnred 12281 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℝ) |
| 304 | 299 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℕ) |
| 305 | 304 | nnred 12281 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℝ) |
| 306 | 20 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ) |
| 307 | 299 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 308 | 307 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℂ) |
| 309 | 308 | 2timesd 12509 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) = (𝑁 + 𝑁)) |
| 310 | 308, 308,
309 | mvrladdd 11676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) = 𝑁) |
| 311 | 241 | rehalfcld 12513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ∈ ℝ) |
| 312 | 241 | ltm1d 12200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) < 𝑄) |
| 313 | 150 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℝ) |
| 314 | 152 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 2) |
| 315 | | ltdiv1 12132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑄 − 1) ∈ ℝ ∧
𝑄 ∈ ℝ ∧ (2
∈ ℝ ∧ 0 < 2)) → ((𝑄 − 1) < 𝑄 ↔ ((𝑄 − 1) / 2) < (𝑄 / 2))) |
| 316 | 282, 241,
313, 314, 315 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) < 𝑄 ↔ ((𝑄 − 1) / 2) < (𝑄 / 2))) |
| 317 | 312, 316 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) / 2) < (𝑄 / 2)) |
| 318 | 279, 317 | eqbrtrid 5178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 < (𝑄 / 2)) |
| 319 | 305, 311,
318 | ltled 11409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ (𝑄 / 2)) |
| 320 | 242, 284,
63, 285 | div32d 12066 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 2) · 𝑃) = (𝑄 · (𝑃 / 2))) |
| 321 | 124 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℝ) |
| 322 | 321 | rehalfcld 12513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) ∈ ℝ) |
| 323 | | peano2re 11434 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
((⌊‘(𝑀 /
2)) ∈ ℝ → ((⌊‘(𝑀 / 2)) + 1) ∈ ℝ) |
| 324 | 322, 133,
323 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ∈ ℝ) |
| 325 | 15 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℝ) |
| 326 | | flltp1 13840 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑀 / 2) ∈ ℝ →
(𝑀 / 2) <
((⌊‘(𝑀 / 2)) +
1)) |
| 327 | 322, 326 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) < ((⌊‘(𝑀 / 2)) + 1)) |
| 328 | | elfzle1 13567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → ((⌊‘(𝑀 / 2)) + 1) ≤ 𝑢) |
| 329 | 328 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ≤ 𝑢) |
| 330 | 322, 324,
325, 327, 329 | ltletrd 11421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) < 𝑢) |
| 331 | | ltdivmul 12143 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑀 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → ((𝑀 / 2) < 𝑢 ↔ 𝑀 < (2 · 𝑢))) |
| 332 | 321, 325,
313, 314, 331 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 / 2) < 𝑢 ↔ 𝑀 < (2 · 𝑢))) |
| 333 | 330, 332 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 < (2 · 𝑢)) |
| 334 | 122, 333 | eqbrtrrid 5179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) / 2) < (2 · 𝑢)) |
| 335 | 62 | nnred 12281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℝ) |
| 336 | | peano2rem 11576 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈
ℝ) |
| 337 | 335, 336 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℝ) |
| 338 | | ltdivmul 12143 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑃 − 1) ∈ ℝ ∧
(2 · 𝑢) ∈
ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝑃 − 1) / 2) < (2 · 𝑢) ↔ (𝑃 − 1) < (2 · (2 ·
𝑢)))) |
| 339 | 337, 18, 313, 314, 338 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑃 − 1) / 2) < (2 · 𝑢) ↔ (𝑃 − 1) < (2 · (2 ·
𝑢)))) |
| 340 | 334, 339 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) < (2 · (2 ·
𝑢))) |
| 341 | 202 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ) |
| 342 | | zmulcl 12666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((2
∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → (2 · (2
· 𝑢)) ∈
ℤ) |
| 343 | 13, 17, 342 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · (2 · 𝑢)) ∈
ℤ) |
| 344 | | zlem1lt 12669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑃 ∈ ℤ ∧ (2
· (2 · 𝑢))
∈ ℤ) → (𝑃
≤ (2 · (2 · 𝑢)) ↔ (𝑃 − 1) < (2 · (2 ·
𝑢)))) |
| 345 | 341, 343,
344 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 ≤ (2 · (2 · 𝑢)) ↔ (𝑃 − 1) < (2 · (2 ·
𝑢)))) |
| 346 | 340, 345 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ≤ (2 · (2 · 𝑢))) |
| 347 | | ledivmul 12144 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑃 ∈ ℝ ∧ (2
· 𝑢) ∈ ℝ
∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ 𝑃 ≤ (2 · (2 · 𝑢)))) |
| 348 | 335, 18, 313, 314, 347 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ 𝑃 ≤ (2 · (2 · 𝑢)))) |
| 349 | 346, 348 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 / 2) ≤ (2 · 𝑢)) |
| 350 | 335 | rehalfcld 12513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 / 2) ∈ ℝ) |
| 351 | 268 | nngt0d 12315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 𝑄) |
| 352 | | lemul2 12120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑃 / 2) ∈ ℝ ∧ (2
· 𝑢) ∈ ℝ
∧ (𝑄 ∈ ℝ
∧ 0 < 𝑄)) →
((𝑃 / 2) ≤ (2 ·
𝑢) ↔ (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢)))) |
| 353 | 350, 18, 241, 351, 352 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢)))) |
| 354 | 349, 353 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢))) |
| 355 | 320, 354 | eqbrtrd 5165 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢))) |
| 356 | 241, 18 | remulcld 11291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (2 · 𝑢)) ∈ ℝ) |
| 357 | 62 | nngt0d 12315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 𝑃) |
| 358 | | lemuldiv 12148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑄 / 2) ∈ ℝ ∧
(𝑄 · (2 ·
𝑢)) ∈ ℝ ∧
(𝑃 ∈ ℝ ∧ 0
< 𝑃)) → (((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))) |
| 359 | 311, 356,
335, 357, 358 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))) |
| 360 | 355, 359 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)) |
| 361 | 242, 65, 63, 245 | div23d 12080 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 · (2 · 𝑢)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑢))) |
| 362 | 360, 361 | breqtrd 5169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ≤ ((𝑄 / 𝑃) · (2 · 𝑢))) |
| 363 | 305, 311,
19, 319, 362 | letrd 11418 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))) |
| 364 | 299 | nnzd 12640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 365 | 364 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℤ) |
| 366 | | flge 13845 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 367 | 19, 365, 366 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 368 | 363, 367 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) |
| 369 | 310, 368 | eqbrtrd 5165 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) |
| 370 | 303, 305,
306, 369 | subled 11866 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) |
| 371 | 370 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) |
| 372 | 302 | nnzd 12640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℤ) |
| 373 | 372, 20 | zsubcld 12727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ) |
| 374 | 373 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ) |
| 375 | 374 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℝ) |
| 376 | 299 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ) |
| 377 | 376 | nnred 12281 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℝ) |
| 378 | | letr 11355 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ ((2
· 𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) → 𝑦 ≤ 𝑁)) |
| 379 | 238, 375,
377, 378 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) → 𝑦 ≤ 𝑁)) |
| 380 | 371, 379 | mpan2d 694 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → 𝑦 ≤ 𝑁)) |
| 381 | 380 | pm4.71rd 562 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ≤ 𝑁 ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 382 | 297, 381 | bitr4d 282 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 383 | 382 | pm5.32da 579 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 384 | 383 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 385 | 232, 384 | bitrid 283 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 386 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑥 = (𝑃 − (2 · 𝑢))) |
| 387 | 341, 17 | zsubcld 12727 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ) |
| 388 | | elfzle2 13568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → 𝑢 ≤ 𝑀) |
| 389 | 388 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ≤ 𝑀) |
| 390 | 389, 122 | breqtrdi 5184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ≤ ((𝑃 − 1) / 2)) |
| 391 | | lemuldiv2 12149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑢 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧
(2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑢) ≤ (𝑃 − 1) ↔ 𝑢 ≤ ((𝑃 − 1) / 2))) |
| 392 | 325, 337,
313, 314, 391 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) ≤ (𝑃 − 1) ↔ 𝑢 ≤ ((𝑃 − 1) / 2))) |
| 393 | 390, 392 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ≤ (𝑃 − 1)) |
| 394 | 335 | ltm1d 12200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) < 𝑃) |
| 395 | 18, 337, 335, 393, 394 | lelttrd 11419 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) < 𝑃) |
| 396 | 18, 335 | posdifd 11850 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) < 𝑃 ↔ 0 < (𝑃 − (2 · 𝑢)))) |
| 397 | 395, 396 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < (𝑃 − (2 · 𝑢))) |
| 398 | | elnnz 12623 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑃 − (2 · 𝑢)) ∈ ℕ ↔ ((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ 0 <
(𝑃 − (2 ·
𝑢)))) |
| 399 | 387, 397,
398 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℕ) |
| 400 | 63, 65, 289 | sub32d 11652 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) − 1) = ((𝑃 − 1) − (2 · 𝑢))) |
| 401 | 122, 122 | oveq12i 7443 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑀 + 𝑀) = (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) |
| 402 | 62 | nnzd 12640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ) |
| 403 | 402, 204 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℤ) |
| 404 | 403 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℂ) |
| 405 | 404 | 2halvesd 12512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1)) |
| 406 | 401, 405 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 + 𝑀) = (𝑃 − 1)) |
| 407 | 406 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 + 𝑀) − 𝑀) = ((𝑃 − 1) − 𝑀)) |
| 408 | 158 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℂ) |
| 409 | 408, 408 | pncan2d 11622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 + 𝑀) − 𝑀) = 𝑀) |
| 410 | 407, 409 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − 𝑀) = 𝑀) |
| 411 | 410, 333 | eqbrtrd 5165 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − 𝑀) < (2 · 𝑢)) |
| 412 | 337, 321,
18, 411 | ltsub23d 11868 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − (2 · 𝑢)) < 𝑀) |
| 413 | 400, 412 | eqbrtrd 5165 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) − 1) < 𝑀) |
| 414 | 123 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℕ) |
| 415 | 414 | nnzd 12640 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℤ) |
| 416 | | zlem1lt 12669 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑃 − (2 · 𝑢)) ≤ 𝑀 ↔ ((𝑃 − (2 · 𝑢)) − 1) < 𝑀)) |
| 417 | 387, 415,
416 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) ≤ 𝑀 ↔ ((𝑃 − (2 · 𝑢)) − 1) < 𝑀)) |
| 418 | 413, 417 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ≤ 𝑀) |
| 419 | | fznn 13632 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀 ∈ ℤ → ((𝑃 − (2 · 𝑢)) ∈ (1...𝑀) ↔ ((𝑃 − (2 · 𝑢)) ∈ ℕ ∧ (𝑃 − (2 · 𝑢)) ≤ 𝑀))) |
| 420 | 415, 419 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) ∈ (1...𝑀) ↔ ((𝑃 − (2 · 𝑢)) ∈ ℕ ∧ (𝑃 − (2 · 𝑢)) ≤ 𝑀))) |
| 421 | 399, 418,
420 | mpbir2and 713 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ (1...𝑀)) |
| 422 | 421 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑃 − (2 · 𝑢)) ∈ (1...𝑀)) |
| 423 | 386, 422 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑥 ∈ (1...𝑀)) |
| 424 | 423 | biantrurd 532 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...𝑁) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)))) |
| 425 | 364 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑁 ∈ ℤ) |
| 426 | | fznn 13632 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℤ → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁))) |
| 427 | 425, 426 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁))) |
| 428 | 424, 427 | bitr3d 281 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁))) |
| 429 | 386 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑥 · 𝑄) = ((𝑃 − (2 · 𝑢)) · 𝑄)) |
| 430 | 429 | breq2d 5155 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑦 · 𝑃) < (𝑥 · 𝑄) ↔ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) |
| 431 | 428, 430 | anbi12d 632 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ ((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)))) |
| 432 | 373 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ) |
| 433 | | fznn 13632 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((2
· 𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ →
(𝑦 ∈ (1...((2 ·
𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 434 | 432, 433 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 435 | 385, 431,
434 | 3bitr4d 311 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 436 | 231, 435 | bitrid 283 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (〈𝑥, 𝑦〉 ∈ 𝑆 ↔ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 437 | 436 | pm5.32da 579 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑥 = (𝑃 − (2 · 𝑢)) ∧ 〈𝑥, 𝑦〉 ∈ 𝑆) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))) |
| 438 | | vex 3484 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑥 ∈ V |
| 439 | | vex 3484 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑦 ∈ V |
| 440 | 438, 439 | op1std 8024 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) |
| 441 | 440 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((1st ‘𝑧) = (𝑃 − (2 · 𝑢)) ↔ 𝑥 = (𝑃 − (2 · 𝑢)))) |
| 442 | 441 | elrab 3692 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ↔ (〈𝑥, 𝑦〉 ∈ 𝑆 ∧ 𝑥 = (𝑃 − (2 · 𝑢)))) |
| 443 | 442 | biancomi 462 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 〈𝑥, 𝑦〉 ∈ 𝑆)) |
| 444 | | opelxp 5721 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 ·
𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 ∈ {(𝑃 − (2 · 𝑢))} ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 445 | | velsn 4642 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ {(𝑃 − (2 · 𝑢))} ↔ 𝑥 = (𝑃 − (2 · 𝑢))) |
| 446 | 445 | anbi1i 624 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ {(𝑃 − (2 · 𝑢))} ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 447 | 444, 446 | bitri 275 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 ·
𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 448 | 437, 443,
447 | 3bitr4g 314 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (〈𝑥, 𝑦〉 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ↔ 〈𝑥, 𝑦〉 ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))) |
| 449 | 227, 228,
448 | eqrelrdv 5802 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} = ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 450 | 449 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘{𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = (♯‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))) |
| 451 | | fzfid 14014 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin) |
| 452 | | xpsnen2g 9105 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ (1...((2
· 𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin) →
({(𝑃 − (2 ·
𝑢))} × (1...((2
· 𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 ·
𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 453 | 387, 451,
452 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 454 | | hasheni 14387 |
. . . . . . . . . . . . 13
⊢ (({(𝑃 − (2 · 𝑢))} × (1...((2 ·
𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 ·
𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) →
(♯‘({(𝑃 −
(2 · 𝑢))} ×
(1...((2 · 𝑁)
− (⌊‘((𝑄
/ 𝑃) · (2 ·
𝑢))))))) =
(♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 455 | 453, 454 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘({(𝑃 − (2 · 𝑢))} × (1...((2 ·
𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) =
(♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 456 | | ltmul2 12118 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((2
· 𝑢) ∈ ℝ
∧ 𝑃 ∈ ℝ
∧ (𝑄 ∈ ℝ
∧ 0 < 𝑄)) → ((2
· 𝑢) < 𝑃 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃))) |
| 457 | 18, 335, 241, 351, 456 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) < 𝑃 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃))) |
| 458 | 395, 457 | mpbid 232 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)) |
| 459 | | ltdivmul2 12145 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑄 · (2 · 𝑢)) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 <
𝑃)) → (((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃))) |
| 460 | 356, 241,
335, 357, 459 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃))) |
| 461 | 458, 460 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄) |
| 462 | 361, 461 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄) |
| 463 | | fllt 13846 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑄 ∈ ℤ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄)) |
| 464 | 19, 269, 463 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄)) |
| 465 | 462, 464 | mpbid 232 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄) |
| 466 | | zltlem1 12670 |
. . . . . . . . . . . . . . . . 17
⊢
(((⌊‘((𝑄
/ 𝑃) · (2 ·
𝑢))) ∈ ℤ ∧
𝑄 ∈ ℤ) →
((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1))) |
| 467 | 20, 269, 466 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1))) |
| 468 | 465, 467 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1)) |
| 469 | 468, 287 | breqtrrd 5171 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (2 · 𝑁)) |
| 470 | | eluz2 12884 |
. . . . . . . . . . . . . 14
⊢ ((2
· 𝑁) ∈
(ℤ≥‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (2 · 𝑁) ∈ ℤ ∧
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (2 · 𝑁))) |
| 471 | 20, 372, 469, 470 | syl3anbrc 1344 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈
(ℤ≥‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 472 | | uznn0sub 12917 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑁) ∈
(ℤ≥‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈
ℕ0) |
| 473 | | hashfz1 14385 |
. . . . . . . . . . . . 13
⊢ (((2
· 𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℕ0
→ (♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 474 | 471, 472,
473 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘(1...((2 ·
𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 475 | 450, 455,
474 | 3eqtrd 2781 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘{𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 476 | 475 | sumeq2dv 15738 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(♯‘{𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 477 | 80, 224, 476 | 3eqtr3rd 2786 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) |
| 478 | 301 | nncnd 12282 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · 𝑁) ∈
ℂ) |
| 479 | 478 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℂ) |
| 480 | 5, 479, 290 | fsumsub 15824 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 481 | 477, 480 | eqtr3d 2779 |
. . . . . . . 8
⊢ (𝜑 → (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 482 | 481 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) =
(Σ𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 483 | 21 | zcnd 12723 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ) |
| 484 | 5, 372 | fsumzcl 15771 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) ∈ ℤ) |
| 485 | 484 | zcnd 12723 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) ∈ ℂ) |
| 486 | 483, 485 | pncan3d 11623 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁)) |
| 487 | | fsumconst 15826 |
. . . . . . . . 9
⊢
(((((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin ∧ (2 · 𝑁) ∈ ℂ) →
Σ𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(2 · 𝑁) =
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁))) |
| 488 | 5, 478, 487 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁))) |
| 489 | | hashcl 14395 |
. . . . . . . . . . 11
⊢
((((⌊‘(𝑀
/ 2)) + 1)...𝑀) ∈ Fin
→ (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈
ℕ0) |
| 490 | 5, 489 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈
ℕ0) |
| 491 | 490 | nn0cnd 12589 |
. . . . . . . . 9
⊢ (𝜑 →
(♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℂ) |
| 492 | | 2cnd 12344 |
. . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℂ) |
| 493 | 491, 492,
307 | mul12d 11470 |
. . . . . . . 8
⊢ (𝜑 →
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)) = (2 ·
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) |
| 494 | 488, 493 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = (2 ·
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) |
| 495 | 482, 486,
494 | 3eqtrd 2781 |
. . . . . 6
⊢ (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) = (2 ·
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) |
| 496 | 495 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) = (-1↑(2
· ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))) |
| 497 | 13 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 2 ∈
ℤ) |
| 498 | 490 | nn0zd 12639 |
. . . . . . 7
⊢ (𝜑 →
(♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℤ) |
| 499 | 498, 364 | zmulcld 12728 |
. . . . . 6
⊢ (𝜑 →
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ) |
| 500 | | expmulz 14149 |
. . . . . 6
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ)) → (-1↑(2
· ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) =
((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) |
| 501 | 2, 4, 497, 499, 500 | syl22anc 839 |
. . . . 5
⊢ (𝜑 → (-1↑(2 ·
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) =
((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) |
| 502 | | neg1sqe1 14235 |
. . . . . . 7
⊢
(-1↑2) = 1 |
| 503 | 502 | oveq1i 7441 |
. . . . . 6
⊢
((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) =
(1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) |
| 504 | | 1exp 14132 |
. . . . . . 7
⊢
(((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ →
(1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1) |
| 505 | 499, 504 | syl 17 |
. . . . . 6
⊢ (𝜑 →
(1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1) |
| 506 | 503, 505 | eqtrid 2789 |
. . . . 5
⊢ (𝜑 →
((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1) |
| 507 | 496, 501,
506 | 3eqtrd 2781 |
. . . 4
⊢ (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) =
1) |
| 508 | 41, 52, 507 | 3eqtr4d 2787 |
. . 3
⊢ (𝜑 →
((-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) =
(-1↑(Σ𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})))) |
| 509 | | expaddz 14147 |
. . . 4
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧
(♯‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)})
∈ ℤ)) → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) =
((-1↑Σ𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})))) |
| 510 | 2, 4, 21, 39, 509 | syl22anc 839 |
. . 3
⊢ (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) =
((-1↑Σ𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})))) |
| 511 | 508, 510 | eqtr2d 2778 |
. 2
⊢ (𝜑 → ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) =
((-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})))) |
| 512 | 22, 38, 38, 40, 511 | mulcan2ad 11899 |
1
⊢ (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) |