| Step | Hyp | Ref
| Expression |
| 1 | | neg1cn 9095 |
. . . 4
⊢ -1 ∈
ℂ |
| 2 | 1 | a1i 9 |
. . 3
⊢ (𝜑 → -1 ∈
ℂ) |
| 3 | | neg1ap0 9099 |
. . . 4
⊢ -1 #
0 |
| 4 | 3 | a1i 9 |
. . 3
⊢ (𝜑 → -1 # 0) |
| 5 | | lgseisen.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
| 6 | | lgsquad.4 |
. . . . . . . . . 10
⊢ 𝑀 = ((𝑃 − 1) / 2) |
| 7 | 5, 6 | gausslemma2dlem0b 15291 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 8 | 7 | nnzd 9447 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 9 | | 2nn 9152 |
. . . . . . . 8
⊢ 2 ∈
ℕ |
| 10 | | znq 9698 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 2 ∈
ℕ) → (𝑀 / 2)
∈ ℚ) |
| 11 | 8, 9, 10 | sylancl 413 |
. . . . . . 7
⊢ (𝜑 → (𝑀 / 2) ∈ ℚ) |
| 12 | 11 | flqcld 10367 |
. . . . . 6
⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈
ℤ) |
| 13 | 12 | peano2zd 9451 |
. . . . 5
⊢ (𝜑 → ((⌊‘(𝑀 / 2)) + 1) ∈
ℤ) |
| 14 | 13, 8 | fzfigd 10523 |
. . . 4
⊢ (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin) |
| 15 | | lgseisen.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 ∈ (ℙ ∖
{2})) |
| 16 | 15 | gausslemma2dlem0a 15290 |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ ℕ) |
| 17 | 16 | nnzd 9447 |
. . . . . . 7
⊢ (𝜑 → 𝑄 ∈ ℤ) |
| 18 | 5 | gausslemma2dlem0a 15290 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℕ) |
| 19 | 18 | adantr 276 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℕ) |
| 20 | | znq 9698 |
. . . . . . 7
⊢ ((𝑄 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑄 / 𝑃) ∈ ℚ) |
| 21 | 17, 19, 20 | syl2an2r 595 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℚ) |
| 22 | | 2z 9354 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
| 23 | | elfzelz 10100 |
. . . . . . . . 9
⊢ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → 𝑢 ∈ ℤ) |
| 24 | 23 | adantl 277 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℤ) |
| 25 | | zmulcl 9379 |
. . . . . . . 8
⊢ ((2
∈ ℤ ∧ 𝑢
∈ ℤ) → (2 · 𝑢) ∈ ℤ) |
| 26 | 22, 24, 25 | sylancr 414 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℤ) |
| 27 | | zq 9700 |
. . . . . . 7
⊢ ((2
· 𝑢) ∈ ℤ
→ (2 · 𝑢)
∈ ℚ) |
| 28 | 26, 27 | syl 14 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℚ) |
| 29 | | qmulcl 9711 |
. . . . . 6
⊢ (((𝑄 / 𝑃) ∈ ℚ ∧ (2 · 𝑢) ∈ ℚ) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℚ) |
| 30 | 21, 28, 29 | syl2anc 411 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℚ) |
| 31 | 30 | flqcld 10367 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ) |
| 32 | 14, 31 | fsumzcl 11567 |
. . 3
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ) |
| 33 | 2, 4, 32 | expclzapd 10770 |
. 2
⊢ (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℂ) |
| 34 | | lgseisen.3 |
. . . . 5
⊢ (𝜑 → 𝑃 ≠ 𝑄) |
| 35 | | lgsquad.5 |
. . . . 5
⊢ 𝑁 = ((𝑄 − 1) / 2) |
| 36 | | lgsquad.6 |
. . . . 5
⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} |
| 37 | 5, 15, 34, 6, 35, 36 | lgsquadlemofi 15317 |
. . . 4
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
| 38 | | hashcl 10873 |
. . . 4
⊢ ({𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈ Fin
→ (♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)}) ∈
ℕ0) |
| 39 | 37, 38 | syl 14 |
. . 3
⊢ (𝜑 → (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) ∈
ℕ0) |
| 40 | | expcl 10649 |
. . 3
⊢ ((-1
∈ ℂ ∧ (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) ∈
ℕ0) → (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) ∈
ℂ) |
| 41 | 1, 39, 40 | sylancr 414 |
. 2
⊢ (𝜑 →
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) ∈ ℂ) |
| 42 | 39 | nn0zd 9446 |
. . 3
⊢ (𝜑 → (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) ∈
ℤ) |
| 43 | 2, 4, 42 | expap0d 10771 |
. 2
⊢ (𝜑 →
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) # 0) |
| 44 | 41, 43 | recidapd 8810 |
. . . 4
⊢ (𝜑 →
((-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) · (1 /
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})))) = 1) |
| 45 | | 1div1e1 8731 |
. . . . . . . . 9
⊢ (1 / 1) =
1 |
| 46 | 45 | negeqi 8220 |
. . . . . . . 8
⊢ -(1 / 1)
= -1 |
| 47 | | ax-1cn 7972 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
| 48 | | 1ap0 8617 |
. . . . . . . . 9
⊢ 1 #
0 |
| 49 | | divneg2ap 8763 |
. . . . . . . . 9
⊢ ((1
∈ ℂ ∧ 1 ∈ ℂ ∧ 1 # 0) → -(1 / 1) = (1 /
-1)) |
| 50 | 47, 47, 48, 49 | mp3an 1348 |
. . . . . . . 8
⊢ -(1 / 1)
= (1 / -1) |
| 51 | 46, 50 | eqtr3i 2219 |
. . . . . . 7
⊢ -1 = (1 /
-1) |
| 52 | 51 | oveq1i 5932 |
. . . . . 6
⊢
(-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) = ((1 /
-1)↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) |
| 53 | 2, 4, 42 | exprecapd 10773 |
. . . . . 6
⊢ (𝜑 → ((1 /
-1)↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) = (1 / (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})))) |
| 54 | 52, 53 | eqtrid 2241 |
. . . . 5
⊢ (𝜑 →
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) = (1 / (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})))) |
| 55 | 54 | oveq2d 5938 |
. . . 4
⊢ (𝜑 →
((-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) =
((-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) · (1 /
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)}))))) |
| 56 | 5, 15, 34, 6, 35, 36 | lgsquadlemsfi 15316 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ Fin) |
| 57 | 56 | adantr 276 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑆 ∈ Fin) |
| 58 | | opabssxp 4737 |
. . . . . . . . . . . . . . . . . 18
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁)) |
| 59 | 36, 58 | eqsstri 3215 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑆 ⊆ ((1...𝑀) × (1...𝑁)) |
| 60 | 59 | sseli 3179 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((1...𝑀) × (1...𝑁))) |
| 61 | | xp1st 6223 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ((1...𝑀) × (1...𝑁)) → (1st ‘𝑧) ∈ (1...𝑀)) |
| 62 | 60, 61 | syl 14 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑆 → (1st ‘𝑧) ∈ (1...𝑀)) |
| 63 | 62 | elfzelzd 10101 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ 𝑆 → (1st ‘𝑧) ∈
ℤ) |
| 64 | 19 | nnzd 9447 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ) |
| 65 | 64, 26 | zsubcld 9453 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ) |
| 66 | | zdceq 9401 |
. . . . . . . . . . . . . 14
⊢
(((1st ‘𝑧) ∈ ℤ ∧ (𝑃 − (2 · 𝑢)) ∈ ℤ) →
DECID (1st ‘𝑧) = (𝑃 − (2 · 𝑢))) |
| 67 | 63, 65, 66 | syl2anr 290 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑧 ∈ 𝑆) → DECID
(1st ‘𝑧) =
(𝑃 − (2 ·
𝑢))) |
| 68 | 67 | ralrimiva 2570 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ∀𝑧 ∈ 𝑆 DECID (1st
‘𝑧) = (𝑃 − (2 · 𝑢))) |
| 69 | 57, 68 | ssfirab 6997 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ∈ Fin) |
| 70 | | fveqeq2 5567 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑣 → ((1st ‘𝑧) = (𝑃 − (2 · 𝑢)) ↔ (1st ‘𝑣) = (𝑃 − (2 · 𝑢)))) |
| 71 | 70 | elrab 2920 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ↔ (𝑣 ∈ 𝑆 ∧ (1st ‘𝑣) = (𝑃 − (2 · 𝑢)))) |
| 72 | 71 | simprbi 275 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} → (1st ‘𝑣) = (𝑃 − (2 · 𝑢))) |
| 73 | 72 | ad2antll 491 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (1st ‘𝑣) = (𝑃 − (2 · 𝑢))) |
| 74 | 73 | oveq2d 5938 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (1st ‘𝑣)) = (𝑃 − (𝑃 − (2 · 𝑢)))) |
| 75 | 19 | nncnd 9004 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℂ) |
| 76 | 75 | adantrr 479 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → 𝑃 ∈ ℂ) |
| 77 | 26 | zcnd 9449 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℂ) |
| 78 | 77 | adantrr 479 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (2 · 𝑢) ∈ ℂ) |
| 79 | 76, 78 | nncand 8342 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (𝑃 − (2 · 𝑢))) = (2 · 𝑢)) |
| 80 | 74, 79 | eqtrd 2229 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (1st ‘𝑣)) = (2 · 𝑢)) |
| 81 | 80 | oveq1d 5937 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → ((𝑃 − (1st ‘𝑣)) / 2) = ((2 · 𝑢) / 2)) |
| 82 | 24 | zcnd 9449 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℂ) |
| 83 | 82 | adantrr 479 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → 𝑢 ∈ ℂ) |
| 84 | | 2cnd 9063 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → 2 ∈
ℂ) |
| 85 | | 2ap0 9083 |
. . . . . . . . . . . . . . . 16
⊢ 2 #
0 |
| 86 | 85 | a1i 9 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → 2 # 0) |
| 87 | 83, 84, 86 | divcanap3d 8822 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → ((2 · 𝑢) / 2) = 𝑢) |
| 88 | 81, 87 | eqtrd 2229 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → ((𝑃 − (1st ‘𝑣)) / 2) = 𝑢) |
| 89 | 88 | ralrimivva 2579 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)∀𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ((𝑃 − (1st ‘𝑣)) / 2) = 𝑢) |
| 90 | | invdisj 4027 |
. . . . . . . . . . . 12
⊢
(∀𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)∀𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ((𝑃 − (1st ‘𝑣)) / 2) = 𝑢 → Disj 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))}) |
| 91 | 89, 90 | syl 14 |
. . . . . . . . . . 11
⊢ (𝜑 → Disj 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))}) |
| 92 | 14, 69, 91 | hashiun 11643 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘∪ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(♯‘{𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) |
| 93 | | iunrab 3964 |
. . . . . . . . . . . 12
⊢ ∪ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧 ∈ 𝑆 ∣ ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st ‘𝑧) = (𝑃 − (2 · 𝑢))} |
| 94 | | eldifsni 3751 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ≠
2) |
| 95 | 5, 94 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑃 ≠ 2) |
| 96 | 95 | necomd 2453 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 2 ≠ 𝑃) |
| 97 | 96 | neneqd 2388 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ¬ 2 = 𝑃) |
| 98 | 97 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 = 𝑃) |
| 99 | | uzid 9615 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
| 100 | 22, 99 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
(ℤ≥‘2) |
| 101 | 5 | eldifad 3168 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑃 ∈ ℙ) |
| 102 | 101 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℙ) |
| 103 | | dvdsprm 12305 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (2 ∥ 𝑃 ↔ 2 = 𝑃)) |
| 104 | 100, 102,
103 | sylancr 414 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ 𝑃 ↔ 2 = 𝑃)) |
| 105 | 98, 104 | mtbird 674 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ 𝑃) |
| 106 | 18 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℕ) |
| 107 | 106 | nncnd 9004 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℂ) |
| 108 | 26 | adantlr 477 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℤ) |
| 109 | 108 | zcnd 9449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℂ) |
| 110 | 107, 109 | npcand 8341 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)) = 𝑃) |
| 111 | 110 | breq2d 4045 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)) ↔ 2 ∥ 𝑃)) |
| 112 | 105, 111 | mtbird 674 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))) |
| 113 | 23 | adantl 277 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℤ) |
| 114 | | dvdsmul1 11978 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℤ ∧ 𝑢
∈ ℤ) → 2 ∥ (2 · 𝑢)) |
| 115 | 22, 113, 114 | sylancr 414 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∥ (2 · 𝑢)) |
| 116 | 22 | a1i 9 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℤ) |
| 117 | 106 | nnzd 9447 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ) |
| 118 | 117, 108 | zsubcld 9453 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ) |
| 119 | | dvds2add 11990 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℤ ∧ (𝑃
− (2 · 𝑢))
∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → ((2 ∥ (𝑃 − (2 · 𝑢)) ∧ 2 ∥ (2 ·
𝑢)) → 2 ∥
((𝑃 − (2 ·
𝑢)) + (2 · 𝑢)))) |
| 120 | 116, 118,
108, 119 | syl3anc 1249 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 ∥ (𝑃 − (2 · 𝑢)) ∧ 2 ∥ (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)))) |
| 121 | 115, 120 | mpan2d 428 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ (𝑃 − (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)))) |
| 122 | 112, 121 | mtod 664 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ (𝑃 − (2 · 𝑢))) |
| 123 | | breq2 4037 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑧) = (𝑃 − (2 · 𝑢)) → (2 ∥ (1st
‘𝑧) ↔ 2 ∥
(𝑃 − (2 ·
𝑢)))) |
| 124 | 123 | notbid 668 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑧) = (𝑃 − (2 · 𝑢)) → (¬ 2 ∥ (1st
‘𝑧) ↔ ¬ 2
∥ (𝑃 − (2
· 𝑢)))) |
| 125 | 122, 124 | syl5ibrcom 157 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((1st ‘𝑧) = (𝑃 − (2 · 𝑢)) → ¬ 2 ∥ (1st
‘𝑧))) |
| 126 | 125 | rexlimdva 2614 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st ‘𝑧) = (𝑃 − (2 · 𝑢)) → ¬ 2 ∥ (1st
‘𝑧))) |
| 127 | | simpr 110 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆) |
| 128 | 59, 127 | sselid 3181 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ ((1...𝑀) × (1...𝑁))) |
| 129 | 128, 61 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (1st ‘𝑧) ∈ (1...𝑀)) |
| 130 | | elfzelz 10100 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑧) ∈ (1...𝑀) → (1st ‘𝑧) ∈
ℤ) |
| 131 | | odd2np1 12038 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑧) ∈ ℤ → (¬ 2 ∥
(1st ‘𝑧)
↔ ∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = (1st ‘𝑧))) |
| 132 | 129, 130,
131 | 3syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ 2 ∥ (1st
‘𝑧) ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) =
(1st ‘𝑧))) |
| 133 | 11 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 / 2) ∈
ℚ) |
| 134 | 133 | flqcld 10367 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
(⌊‘(𝑀 / 2))
∈ ℤ) |
| 135 | 134 | peano2zd 9451 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
((⌊‘(𝑀 / 2)) +
1) ∈ ℤ) |
| 136 | 7 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑀 ∈
ℕ) |
| 137 | 136 | nnzd 9447 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑀 ∈
ℤ) |
| 138 | | simprl 529 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑛 ∈
ℤ) |
| 139 | 137, 138 | zsubcld 9453 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 − 𝑛) ∈ ℤ) |
| 140 | 134 | zred 9448 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
(⌊‘(𝑀 / 2))
∈ ℝ) |
| 141 | 7 | nnred 9003 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 142 | 141 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑀 ∈
ℝ) |
| 143 | 142 | rehalfcld 9238 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 / 2) ∈
ℝ) |
| 144 | 139 | zred 9448 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 − 𝑛) ∈ ℝ) |
| 145 | | flqle 10368 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 / 2) ∈ ℚ →
(⌊‘(𝑀 / 2))
≤ (𝑀 /
2)) |
| 146 | 133, 145 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
(⌊‘(𝑀 / 2))
≤ (𝑀 /
2)) |
| 147 | | zre 9330 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℝ) |
| 148 | 147 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑛 ∈
ℝ) |
| 149 | | simprr 531 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑛) + 1) =
(1st ‘𝑧)) |
| 150 | 129 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
(1st ‘𝑧)
∈ (1...𝑀)) |
| 151 | 149, 150 | eqeltrd 2273 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑛) + 1) ∈
(1...𝑀)) |
| 152 | | elfzle2 10103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((2
· 𝑛) + 1) ∈
(1...𝑀) → ((2 ·
𝑛) + 1) ≤ 𝑀) |
| 153 | 151, 152 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑛) + 1) ≤ 𝑀) |
| 154 | | zmulcl 9379 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((2
∈ ℤ ∧ 𝑛
∈ ℤ) → (2 · 𝑛) ∈ ℤ) |
| 155 | 22, 138, 154 | sylancr 414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· 𝑛) ∈
ℤ) |
| 156 | | zltp1le 9380 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((2
· 𝑛) ∈ ℤ
∧ 𝑀 ∈ ℤ)
→ ((2 · 𝑛) <
𝑀 ↔ ((2 · 𝑛) + 1) ≤ 𝑀)) |
| 157 | 155, 137,
156 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑛) < 𝑀 ↔ ((2 · 𝑛) + 1) ≤ 𝑀)) |
| 158 | 153, 157 | mpbird 167 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· 𝑛) < 𝑀) |
| 159 | | 2re 9060 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ∈
ℝ |
| 160 | 159 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 2 ∈
ℝ) |
| 161 | | 2pos 9081 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 <
2 |
| 162 | 161 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 0 <
2) |
| 163 | | ltmuldiv2 8902 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → ((2 · 𝑛) < 𝑀 ↔ 𝑛 < (𝑀 / 2))) |
| 164 | 148, 142,
160, 162, 163 | syl112anc 1253 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑛) < 𝑀 ↔ 𝑛 < (𝑀 / 2))) |
| 165 | 158, 164 | mpbid 147 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑛 < (𝑀 / 2)) |
| 166 | 143 | recnd 8055 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 / 2) ∈
ℂ) |
| 167 | 7 | nncnd 9004 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑀 ∈ ℂ) |
| 168 | 167 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑀 ∈
ℂ) |
| 169 | 168 | 2halvesd 9237 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((𝑀 / 2) + (𝑀 / 2)) = 𝑀) |
| 170 | 166, 166,
169 | mvlraddd 8390 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 / 2) = (𝑀 − (𝑀 / 2))) |
| 171 | 165, 170 | breqtrd 4059 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑛 < (𝑀 − (𝑀 / 2))) |
| 172 | 148, 142,
143, 171 | ltsub13d 8578 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 / 2) < (𝑀 − 𝑛)) |
| 173 | 140, 143,
144, 146, 172 | lelttrd 8151 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
(⌊‘(𝑀 / 2))
< (𝑀 − 𝑛)) |
| 174 | | zltp1le 9380 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((⌊‘(𝑀
/ 2)) ∈ ℤ ∧ (𝑀 − 𝑛) ∈ ℤ) →
((⌊‘(𝑀 / 2))
< (𝑀 − 𝑛) ↔ ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀 − 𝑛))) |
| 175 | 134, 139,
174 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
((⌊‘(𝑀 / 2))
< (𝑀 − 𝑛) ↔ ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀 − 𝑛))) |
| 176 | 173, 175 | mpbid 147 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
((⌊‘(𝑀 / 2)) +
1) ≤ (𝑀 − 𝑛)) |
| 177 | | 2t0e0 9150 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
· 0) = 0 |
| 178 | | 2cn 9061 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ∈
ℂ |
| 179 | | zcn 9331 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
| 180 | 179 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑛 ∈
ℂ) |
| 181 | | mulcl 8006 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((2
∈ ℂ ∧ 𝑛
∈ ℂ) → (2 · 𝑛) ∈ ℂ) |
| 182 | 178, 180,
181 | sylancr 414 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· 𝑛) ∈
ℂ) |
| 183 | | pncan 8232 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((2
· 𝑛) ∈ ℂ
∧ 1 ∈ ℂ) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛)) |
| 184 | 182, 47, 183 | sylancl 413 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (((2
· 𝑛) + 1) − 1)
= (2 · 𝑛)) |
| 185 | | elfznn 10129 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((2
· 𝑛) + 1) ∈
(1...𝑀) → ((2 ·
𝑛) + 1) ∈
ℕ) |
| 186 | | nnm1nn0 9290 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((2
· 𝑛) + 1) ∈
ℕ → (((2 · 𝑛) + 1) − 1) ∈
ℕ0) |
| 187 | 151, 185,
186 | 3syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (((2
· 𝑛) + 1) − 1)
∈ ℕ0) |
| 188 | 184, 187 | eqeltrrd 2274 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· 𝑛) ∈
ℕ0) |
| 189 | 188 | nn0ge0d 9305 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 0 ≤
(2 · 𝑛)) |
| 190 | 177, 189 | eqbrtrid 4068 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· 0) ≤ (2 · 𝑛)) |
| 191 | | 0red 8027 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 0 ∈
ℝ) |
| 192 | | lemul2 8884 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0
∈ ℝ ∧ 𝑛
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (0 ≤ 𝑛 ↔ (2 · 0) ≤ (2
· 𝑛))) |
| 193 | 191, 148,
160, 162, 192 | syl112anc 1253 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (0 ≤
𝑛 ↔ (2 · 0)
≤ (2 · 𝑛))) |
| 194 | 190, 193 | mpbird 167 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 0 ≤
𝑛) |
| 195 | 142, 148 | subge02d 8564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (0 ≤
𝑛 ↔ (𝑀 − 𝑛) ≤ 𝑀)) |
| 196 | 194, 195 | mpbid 147 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 − 𝑛) ≤ 𝑀) |
| 197 | 135, 137,
139, 176, 196 | elfzd 10091 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 − 𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) |
| 198 | 101 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑃 ∈
ℙ) |
| 199 | | prmnn 12278 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 200 | 198, 199 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑃 ∈
ℕ) |
| 201 | 200 | nncnd 9004 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑃 ∈
ℂ) |
| 202 | | peano2cn 8161 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
· 𝑛) ∈ ℂ
→ ((2 · 𝑛) + 1)
∈ ℂ) |
| 203 | 182, 202 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑛) + 1) ∈
ℂ) |
| 204 | 201, 203 | nncand 8342 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑃 − (𝑃 − ((2 · 𝑛) + 1))) = ((2 · 𝑛) + 1)) |
| 205 | | 1cnd 8042 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 1 ∈
ℂ) |
| 206 | 201, 182,
205 | sub32d 8369 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((𝑃 − (2 · 𝑛)) − 1) = ((𝑃 − 1) − (2 ·
𝑛))) |
| 207 | 201, 182,
205 | subsub4d 8368 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((𝑃 − (2 · 𝑛)) − 1) = (𝑃 − ((2 · 𝑛) + 1))) |
| 208 | | 2cnd 9063 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 2 ∈
ℂ) |
| 209 | 208, 168,
180 | subdid 8440 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· (𝑀 − 𝑛)) = ((2 · 𝑀) − (2 · 𝑛))) |
| 210 | 6 | oveq2i 5933 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2
· 𝑀) = (2 ·
((𝑃 − 1) /
2)) |
| 211 | 18 | nnzd 9447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝑃 ∈ ℤ) |
| 212 | 211 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑃 ∈
ℤ) |
| 213 | | peano2zm 9364 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈
ℤ) |
| 214 | 212, 213 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑃 − 1) ∈
ℤ) |
| 215 | 214 | zcnd 9449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑃 − 1) ∈
ℂ) |
| 216 | 160, 162 | gt0ap0d 8656 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 2 #
0) |
| 217 | 215, 208,
216 | divcanap2d 8819 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· ((𝑃 − 1) /
2)) = (𝑃 −
1)) |
| 218 | 210, 217 | eqtrid 2241 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· 𝑀) = (𝑃 − 1)) |
| 219 | 218 | oveq1d 5937 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑀) − (2
· 𝑛)) = ((𝑃 − 1) − (2 ·
𝑛))) |
| 220 | 209, 219 | eqtr2d 2230 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((𝑃 − 1) − (2 ·
𝑛)) = (2 · (𝑀 − 𝑛))) |
| 221 | 206, 207,
220 | 3eqtr3d 2237 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑃 − ((2 · 𝑛) + 1)) = (2 · (𝑀 − 𝑛))) |
| 222 | 221 | oveq2d 5938 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑃 − (𝑃 − ((2 · 𝑛) + 1))) = (𝑃 − (2 · (𝑀 − 𝑛)))) |
| 223 | 204, 222,
149 | 3eqtr3rd 2238 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
(1st ‘𝑧) =
(𝑃 − (2 ·
(𝑀 − 𝑛)))) |
| 224 | | oveq2 5930 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = (𝑀 − 𝑛) → (2 · 𝑢) = (2 · (𝑀 − 𝑛))) |
| 225 | 224 | oveq2d 5938 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = (𝑀 − 𝑛) → (𝑃 − (2 · 𝑢)) = (𝑃 − (2 · (𝑀 − 𝑛)))) |
| 226 | 225 | rspceeqv 2886 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 − 𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ (1st ‘𝑧) = (𝑃 − (2 · (𝑀 − 𝑛)))) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st ‘𝑧) = (𝑃 − (2 · 𝑢))) |
| 227 | 197, 223,
226 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
∃𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(1st
‘𝑧) = (𝑃 − (2 · 𝑢))) |
| 228 | 227 | rexlimdvaa 2615 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (1st
‘𝑧) →
∃𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(1st
‘𝑧) = (𝑃 − (2 · 𝑢)))) |
| 229 | 132, 228 | sylbid 150 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ 2 ∥ (1st
‘𝑧) →
∃𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(1st
‘𝑧) = (𝑃 − (2 · 𝑢)))) |
| 230 | 126, 229 | impbid 129 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st ‘𝑧) = (𝑃 − (2 · 𝑢)) ↔ ¬ 2 ∥ (1st
‘𝑧))) |
| 231 | 230 | rabbidva 2751 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st ‘𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) |
| 232 | 93, 231 | eqtrid 2241 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) |
| 233 | 232 | fveq2d 5562 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘∪ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) |
| 234 | | ssrab2 3268 |
. . . . . . . . . . . . . . 15
⊢ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆 |
| 235 | 36 | relopabiv 4789 |
. . . . . . . . . . . . . . 15
⊢ Rel 𝑆 |
| 236 | | relss 4750 |
. . . . . . . . . . . . . . 15
⊢ ({𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆 → (Rel 𝑆 → Rel {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) |
| 237 | 234, 235,
236 | mp2 16 |
. . . . . . . . . . . . . 14
⊢ Rel
{𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} |
| 238 | | relxp 4772 |
. . . . . . . . . . . . . 14
⊢ Rel
({(𝑃 − (2 ·
𝑢))} × (1...((2
· 𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 239 | 36 | eleq2i 2263 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑥, 𝑦〉 ∈ 𝑆 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}) |
| 240 | | opabidw 4291 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) |
| 241 | 239, 240 | bitri 184 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑥, 𝑦〉 ∈ 𝑆 ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) |
| 242 | | anass 401 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)))) |
| 243 | 31 | peano2zd 9451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℤ) |
| 244 | 243 | zred 9448 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ) |
| 245 | 244 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) →
((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈
ℝ) |
| 246 | 16 | nnred 9003 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑄 ∈ ℝ) |
| 247 | 246 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℝ) |
| 248 | | nnre 8997 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
| 249 | 248 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ) |
| 250 | | lesub 8468 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(((⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))) + 1) ≤ (𝑄 − 𝑦) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))) |
| 251 | 245, 247,
249, 250 | syl3anc 1249 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) →
(((⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))) + 1) ≤ (𝑄 − 𝑦) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))) |
| 252 | 246 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℝ) |
| 253 | 252 | recnd 8055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℂ) |
| 254 | 75, 253 | mulcomd 8048 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 · 𝑄) = (𝑄 · 𝑃)) |
| 255 | 77, 253 | mulcomd 8048 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) · 𝑄) = (𝑄 · (2 · 𝑢))) |
| 256 | 19 | nnap0d 9036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 # 0) |
| 257 | 253, 75, 256 | divcanap1d 8818 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · 𝑃) = 𝑄) |
| 258 | 257 | oveq1d 5937 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · 𝑃) · (2 · 𝑢)) = (𝑄 · (2 · 𝑢))) |
| 259 | 246, 18 | nndivred 9040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → (𝑄 / 𝑃) ∈ ℝ) |
| 260 | 259 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℝ) |
| 261 | 260 | recnd 8055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℂ) |
| 262 | 261, 75, 77 | mul32d 8179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · 𝑃) · (2 · 𝑢)) = (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃)) |
| 263 | 255, 258,
262 | 3eqtr2d 2235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) · 𝑄) = (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃)) |
| 264 | 254, 263 | oveq12d 5940 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 · 𝑄) − ((2 · 𝑢) · 𝑄)) = ((𝑄 · 𝑃) − (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃))) |
| 265 | 75, 77, 253 | subdird 8441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑃 · 𝑄) − ((2 · 𝑢) · 𝑄))) |
| 266 | 26 | zred 9448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℝ) |
| 267 | 260, 266 | remulcld 8057 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) |
| 268 | 267 | recnd 8055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℂ) |
| 269 | 253, 268,
75 | subdird 8441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃) = ((𝑄 · 𝑃) − (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃))) |
| 270 | 264, 265,
269 | 3eqtr4d 2239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)) |
| 271 | 270 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)) |
| 272 | 271 | breq2d 4045 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))) |
| 273 | 267 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) |
| 274 | 247, 273 | resubcld 8407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ) |
| 275 | 19 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℕ) |
| 276 | 275 | nnred 9003 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ) |
| 277 | 275 | nngt0d 9034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 0 < 𝑃) |
| 278 | | ltmul1 8619 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))) |
| 279 | 249, 274,
276, 277, 278 | syl112anc 1253 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))) |
| 280 | | ltsub13 8470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦))) |
| 281 | 249, 247,
273, 280 | syl3anc 1249 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦))) |
| 282 | 272, 279,
281 | 3bitr2d 216 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦))) |
| 283 | 16 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℕ) |
| 284 | 283 | nnzd 9447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℤ) |
| 285 | | nnz 9345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
| 286 | | zsubcl 9367 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑄 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑄 − 𝑦) ∈ ℤ) |
| 287 | 284, 285,
286 | syl2an 289 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑄 − 𝑦) ∈ ℤ) |
| 288 | | flqlt 10373 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℚ ∧ (𝑄 − 𝑦) ∈ ℤ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦) ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄 − 𝑦))) |
| 289 | 30, 287, 288 | syl2an2r 595 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦) ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄 − 𝑦))) |
| 290 | | zltp1le 9380 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((⌊‘((𝑄
/ 𝑃) · (2 ·
𝑢))) ∈ ℤ ∧
(𝑄 − 𝑦) ∈ ℤ) →
((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄 − 𝑦) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄 − 𝑦))) |
| 291 | 31, 287, 290 | syl2an2r 595 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) →
((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄 − 𝑦) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄 − 𝑦))) |
| 292 | 282, 289,
291 | 3bitrd 214 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄 − 𝑦))) |
| 293 | 35 | oveq2i 5933 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (2
· 𝑁) = (2 ·
((𝑄 − 1) /
2)) |
| 294 | | peano2rem 8293 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑄 ∈ ℝ → (𝑄 − 1) ∈
ℝ) |
| 295 | 252, 294 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) ∈ ℝ) |
| 296 | 295 | recnd 8055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) ∈ ℂ) |
| 297 | | 2cnd 9063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℂ) |
| 298 | 85 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 # 0) |
| 299 | 296, 297,
298 | divcanap2d 8819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · ((𝑄 − 1) / 2)) = (𝑄 − 1)) |
| 300 | 293, 299 | eqtrid 2241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) = (𝑄 − 1)) |
| 301 | 300 | oveq1d 5937 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = ((𝑄 − 1) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 302 | | 1cnd 8042 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 1 ∈ ℂ) |
| 303 | 31 | zcnd 9449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ) |
| 304 | 253, 302,
303 | sub32d 8369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = ((𝑄 − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) − 1)) |
| 305 | 253, 303,
302 | subsub4d 8368 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) − 1) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))) |
| 306 | 301, 304,
305 | 3eqtrd 2233 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))) |
| 307 | 306 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))) |
| 308 | 307 | breq2d 4045 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))) |
| 309 | 251, 292,
308 | 3bitr4d 220 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 310 | 309 | anbi2d 464 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ≤ 𝑁 ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 311 | 15, 35 | gausslemma2dlem0b 15291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 312 | | nnmulcl 9011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((2
∈ ℕ ∧ 𝑁
∈ ℕ) → (2 · 𝑁) ∈ ℕ) |
| 313 | 9, 311, 312 | sylancr 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (2 · 𝑁) ∈
ℕ) |
| 314 | 313 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℕ) |
| 315 | 314 | nnred 9003 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℝ) |
| 316 | 311 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℕ) |
| 317 | 316 | nnred 9003 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℝ) |
| 318 | 31 | zred 9448 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ) |
| 319 | 311 | nncnd 9004 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 320 | 319 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℂ) |
| 321 | 320 | 2timesd 9234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) = (𝑁 + 𝑁)) |
| 322 | 320, 320,
321 | mvrladdd 8393 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) = 𝑁) |
| 323 | 252 | rehalfcld 9238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ∈ ℝ) |
| 324 | 252 | ltm1d 8959 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) < 𝑄) |
| 325 | 159 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℝ) |
| 326 | 161 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 2) |
| 327 | | ltdiv1 8895 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑄 − 1) ∈ ℝ ∧
𝑄 ∈ ℝ ∧ (2
∈ ℝ ∧ 0 < 2)) → ((𝑄 − 1) < 𝑄 ↔ ((𝑄 − 1) / 2) < (𝑄 / 2))) |
| 328 | 295, 252,
325, 326, 327 | syl112anc 1253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) < 𝑄 ↔ ((𝑄 − 1) / 2) < (𝑄 / 2))) |
| 329 | 324, 328 | mpbid 147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) / 2) < (𝑄 / 2)) |
| 330 | 35, 329 | eqbrtrid 4068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 < (𝑄 / 2)) |
| 331 | 317, 323,
330 | ltled 8145 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ (𝑄 / 2)) |
| 332 | 253, 297,
75, 298 | div32apd 8841 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 2) · 𝑃) = (𝑄 · (𝑃 / 2))) |
| 333 | 141 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℝ) |
| 334 | 333 | rehalfcld 9238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) ∈ ℝ) |
| 335 | 13 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ∈ ℤ) |
| 336 | 335 | zred 9448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ∈ ℝ) |
| 337 | 24 | zred 9448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℝ) |
| 338 | 11 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) ∈ ℚ) |
| 339 | | flqltp1 10369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑀 / 2) ∈ ℚ →
(𝑀 / 2) <
((⌊‘(𝑀 / 2)) +
1)) |
| 340 | 338, 339 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) < ((⌊‘(𝑀 / 2)) + 1)) |
| 341 | | elfzle1 10102 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → ((⌊‘(𝑀 / 2)) + 1) ≤ 𝑢) |
| 342 | 341 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ≤ 𝑢) |
| 343 | 334, 336,
337, 340, 342 | ltletrd 8450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) < 𝑢) |
| 344 | | ltdivmul 8903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑀 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → ((𝑀 / 2) < 𝑢 ↔ 𝑀 < (2 · 𝑢))) |
| 345 | 333, 337,
325, 326, 344 | syl112anc 1253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 / 2) < 𝑢 ↔ 𝑀 < (2 · 𝑢))) |
| 346 | 343, 345 | mpbid 147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 < (2 · 𝑢)) |
| 347 | 6, 346 | eqbrtrrid 4069 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) / 2) < (2 · 𝑢)) |
| 348 | 19 | nnred 9003 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℝ) |
| 349 | | peano2rem 8293 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈
ℝ) |
| 350 | 348, 349 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℝ) |
| 351 | | ltdivmul 8903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑃 − 1) ∈ ℝ ∧
(2 · 𝑢) ∈
ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝑃 − 1) / 2) < (2 · 𝑢) ↔ (𝑃 − 1) < (2 · (2 ·
𝑢)))) |
| 352 | 350, 266,
325, 326, 351 | syl112anc 1253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑃 − 1) / 2) < (2 · 𝑢) ↔ (𝑃 − 1) < (2 · (2 ·
𝑢)))) |
| 353 | 347, 352 | mpbid 147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) < (2 · (2 ·
𝑢))) |
| 354 | | zmulcl 9379 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((2
∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → (2 · (2
· 𝑢)) ∈
ℤ) |
| 355 | 22, 26, 354 | sylancr 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · (2 · 𝑢)) ∈
ℤ) |
| 356 | | zlem1lt 9382 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑃 ∈ ℤ ∧ (2
· (2 · 𝑢))
∈ ℤ) → (𝑃
≤ (2 · (2 · 𝑢)) ↔ (𝑃 − 1) < (2 · (2 ·
𝑢)))) |
| 357 | 211, 355,
356 | syl2an2r 595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 ≤ (2 · (2 · 𝑢)) ↔ (𝑃 − 1) < (2 · (2 ·
𝑢)))) |
| 358 | 353, 357 | mpbird 167 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ≤ (2 · (2 · 𝑢))) |
| 359 | | ledivmul 8904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑃 ∈ ℝ ∧ (2
· 𝑢) ∈ ℝ
∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ 𝑃 ≤ (2 · (2 · 𝑢)))) |
| 360 | 348, 266,
325, 326, 359 | syl112anc 1253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ 𝑃 ≤ (2 · (2 · 𝑢)))) |
| 361 | 358, 360 | mpbird 167 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 / 2) ≤ (2 · 𝑢)) |
| 362 | 348 | rehalfcld 9238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 / 2) ∈ ℝ) |
| 363 | 283 | nngt0d 9034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 𝑄) |
| 364 | | lemul2 8884 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑃 / 2) ∈ ℝ ∧ (2
· 𝑢) ∈ ℝ
∧ (𝑄 ∈ ℝ
∧ 0 < 𝑄)) →
((𝑃 / 2) ≤ (2 ·
𝑢) ↔ (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢)))) |
| 365 | 362, 266,
252, 363, 364 | syl112anc 1253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢)))) |
| 366 | 361, 365 | mpbid 147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢))) |
| 367 | 332, 366 | eqbrtrd 4055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢))) |
| 368 | 252, 266 | remulcld 8057 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (2 · 𝑢)) ∈ ℝ) |
| 369 | 19 | nngt0d 9034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 𝑃) |
| 370 | | lemuldiv 8908 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑄 / 2) ∈ ℝ ∧
(𝑄 · (2 ·
𝑢)) ∈ ℝ ∧
(𝑃 ∈ ℝ ∧ 0
< 𝑃)) → (((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))) |
| 371 | 323, 368,
348, 369, 370 | syl112anc 1253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))) |
| 372 | 367, 371 | mpbid 147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)) |
| 373 | 253, 77, 75, 256 | div23apd 8855 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 · (2 · 𝑢)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑢))) |
| 374 | 372, 373 | breqtrd 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ≤ ((𝑄 / 𝑃) · (2 · 𝑢))) |
| 375 | 317, 323,
267, 331, 374 | letrd 8150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))) |
| 376 | 311 | nnzd 9447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 377 | 376 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℤ) |
| 378 | | flqge 10372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℚ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 379 | 30, 377, 378 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 380 | 375, 379 | mpbid 147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) |
| 381 | 322, 380 | eqbrtrd 4055 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) |
| 382 | 315, 317,
318, 381 | subled 8575 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) |
| 383 | 382 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) |
| 384 | 314 | nnzd 9447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℤ) |
| 385 | 384, 31 | zsubcld 9453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ) |
| 386 | 385 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ) |
| 387 | 386 | zred 9448 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℝ) |
| 388 | 311 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ) |
| 389 | 388 | nnred 9003 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℝ) |
| 390 | | letr 8109 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ ((2
· 𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) → 𝑦 ≤ 𝑁)) |
| 391 | 249, 387,
389, 390 | syl3anc 1249 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) → 𝑦 ≤ 𝑁)) |
| 392 | 383, 391 | mpan2d 428 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → 𝑦 ≤ 𝑁)) |
| 393 | 392 | pm4.71rd 394 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ≤ 𝑁 ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 394 | 310, 393 | bitr4d 191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 395 | 394 | pm5.32da 452 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 396 | 395 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 397 | 242, 396 | bitrid 192 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 398 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑥 = (𝑃 − (2 · 𝑢))) |
| 399 | 211 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ) |
| 400 | 399, 26 | zsubcld 9453 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ) |
| 401 | | elfzle2 10103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → 𝑢 ≤ 𝑀) |
| 402 | 401 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ≤ 𝑀) |
| 403 | 402, 6 | breqtrdi 4074 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ≤ ((𝑃 − 1) / 2)) |
| 404 | | lemuldiv2 8909 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑢 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧
(2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑢) ≤ (𝑃 − 1) ↔ 𝑢 ≤ ((𝑃 − 1) / 2))) |
| 405 | 337, 350,
325, 326, 404 | syl112anc 1253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) ≤ (𝑃 − 1) ↔ 𝑢 ≤ ((𝑃 − 1) / 2))) |
| 406 | 403, 405 | mpbird 167 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ≤ (𝑃 − 1)) |
| 407 | 348 | ltm1d 8959 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) < 𝑃) |
| 408 | 266, 350,
348, 406, 407 | lelttrd 8151 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) < 𝑃) |
| 409 | 266, 348 | posdifd 8559 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) < 𝑃 ↔ 0 < (𝑃 − (2 · 𝑢)))) |
| 410 | 408, 409 | mpbid 147 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < (𝑃 − (2 · 𝑢))) |
| 411 | | elnnz 9336 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑃 − (2 · 𝑢)) ∈ ℕ ↔ ((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ 0 <
(𝑃 − (2 ·
𝑢)))) |
| 412 | 400, 410,
411 | sylanbrc 417 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℕ) |
| 413 | 75, 77, 302 | sub32d 8369 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) − 1) = ((𝑃 − 1) − (2 · 𝑢))) |
| 414 | 6, 6 | oveq12i 5934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑀 + 𝑀) = (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) |
| 415 | 64, 213 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℤ) |
| 416 | 415 | zcnd 9449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℂ) |
| 417 | 416 | 2halvesd 9237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1)) |
| 418 | 414, 417 | eqtrid 2241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 + 𝑀) = (𝑃 − 1)) |
| 419 | 418 | oveq1d 5937 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 + 𝑀) − 𝑀) = ((𝑃 − 1) − 𝑀)) |
| 420 | 167 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℂ) |
| 421 | 420, 420 | pncan2d 8339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 + 𝑀) − 𝑀) = 𝑀) |
| 422 | 419, 421 | eqtr3d 2231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − 𝑀) = 𝑀) |
| 423 | 422, 346 | eqbrtrd 4055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − 𝑀) < (2 · 𝑢)) |
| 424 | 350, 333,
266, 423 | ltsub23d 8577 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − (2 · 𝑢)) < 𝑀) |
| 425 | 413, 424 | eqbrtrd 4055 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) − 1) < 𝑀) |
| 426 | 7 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℕ) |
| 427 | 426 | nnzd 9447 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℤ) |
| 428 | | zlem1lt 9382 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑃 − (2 · 𝑢)) ≤ 𝑀 ↔ ((𝑃 − (2 · 𝑢)) − 1) < 𝑀)) |
| 429 | 400, 427,
428 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) ≤ 𝑀 ↔ ((𝑃 − (2 · 𝑢)) − 1) < 𝑀)) |
| 430 | 425, 429 | mpbird 167 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ≤ 𝑀) |
| 431 | | fznn 10164 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀 ∈ ℤ → ((𝑃 − (2 · 𝑢)) ∈ (1...𝑀) ↔ ((𝑃 − (2 · 𝑢)) ∈ ℕ ∧ (𝑃 − (2 · 𝑢)) ≤ 𝑀))) |
| 432 | 427, 431 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) ∈ (1...𝑀) ↔ ((𝑃 − (2 · 𝑢)) ∈ ℕ ∧ (𝑃 − (2 · 𝑢)) ≤ 𝑀))) |
| 433 | 412, 430,
432 | mpbir2and 946 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ (1...𝑀)) |
| 434 | 433 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑃 − (2 · 𝑢)) ∈ (1...𝑀)) |
| 435 | 398, 434 | eqeltrd 2273 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑥 ∈ (1...𝑀)) |
| 436 | 435 | biantrurd 305 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...𝑁) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)))) |
| 437 | 376 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑁 ∈ ℤ) |
| 438 | | fznn 10164 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℤ → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁))) |
| 439 | 437, 438 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁))) |
| 440 | 436, 439 | bitr3d 190 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁))) |
| 441 | 398 | oveq1d 5937 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑥 · 𝑄) = ((𝑃 − (2 · 𝑢)) · 𝑄)) |
| 442 | 441 | breq2d 4045 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑦 · 𝑃) < (𝑥 · 𝑄) ↔ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) |
| 443 | 440, 442 | anbi12d 473 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ ((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)))) |
| 444 | 385 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ) |
| 445 | | fznn 10164 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((2
· 𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ →
(𝑦 ∈ (1...((2 ·
𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 446 | 444, 445 | syl 14 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 447 | 397, 443,
446 | 3bitr4d 220 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 448 | 241, 447 | bitrid 192 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (〈𝑥, 𝑦〉 ∈ 𝑆 ↔ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 449 | 448 | pm5.32da 452 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑥 = (𝑃 − (2 · 𝑢)) ∧ 〈𝑥, 𝑦〉 ∈ 𝑆) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))) |
| 450 | | vex 2766 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑥 ∈ V |
| 451 | | vex 2766 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑦 ∈ V |
| 452 | 450, 451 | op1std 6206 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) |
| 453 | 452 | eqeq1d 2205 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((1st ‘𝑧) = (𝑃 − (2 · 𝑢)) ↔ 𝑥 = (𝑃 − (2 · 𝑢)))) |
| 454 | 453 | elrab 2920 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ↔ (〈𝑥, 𝑦〉 ∈ 𝑆 ∧ 𝑥 = (𝑃 − (2 · 𝑢)))) |
| 455 | 454 | biancomi 270 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 〈𝑥, 𝑦〉 ∈ 𝑆)) |
| 456 | | opelxp 4693 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 ·
𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 ∈ {(𝑃 − (2 · 𝑢))} ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 457 | | velsn 3639 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ {(𝑃 − (2 · 𝑢))} ↔ 𝑥 = (𝑃 − (2 · 𝑢))) |
| 458 | 457 | anbi1i 458 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ {(𝑃 − (2 · 𝑢))} ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 459 | 456, 458 | bitri 184 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 ·
𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 460 | 449, 455,
459 | 3bitr4g 223 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (〈𝑥, 𝑦〉 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ↔ 〈𝑥, 𝑦〉 ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))) |
| 461 | 237, 238,
460 | eqrelrdv 4759 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} = ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 462 | 461 | fveq2d 5562 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘{𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = (♯‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))) |
| 463 | | 1zzd 9353 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 1 ∈ ℤ) |
| 464 | 463, 385 | fzfigd 10523 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin) |
| 465 | | xpsnen2g 6888 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ (1...((2
· 𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin) →
({(𝑃 − (2 ·
𝑢))} × (1...((2
· 𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 ·
𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 466 | 400, 464,
465 | syl2anc 411 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 467 | 461, 69 | eqeltrrd 2274 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ∈ Fin) |
| 468 | | hashen 10876 |
. . . . . . . . . . . . . 14
⊢
((({(𝑃 − (2
· 𝑢))} ×
(1...((2 · 𝑁)
− (⌊‘((𝑄
/ 𝑃) · (2 ·
𝑢)))))) ∈ Fin ∧
(1...((2 · 𝑁)
− (⌊‘((𝑄
/ 𝑃) · (2 ·
𝑢))))) ∈ Fin) →
((♯‘({(𝑃
− (2 · 𝑢))}
× (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) = (♯‘(1...((2 ·
𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ ({(𝑃 − (2 · 𝑢))} × (1...((2 ·
𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 ·
𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 469 | 467, 464,
468 | syl2anc 411 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((♯‘({(𝑃 − (2 · 𝑢))} × (1...((2 ·
𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) =
(♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 470 | 466, 469 | mpbird 167 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘({(𝑃 − (2 · 𝑢))} × (1...((2 ·
𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) =
(♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
| 471 | | ltmul2 8883 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((2
· 𝑢) ∈ ℝ
∧ 𝑃 ∈ ℝ
∧ (𝑄 ∈ ℝ
∧ 0 < 𝑄)) → ((2
· 𝑢) < 𝑃 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃))) |
| 472 | 266, 348,
252, 363, 471 | syl112anc 1253 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) < 𝑃 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃))) |
| 473 | 408, 472 | mpbid 147 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)) |
| 474 | | ltdivmul2 8905 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑄 · (2 · 𝑢)) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 <
𝑃)) → (((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃))) |
| 475 | 368, 252,
348, 369, 474 | syl112anc 1253 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃))) |
| 476 | 473, 475 | mpbird 167 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄) |
| 477 | 373, 476 | eqbrtrrd 4057 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄) |
| 478 | | flqlt 10373 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℚ ∧ 𝑄 ∈ ℤ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄)) |
| 479 | 30, 284, 478 | syl2anc 411 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄)) |
| 480 | 477, 479 | mpbid 147 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄) |
| 481 | | zltlem1 9383 |
. . . . . . . . . . . . . . . . 17
⊢
(((⌊‘((𝑄
/ 𝑃) · (2 ·
𝑢))) ∈ ℤ ∧
𝑄 ∈ ℤ) →
((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1))) |
| 482 | 31, 284, 481 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1))) |
| 483 | 480, 482 | mpbid 147 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1)) |
| 484 | 483, 300 | breqtrrd 4061 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (2 · 𝑁)) |
| 485 | | eluz2 9607 |
. . . . . . . . . . . . . 14
⊢ ((2
· 𝑁) ∈
(ℤ≥‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (2 · 𝑁) ∈ ℤ ∧
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (2 · 𝑁))) |
| 486 | 31, 384, 484, 485 | syl3anbrc 1183 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈
(ℤ≥‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 487 | | uznn0sub 9633 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑁) ∈
(ℤ≥‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈
ℕ0) |
| 488 | | hashfz1 10875 |
. . . . . . . . . . . . 13
⊢ (((2
· 𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℕ0
→ (♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 489 | 486, 487,
488 | 3syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘(1...((2 ·
𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 490 | 462, 470,
489 | 3eqtrd 2233 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘{𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 491 | 490 | sumeq2dv 11533 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(♯‘{𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 492 | 92, 233, 491 | 3eqtr3rd 2238 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) |
| 493 | 313 | nncnd 9004 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · 𝑁) ∈
ℂ) |
| 494 | 493 | adantr 276 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℂ) |
| 495 | 14, 494, 303 | fsumsub 11617 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 496 | 492, 495 | eqtr3d 2231 |
. . . . . . . 8
⊢ (𝜑 → (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
| 497 | 496 | oveq2d 5938 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) =
(Σ𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
| 498 | 32 | zcnd 9449 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ) |
| 499 | 14, 384 | fsumzcl 11567 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) ∈ ℤ) |
| 500 | 499 | zcnd 9449 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) ∈ ℂ) |
| 501 | 498, 500 | pncan3d 8340 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁)) |
| 502 | | fsumconst 11619 |
. . . . . . . . 9
⊢
(((((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin ∧ (2 · 𝑁) ∈ ℂ) →
Σ𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(2 · 𝑁) =
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁))) |
| 503 | 14, 493, 502 | syl2anc 411 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁))) |
| 504 | | hashcl 10873 |
. . . . . . . . . . 11
⊢
((((⌊‘(𝑀
/ 2)) + 1)...𝑀) ∈ Fin
→ (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈
ℕ0) |
| 505 | 14, 504 | syl 14 |
. . . . . . . . . 10
⊢ (𝜑 →
(♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈
ℕ0) |
| 506 | 505 | nn0cnd 9304 |
. . . . . . . . 9
⊢ (𝜑 →
(♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℂ) |
| 507 | | 2cnd 9063 |
. . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℂ) |
| 508 | 506, 507,
319 | mul12d 8178 |
. . . . . . . 8
⊢ (𝜑 →
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)) = (2 ·
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) |
| 509 | 503, 508 | eqtrd 2229 |
. . . . . . 7
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = (2 ·
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) |
| 510 | 497, 501,
509 | 3eqtrd 2233 |
. . . . . 6
⊢ (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) = (2 ·
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) |
| 511 | 510 | oveq2d 5938 |
. . . . 5
⊢ (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) = (-1↑(2
· ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))) |
| 512 | 22 | a1i 9 |
. . . . . 6
⊢ (𝜑 → 2 ∈
ℤ) |
| 513 | 505 | nn0zd 9446 |
. . . . . . 7
⊢ (𝜑 →
(♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℤ) |
| 514 | 513, 376 | zmulcld 9454 |
. . . . . 6
⊢ (𝜑 →
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ) |
| 515 | | expmulzap 10677 |
. . . . . 6
⊢ (((-1
∈ ℂ ∧ -1 # 0) ∧ (2 ∈ ℤ ∧
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ)) → (-1↑(2
· ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) =
((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) |
| 516 | 2, 4, 512, 514, 515 | syl22anc 1250 |
. . . . 5
⊢ (𝜑 → (-1↑(2 ·
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) =
((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) |
| 517 | | neg1sqe1 10726 |
. . . . . . 7
⊢
(-1↑2) = 1 |
| 518 | 517 | oveq1i 5932 |
. . . . . 6
⊢
((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) =
(1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) |
| 519 | | 1exp 10660 |
. . . . . . 7
⊢
(((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ →
(1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1) |
| 520 | 514, 519 | syl 14 |
. . . . . 6
⊢ (𝜑 →
(1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1) |
| 521 | 518, 520 | eqtrid 2241 |
. . . . 5
⊢ (𝜑 →
((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1) |
| 522 | 511, 516,
521 | 3eqtrd 2233 |
. . . 4
⊢ (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) =
1) |
| 523 | 44, 55, 522 | 3eqtr4d 2239 |
. . 3
⊢ (𝜑 →
((-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) =
(-1↑(Σ𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})))) |
| 524 | | expaddzap 10675 |
. . . 4
⊢ (((-1
∈ ℂ ∧ -1 # 0) ∧ (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧
(♯‘{𝑧 ∈
𝑆 ∣ ¬ 2 ∥
(1st ‘𝑧)})
∈ ℤ)) → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) =
((-1↑Σ𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})))) |
| 525 | 2, 4, 32, 42, 524 | syl22anc 1250 |
. . 3
⊢ (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) =
((-1↑Σ𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})))) |
| 526 | 523, 525 | eqtr2d 2230 |
. 2
⊢ (𝜑 → ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) =
((-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})))) |
| 527 | 33, 41, 41, 43, 526 | mulcanap2ad 8691 |
1
⊢ (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) |