Step | Hyp | Ref
| Expression |
1 | | neg1cn 12087 |
. . . 4
⊢ -1 ∈
ℂ |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → -1 ∈
ℂ) |
3 | | neg1ne0 12089 |
. . . 4
⊢ -1 ≠
0 |
4 | 3 | a1i 11 |
. . 3
⊢ (𝜑 → -1 ≠
0) |
5 | | fzfid 13693 |
. . . 4
⊢ (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin) |
6 | | lgseisen.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄 ∈ (ℙ ∖
{2})) |
7 | 6 | gausslemma2dlem0a 26504 |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 ∈ ℕ) |
8 | 7 | nnred 11988 |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ ℝ) |
9 | | lgseisen.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
10 | 9 | gausslemma2dlem0a 26504 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℕ) |
11 | 8, 10 | nndivred 12027 |
. . . . . . 7
⊢ (𝜑 → (𝑄 / 𝑃) ∈ ℝ) |
12 | 11 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℝ) |
13 | | 2z 12352 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
14 | | elfzelz 13256 |
. . . . . . . . 9
⊢ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → 𝑢 ∈ ℤ) |
15 | 14 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℤ) |
16 | | zmulcl 12369 |
. . . . . . . 8
⊢ ((2
∈ ℤ ∧ 𝑢
∈ ℤ) → (2 · 𝑢) ∈ ℤ) |
17 | 13, 15, 16 | sylancr 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℤ) |
18 | 17 | zred 12426 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℝ) |
19 | 12, 18 | remulcld 11005 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) |
20 | 19 | flcld 13518 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ) |
21 | 5, 20 | fsumzcl 15447 |
. . 3
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ) |
22 | 2, 4, 21 | expclzd 13869 |
. 2
⊢ (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℂ) |
23 | | fzfid 13693 |
. . . . . . 7
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
24 | | fzfid 13693 |
. . . . . . 7
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
25 | | xpfi 9085 |
. . . . . . 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 5679 |
. . . . . . 7
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁)) |
29 | 27, 28 | eqsstri 3955 |
. . . . . 6
⊢ 𝑆 ⊆ ((1...𝑀) × (1...𝑁)) |
30 | | ssfi 8956 |
. . . . . 6
⊢
((((1...𝑀) ×
(1...𝑁)) ∈ Fin ∧
𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin) |
31 | 26, 29, 30 | sylancl 586 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ Fin) |
32 | | ssrab2 4013 |
. . . . 5
⊢ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ⊆ 𝑆 |
33 | | ssfi 8956 |
. . . . 5
⊢ ((𝑆 ∈ Fin ∧ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ⊆ 𝑆) → {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
34 | 31, 32, 33 | sylancl 586 |
. . . 4
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈
Fin) |
35 | | hashcl 14071 |
. . . 4
⊢ ({𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)} ∈ Fin
→ (♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)}) ∈
ℕ0) |
36 | 34, 35 | syl 17 |
. . 3
⊢ (𝜑 → (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) ∈
ℕ0) |
37 | | expcl 13800 |
. . 3
⊢ ((-1
∈ ℂ ∧ (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) ∈
ℕ0) → (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) ∈
ℂ) |
38 | 1, 36, 37 | sylancr 587 |
. 2
⊢ (𝜑 →
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) ∈ ℂ) |
39 | 36 | nn0zd 12424 |
. . 3
⊢ (𝜑 → (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) ∈
ℤ) |
40 | 2, 4, 39 | expne0d 13870 |
. 2
⊢ (𝜑 →
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) ≠ 0) |
41 | 38, 40 | recidd 11746 |
. . . 4
⊢ (𝜑 →
((-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) · (1 /
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})))) = 1) |
42 | | 1div1e1 11665 |
. . . . . . . . 9
⊢ (1 / 1) =
1 |
43 | 42 | negeqi 11214 |
. . . . . . . 8
⊢ -(1 / 1)
= -1 |
44 | | ax-1cn 10929 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
45 | | ax-1ne0 10940 |
. . . . . . . . 9
⊢ 1 ≠
0 |
46 | | divneg2 11699 |
. . . . . . . . 9
⊢ ((1
∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → -(1 / 1) = (1 /
-1)) |
47 | 44, 44, 45, 46 | mp3an 1460 |
. . . . . . . 8
⊢ -(1 / 1)
= (1 / -1) |
48 | 43, 47 | eqtr3i 2768 |
. . . . . . 7
⊢ -1 = (1 /
-1) |
49 | 48 | oveq1i 7285 |
. . . . . 6
⊢
(-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) = ((1 /
-1)↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) |
50 | 2, 4, 39 | exprecd 13872 |
. . . . . 6
⊢ (𝜑 → ((1 /
-1)↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) = (1 / (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})))) |
51 | 49, 50 | eqtrid 2790 |
. . . . 5
⊢ (𝜑 →
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) = (1 / (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})))) |
52 | 51 | oveq2d 7291 |
. . . 4
⊢ (𝜑 →
((-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) =
((-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) · (1 /
(-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)}))))) |
53 | 31 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑆 ∈ Fin) |
54 | | ssrab2 4013 |
. . . . . . . . . . . 12
⊢ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆 |
55 | | ssfi 8956 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Fin ∧ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆) → {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ∈ Fin) |
56 | 53, 54, 55 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ∈ Fin) |
57 | | fveqeq2 6783 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑣 → ((1st ‘𝑧) = (𝑃 − (2 · 𝑢)) ↔ (1st ‘𝑣) = (𝑃 − (2 · 𝑢)))) |
58 | 57 | elrab 3624 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ↔ (𝑣 ∈ 𝑆 ∧ (1st ‘𝑣) = (𝑃 − (2 · 𝑢)))) |
59 | 58 | simprbi 497 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} → (1st ‘𝑣) = (𝑃 − (2 · 𝑢))) |
60 | 59 | ad2antll 726 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (1st ‘𝑣) = (𝑃 − (2 · 𝑢))) |
61 | 60 | oveq2d 7291 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (1st ‘𝑣)) = (𝑃 − (𝑃 − (2 · 𝑢)))) |
62 | 10 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℕ) |
63 | 62 | nncnd 11989 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℂ) |
64 | 63 | adantrr 714 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → 𝑃 ∈ ℂ) |
65 | 17 | zcnd 12427 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℂ) |
66 | 65 | adantrr 714 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (2 · 𝑢) ∈ ℂ) |
67 | 64, 66 | nncand 11337 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (𝑃 − (2 · 𝑢))) = (2 · 𝑢)) |
68 | 61, 67 | eqtrd 2778 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (1st ‘𝑣)) = (2 · 𝑢)) |
69 | 68 | oveq1d 7290 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → ((𝑃 − (1st ‘𝑣)) / 2) = ((2 · 𝑢) / 2)) |
70 | 15 | zcnd 12427 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℂ) |
71 | 70 | adantrr 714 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → 𝑢 ∈ ℂ) |
72 | | 2cnd 12051 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → 2 ∈
ℂ) |
73 | | 2ne0 12077 |
. . . . . . . . . . . . . . . 16
⊢ 2 ≠
0 |
74 | 73 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → 2 ≠ 0) |
75 | 71, 72, 74 | divcan3d 11756 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → ((2 · 𝑢) / 2) = 𝑢) |
76 | 69, 75 | eqtrd 2778 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → ((𝑃 − (1st ‘𝑣)) / 2) = 𝑢) |
77 | 76 | ralrimivva 3123 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)∀𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ((𝑃 − (1st ‘𝑣)) / 2) = 𝑢) |
78 | | invdisj 5058 |
. . . . . . . . . . . 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 15534 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘∪ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(♯‘{𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) |
81 | | iunrab 4982 |
. . . . . . . . . . . 12
⊢ ∪ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧 ∈ 𝑆 ∣ ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st ‘𝑧) = (𝑃 − (2 · 𝑢))} |
82 | | eldifsni 4723 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ≠
2) |
83 | 9, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑃 ≠ 2) |
84 | 83 | necomd 2999 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 2 ≠ 𝑃) |
85 | 84 | neneqd 2948 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ¬ 2 = 𝑃) |
86 | 85 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 = 𝑃) |
87 | | uzid 12597 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
88 | 13, 87 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
(ℤ≥‘2) |
89 | 9 | eldifad 3899 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑃 ∈ ℙ) |
90 | 89 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℙ) |
91 | | dvdsprm 16408 |
. . . . . . . . . . . . . . . . . . . 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 723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℕ) |
95 | 94 | nncnd 11989 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℂ) |
96 | 17 | adantlr 712 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℤ) |
97 | 96 | zcnd 12427 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℂ) |
98 | 95, 97 | npcand 11336 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)) = 𝑃) |
99 | 98 | breq2d 5086 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)) ↔ 2 ∥ 𝑃)) |
100 | 93, 99 | mtbird 325 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))) |
101 | 14 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℤ) |
102 | | dvdsmul1 15987 |
. . . . . . . . . . . . . . . . . . 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 12425 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ) |
106 | 105, 96 | zsubcld 12431 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ) |
107 | | dvds2add 15999 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℤ ∧ (𝑃
− (2 · 𝑢))
∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → ((2 ∥ (𝑃 − (2 · 𝑢)) ∧ 2 ∥ (2 ·
𝑢)) → 2 ∥
((𝑃 − (2 ·
𝑢)) + (2 · 𝑢)))) |
108 | 104, 106,
96, 107 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 ∥ (𝑃 − (2 · 𝑢)) ∧ 2 ∥ (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)))) |
109 | 103, 108 | mpan2d 691 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ (𝑃 − (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)))) |
110 | 100, 109 | mtod 197 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ (𝑃 − (2 · 𝑢))) |
111 | | breq2 5078 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑧) = (𝑃 − (2 · 𝑢)) → (2 ∥ (1st
‘𝑧) ↔ 2 ∥
(𝑃 − (2 ·
𝑢)))) |
112 | 111 | notbid 318 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑧) = (𝑃 − (2 · 𝑢)) → (¬ 2 ∥ (1st
‘𝑧) ↔ ¬ 2
∥ (𝑃 − (2
· 𝑢)))) |
113 | 110, 112 | syl5ibrcom 246 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((1st ‘𝑧) = (𝑃 − (2 · 𝑢)) → ¬ 2 ∥ (1st
‘𝑧))) |
114 | 113 | rexlimdva 3213 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st ‘𝑧) = (𝑃 − (2 · 𝑢)) → ¬ 2 ∥ (1st
‘𝑧))) |
115 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆) |
116 | 29, 115 | sselid 3919 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ ((1...𝑀) × (1...𝑁))) |
117 | | xp1st 7863 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ((1...𝑀) × (1...𝑁)) → (1st ‘𝑧) ∈ (1...𝑀)) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (1st ‘𝑧) ∈ (1...𝑀)) |
119 | | elfzelz 13256 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑧) ∈ (1...𝑀) → (1st ‘𝑧) ∈
ℤ) |
120 | | odd2np1 16050 |
. . . . . . . . . . . . . . . 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 26505 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑀 ∈ ℕ) |
124 | 123 | nnred 11988 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑀 ∈ ℝ) |
125 | 124 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑀 ∈
ℝ) |
126 | 125 | rehalfcld 12220 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 / 2) ∈
ℝ) |
127 | 126 | flcld 13518 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
(⌊‘(𝑀 / 2))
∈ ℤ) |
128 | 127 | peano2zd 12429 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
((⌊‘(𝑀 / 2)) +
1) ∈ ℤ) |
129 | 123 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑀 ∈
ℕ) |
130 | 129 | nnzd 12425 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑀 ∈
ℤ) |
131 | | simprl 768 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑛 ∈
ℤ) |
132 | 130, 131 | zsubcld 12431 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 − 𝑛) ∈ ℤ) |
133 | | reflcl 13516 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 / 2) ∈ ℝ →
(⌊‘(𝑀 / 2))
∈ ℝ) |
134 | 126, 133 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
(⌊‘(𝑀 / 2))
∈ ℝ) |
135 | 132 | zred 12426 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 − 𝑛) ∈ ℝ) |
136 | | flle 13519 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 / 2) ∈ ℝ →
(⌊‘(𝑀 / 2))
≤ (𝑀 /
2)) |
137 | 126, 136 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
(⌊‘(𝑀 / 2))
≤ (𝑀 /
2)) |
138 | | zre 12323 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℝ) |
139 | 138 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑛 ∈
ℝ) |
140 | | simprr 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑛) + 1) =
(1st ‘𝑧)) |
141 | 118 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
(1st ‘𝑧)
∈ (1...𝑀)) |
142 | 140, 141 | eqeltrd 2839 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑛) + 1) ∈
(1...𝑀)) |
143 | | elfzle2 13260 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((2
· 𝑛) + 1) ∈
(1...𝑀) → ((2 ·
𝑛) + 1) ≤ 𝑀) |
144 | 142, 143 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑛) + 1) ≤ 𝑀) |
145 | | zmulcl 12369 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((2
∈ ℤ ∧ 𝑛
∈ ℤ) → (2 · 𝑛) ∈ ℤ) |
146 | 13, 131, 145 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· 𝑛) ∈
ℤ) |
147 | | zltp1le 12370 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((2
· 𝑛) ∈ ℤ
∧ 𝑀 ∈ ℤ)
→ ((2 · 𝑛) <
𝑀 ↔ ((2 · 𝑛) + 1) ≤ 𝑀)) |
148 | 146, 130,
147 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑛) < 𝑀 ↔ ((2 · 𝑛) + 1) ≤ 𝑀)) |
149 | 144, 148 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· 𝑛) < 𝑀) |
150 | | 2re 12047 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ∈
ℝ |
151 | 150 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 2 ∈
ℝ) |
152 | | 2pos 12076 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 <
2 |
153 | 152 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 0 <
2) |
154 | | ltmuldiv2 11849 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → ((2 · 𝑛) < 𝑀 ↔ 𝑛 < (𝑀 / 2))) |
155 | 139, 125,
151, 153, 154 | syl112anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑛) < 𝑀 ↔ 𝑛 < (𝑀 / 2))) |
156 | 149, 155 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑛 < (𝑀 / 2)) |
157 | 126 | recnd 11003 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 / 2) ∈
ℂ) |
158 | 123 | nncnd 11989 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑀 ∈ ℂ) |
159 | 158 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑀 ∈
ℂ) |
160 | 159 | 2halvesd 12219 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((𝑀 / 2) + (𝑀 / 2)) = 𝑀) |
161 | 157, 157,
160 | mvlraddd 11385 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 / 2) = (𝑀 − (𝑀 / 2))) |
162 | 156, 161 | breqtrd 5100 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑛 < (𝑀 − (𝑀 / 2))) |
163 | 139, 125,
126, 162 | ltsub13d 11581 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 / 2) < (𝑀 − 𝑛)) |
164 | 134, 126,
135, 137, 163 | lelttrd 11133 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
(⌊‘(𝑀 / 2))
< (𝑀 − 𝑛)) |
165 | | zltp1le 12370 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((⌊‘(𝑀
/ 2)) ∈ ℤ ∧ (𝑀 − 𝑛) ∈ ℤ) →
((⌊‘(𝑀 / 2))
< (𝑀 − 𝑛) ↔ ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀 − 𝑛))) |
166 | 127, 132,
165 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
((⌊‘(𝑀 / 2))
< (𝑀 − 𝑛) ↔ ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀 − 𝑛))) |
167 | 164, 166 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
((⌊‘(𝑀 / 2)) +
1) ≤ (𝑀 − 𝑛)) |
168 | | 2t0e0 12142 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
· 0) = 0 |
169 | | 2cn 12048 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ∈
ℂ |
170 | | zcn 12324 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
171 | 170 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑛 ∈
ℂ) |
172 | | mulcl 10955 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((2
∈ ℂ ∧ 𝑛
∈ ℂ) → (2 · 𝑛) ∈ ℂ) |
173 | 169, 171,
172 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· 𝑛) ∈
ℂ) |
174 | | pncan 11227 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((2
· 𝑛) ∈ ℂ
∧ 1 ∈ ℂ) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛)) |
175 | 173, 44, 174 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (((2
· 𝑛) + 1) − 1)
= (2 · 𝑛)) |
176 | | elfznn 13285 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((2
· 𝑛) + 1) ∈
(1...𝑀) → ((2 ·
𝑛) + 1) ∈
ℕ) |
177 | | nnm1nn0 12274 |
. . . . . . . . . . . . . . . . . . . . . . . 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 2840 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· 𝑛) ∈
ℕ0) |
180 | 179 | nn0ge0d 12296 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 0 ≤
(2 · 𝑛)) |
181 | 168, 180 | eqbrtrid 5109 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· 0) ≤ (2 · 𝑛)) |
182 | | 0red 10978 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 0 ∈
ℝ) |
183 | | lemul2 11828 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0
∈ ℝ ∧ 𝑛
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (0 ≤ 𝑛 ↔ (2 · 0) ≤ (2
· 𝑛))) |
184 | 182, 139,
151, 153, 183 | syl112anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (0 ≤
𝑛 ↔ (2 · 0)
≤ (2 · 𝑛))) |
185 | 181, 184 | mpbird 256 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 0 ≤
𝑛) |
186 | 125, 139 | subge02d 11567 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (0 ≤
𝑛 ↔ (𝑀 − 𝑛) ≤ 𝑀)) |
187 | 185, 186 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 − 𝑛) ≤ 𝑀) |
188 | 128, 130,
132, 167, 187 | elfzd 13247 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑀 − 𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) |
189 | 89 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑃 ∈
ℙ) |
190 | | prmnn 16379 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
191 | 189, 190 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑃 ∈
ℕ) |
192 | 191 | nncnd 11989 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑃 ∈
ℂ) |
193 | | peano2cn 11147 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
· 𝑛) ∈ ℂ
→ ((2 · 𝑛) + 1)
∈ ℂ) |
194 | 173, 193 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑛) + 1) ∈
ℂ) |
195 | 192, 194 | nncand 11337 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑃 − (𝑃 − ((2 · 𝑛) + 1))) = ((2 · 𝑛) + 1)) |
196 | | 1cnd 10970 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 1 ∈
ℂ) |
197 | 192, 173,
196 | sub32d 11364 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((𝑃 − (2 · 𝑛)) − 1) = ((𝑃 − 1) − (2 ·
𝑛))) |
198 | 192, 173,
196 | subsub4d 11363 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((𝑃 − (2 · 𝑛)) − 1) = (𝑃 − ((2 · 𝑛) + 1))) |
199 | | 2cnd 12051 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 2 ∈
ℂ) |
200 | 199, 159,
171 | subdid 11431 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· (𝑀 − 𝑛)) = ((2 · 𝑀) − (2 · 𝑛))) |
201 | 122 | oveq2i 7286 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2
· 𝑀) = (2 ·
((𝑃 − 1) /
2)) |
202 | 10 | nnzd 12425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝑃 ∈ ℤ) |
203 | 202 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 𝑃 ∈
ℤ) |
204 | | peano2zm 12363 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈
ℤ) |
205 | 203, 204 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑃 − 1) ∈
ℤ) |
206 | 205 | zcnd 12427 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑃 − 1) ∈
ℂ) |
207 | 73 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → 2 ≠
0) |
208 | 206, 199,
207 | divcan2d 11753 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· ((𝑃 − 1) /
2)) = (𝑃 −
1)) |
209 | 201, 208 | eqtrid 2790 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (2
· 𝑀) = (𝑃 − 1)) |
210 | 209 | oveq1d 7290 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((2
· 𝑀) − (2
· 𝑛)) = ((𝑃 − 1) − (2 ·
𝑛))) |
211 | 200, 210 | eqtr2d 2779 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → ((𝑃 − 1) − (2 ·
𝑛)) = (2 · (𝑀 − 𝑛))) |
212 | 197, 198,
211 | 3eqtr3d 2786 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑃 − ((2 · 𝑛) + 1)) = (2 · (𝑀 − 𝑛))) |
213 | 212 | oveq2d 7291 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) → (𝑃 − (𝑃 − ((2 · 𝑛) + 1))) = (𝑃 − (2 · (𝑀 − 𝑛)))) |
214 | 195, 213,
140 | 3eqtr3rd 2787 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st
‘𝑧))) →
(1st ‘𝑧) =
(𝑃 − (2 ·
(𝑀 − 𝑛)))) |
215 | | oveq2 7283 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = (𝑀 − 𝑛) → (2 · 𝑢) = (2 · (𝑀 − 𝑛))) |
216 | 215 | oveq2d 7291 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = (𝑀 − 𝑛) → (𝑃 − (2 · 𝑢)) = (𝑃 − (2 · (𝑀 − 𝑛)))) |
217 | 216 | rspceeqv 3575 |
. . . . . . . . . . . . . . . . 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 3214 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (1st
‘𝑧) →
∃𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(1st
‘𝑧) = (𝑃 − (2 · 𝑢)))) |
220 | 121, 219 | sylbid 239 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ 2 ∥ (1st
‘𝑧) →
∃𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(1st
‘𝑧) = (𝑃 − (2 · 𝑢)))) |
221 | 114, 220 | impbid 211 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st ‘𝑧) = (𝑃 − (2 · 𝑢)) ↔ ¬ 2 ∥ (1st
‘𝑧))) |
222 | 221 | rabbidva 3413 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st ‘𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) |
223 | 81, 222 | eqtrid 2790 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) |
224 | 223 | fveq2d 6778 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘∪ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) |
225 | 27 | relopabiv 5730 |
. . . . . . . . . . . . . . 15
⊢ Rel 𝑆 |
226 | | relss 5692 |
. . . . . . . . . . . . . . 15
⊢ ({𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆 → (Rel 𝑆 → Rel {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))})) |
227 | 54, 225, 226 | mp2 9 |
. . . . . . . . . . . . . 14
⊢ Rel
{𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} |
228 | | relxp 5607 |
. . . . . . . . . . . . . 14
⊢ Rel
({(𝑃 − (2 ·
𝑢))} × (1...((2
· 𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
229 | 27 | eleq2i 2830 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑥, 𝑦〉 ∈ 𝑆 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}) |
230 | | opabidw 5437 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) |
231 | 229, 230 | bitri 274 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑥, 𝑦〉 ∈ 𝑆 ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) |
232 | | anass 469 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)))) |
233 | 20 | peano2zd 12429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℤ) |
234 | 233 | zred 12426 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ) |
235 | 234 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) →
((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈
ℝ) |
236 | 8 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℝ) |
237 | | nnre 11980 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
238 | 237 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ) |
239 | | lesub 11454 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(((⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))) + 1) ≤ (𝑄 − 𝑦) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))) |
240 | 235, 236,
238, 239 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) →
(((⌊‘((𝑄 /
𝑃) · (2 ·
𝑢))) + 1) ≤ (𝑄 − 𝑦) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))) |
241 | 8 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℝ) |
242 | 241 | recnd 11003 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℂ) |
243 | 63, 242 | mulcomd 10996 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 · 𝑄) = (𝑄 · 𝑃)) |
244 | 65, 242 | mulcomd 10996 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) · 𝑄) = (𝑄 · (2 · 𝑢))) |
245 | 62 | nnne0d 12023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ≠ 0) |
246 | 242, 63, 245 | divcan1d 11752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · 𝑃) = 𝑄) |
247 | 246 | oveq1d 7290 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · 𝑃) · (2 · 𝑢)) = (𝑄 · (2 · 𝑢))) |
248 | 12 | recnd 11003 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℂ) |
249 | 248, 63, 65 | mul32d 11185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · 𝑃) · (2 · 𝑢)) = (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃)) |
250 | 244, 247,
249 | 3eqtr2d 2784 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) · 𝑄) = (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃)) |
251 | 243, 250 | oveq12d 7293 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 · 𝑄) − ((2 · 𝑢) · 𝑄)) = ((𝑄 · 𝑃) − (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃))) |
252 | 63, 65, 242 | subdird 11432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑃 · 𝑄) − ((2 · 𝑢) · 𝑄))) |
253 | 19 | recnd 11003 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℂ) |
254 | 242, 253,
63 | subdird 11432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃) = ((𝑄 · 𝑃) − (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃))) |
255 | 251, 252,
254 | 3eqtr4d 2788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)) |
256 | 255 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)) |
257 | 256 | breq2d 5086 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))) |
258 | 19 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) |
259 | 236, 258 | resubcld 11403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ) |
260 | 62 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℕ) |
261 | 260 | nnred 11988 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ) |
262 | 260 | nngt0d 12022 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 0 < 𝑃) |
263 | | ltmul1 11825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))) |
264 | 238, 259,
261, 262, 263 | syl112anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))) |
265 | | ltsub13 11456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦))) |
266 | 238, 236,
258, 265 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦))) |
267 | 257, 264,
266 | 3bitr2d 307 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦))) |
268 | 7 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℕ) |
269 | 268 | nnzd 12425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℤ) |
270 | | nnz 12342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
271 | | zsubcl 12362 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑄 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑄 − 𝑦) ∈ ℤ) |
272 | 269, 270,
271 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑄 − 𝑦) ∈ ℤ) |
273 | | fllt 13526 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ (𝑄 − 𝑦) ∈ ℤ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦) ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄 − 𝑦))) |
274 | 258, 272,
273 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦) ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄 − 𝑦))) |
275 | 20 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈
ℤ) |
276 | | zltp1le 12370 |
. . . . . . . . . . . . . . . . . . . . . . . . . 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 7286 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (2
· 𝑁) = (2 ·
((𝑄 − 1) /
2)) |
281 | | peano2rem 11288 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑄 ∈ ℝ → (𝑄 − 1) ∈
ℝ) |
282 | 241, 281 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) ∈ ℝ) |
283 | 282 | recnd 11003 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) ∈ ℂ) |
284 | | 2cnd 12051 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℂ) |
285 | 73 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ≠ 0) |
286 | 283, 284,
285 | divcan2d 11753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · ((𝑄 − 1) / 2)) = (𝑄 − 1)) |
287 | 280, 286 | eqtrid 2790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) = (𝑄 − 1)) |
288 | 287 | oveq1d 7290 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = ((𝑄 − 1) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
289 | | 1cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 1 ∈ ℂ) |
290 | 20 | zcnd 12427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ) |
291 | 242, 289,
290 | sub32d 11364 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = ((𝑄 − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) − 1)) |
292 | 242, 290,
289 | subsub4d 11363 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) − 1) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))) |
293 | 288, 291,
292 | 3eqtrd 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))) |
294 | 293 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))) |
295 | 294 | breq2d 5086 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))) |
296 | 240, 278,
295 | 3bitr4d 311 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
297 | 296 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ≤ 𝑁 ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
298 | | 2nn 12046 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 2 ∈
ℕ |
299 | 6, 279 | gausslemma2dlem0b 26505 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑁 ∈ ℕ) |
300 | | nnmulcl 11997 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((2
∈ ℕ ∧ 𝑁
∈ ℕ) → (2 · 𝑁) ∈ ℕ) |
301 | 298, 299,
300 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (2 · 𝑁) ∈
ℕ) |
302 | 301 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℕ) |
303 | 302 | nnred 11988 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℝ) |
304 | 299 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℕ) |
305 | 304 | nnred 11988 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℝ) |
306 | 20 | zred 12426 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ) |
307 | 299 | nncnd 11989 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑁 ∈ ℂ) |
308 | 307 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℂ) |
309 | 308 | 2timesd 12216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) = (𝑁 + 𝑁)) |
310 | 308, 308,
309 | mvrladdd 11388 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) = 𝑁) |
311 | 241 | rehalfcld 12220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ∈ ℝ) |
312 | 241 | ltm1d 11907 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) < 𝑄) |
313 | 150 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℝ) |
314 | 152 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 2) |
315 | | ltdiv1 11839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑄 − 1) ∈ ℝ ∧
𝑄 ∈ ℝ ∧ (2
∈ ℝ ∧ 0 < 2)) → ((𝑄 − 1) < 𝑄 ↔ ((𝑄 − 1) / 2) < (𝑄 / 2))) |
316 | 282, 241,
313, 314, 315 | syl112anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) < 𝑄 ↔ ((𝑄 − 1) / 2) < (𝑄 / 2))) |
317 | 312, 316 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) / 2) < (𝑄 / 2)) |
318 | 279, 317 | eqbrtrid 5109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 < (𝑄 / 2)) |
319 | 305, 311,
318 | ltled 11123 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ (𝑄 / 2)) |
320 | 242, 284,
63, 285 | div32d 11774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 2) · 𝑃) = (𝑄 · (𝑃 / 2))) |
321 | 124 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℝ) |
322 | 321 | rehalfcld 12220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) ∈ ℝ) |
323 | | peano2re 11148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
((⌊‘(𝑀 /
2)) ∈ ℝ → ((⌊‘(𝑀 / 2)) + 1) ∈ ℝ) |
324 | 322, 133,
323 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ∈ ℝ) |
325 | 15 | zred 12426 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℝ) |
326 | | flltp1 13520 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑀 / 2) ∈ ℝ →
(𝑀 / 2) <
((⌊‘(𝑀 / 2)) +
1)) |
327 | 322, 326 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) < ((⌊‘(𝑀 / 2)) + 1)) |
328 | | elfzle1 13259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → ((⌊‘(𝑀 / 2)) + 1) ≤ 𝑢) |
329 | 328 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ≤ 𝑢) |
330 | 322, 324,
325, 327, 329 | ltletrd 11135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) < 𝑢) |
331 | | ltdivmul 11850 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑀 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → ((𝑀 / 2) < 𝑢 ↔ 𝑀 < (2 · 𝑢))) |
332 | 321, 325,
313, 314, 331 | syl112anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 / 2) < 𝑢 ↔ 𝑀 < (2 · 𝑢))) |
333 | 330, 332 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 < (2 · 𝑢)) |
334 | 122, 333 | eqbrtrrid 5110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) / 2) < (2 · 𝑢)) |
335 | 62 | nnred 11988 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℝ) |
336 | | peano2rem 11288 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈
ℝ) |
337 | 335, 336 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℝ) |
338 | | ltdivmul 11850 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑃 − 1) ∈ ℝ ∧
(2 · 𝑢) ∈
ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝑃 − 1) / 2) < (2 · 𝑢) ↔ (𝑃 − 1) < (2 · (2 ·
𝑢)))) |
339 | 337, 18, 313, 314, 338 | syl112anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑃 − 1) / 2) < (2 · 𝑢) ↔ (𝑃 − 1) < (2 · (2 ·
𝑢)))) |
340 | 334, 339 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) < (2 · (2 ·
𝑢))) |
341 | 202 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ) |
342 | | zmulcl 12369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((2
∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → (2 · (2
· 𝑢)) ∈
ℤ) |
343 | 13, 17, 342 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · (2 · 𝑢)) ∈
ℤ) |
344 | | zlem1lt 12372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 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 256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ≤ (2 · (2 · 𝑢))) |
347 | | ledivmul 11851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑃 ∈ ℝ ∧ (2
· 𝑢) ∈ ℝ
∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ 𝑃 ≤ (2 · (2 · 𝑢)))) |
348 | 335, 18, 313, 314, 347 | syl112anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ 𝑃 ≤ (2 · (2 · 𝑢)))) |
349 | 346, 348 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 / 2) ≤ (2 · 𝑢)) |
350 | 335 | rehalfcld 12220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 / 2) ∈ ℝ) |
351 | 268 | nngt0d 12022 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 𝑄) |
352 | | lemul2 11828 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑃 / 2) ∈ ℝ ∧ (2
· 𝑢) ∈ ℝ
∧ (𝑄 ∈ ℝ
∧ 0 < 𝑄)) →
((𝑃 / 2) ≤ (2 ·
𝑢) ↔ (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢)))) |
353 | 350, 18, 241, 351, 352 | syl112anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢)))) |
354 | 349, 353 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢))) |
355 | 320, 354 | eqbrtrd 5096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢))) |
356 | 241, 18 | remulcld 11005 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (2 · 𝑢)) ∈ ℝ) |
357 | 62 | nngt0d 12022 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 𝑃) |
358 | | lemuldiv 11855 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑄 / 2) ∈ ℝ ∧
(𝑄 · (2 ·
𝑢)) ∈ ℝ ∧
(𝑃 ∈ ℝ ∧ 0
< 𝑃)) → (((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))) |
359 | 311, 356,
335, 357, 358 | syl112anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))) |
360 | 355, 359 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)) |
361 | 242, 65, 63, 245 | div23d 11788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 · (2 · 𝑢)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑢))) |
362 | 360, 361 | breqtrd 5100 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ≤ ((𝑄 / 𝑃) · (2 · 𝑢))) |
363 | 305, 311,
19, 319, 362 | letrd 11132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))) |
364 | 299 | nnzd 12425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → 𝑁 ∈ ℤ) |
365 | 364 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℤ) |
366 | | flge 13525 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
367 | 19, 365, 366 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
368 | 363, 367 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) |
369 | 310, 368 | eqbrtrd 5096 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) |
370 | 303, 305,
306, 369 | subled 11578 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) |
371 | 370 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) |
372 | 302 | nnzd 12425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℤ) |
373 | 372, 20 | zsubcld 12431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ) |
374 | 373 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ) |
375 | 374 | zred 12426 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℝ) |
376 | 299 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ) |
377 | 376 | nnred 11988 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℝ) |
378 | | letr 11069 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ ((2
· 𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) → 𝑦 ≤ 𝑁)) |
379 | 238, 375,
377, 378 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) → 𝑦 ≤ 𝑁)) |
380 | 371, 379 | mpan2d 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → 𝑦 ≤ 𝑁)) |
381 | 380 | pm4.71rd 563 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ≤ 𝑁 ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
382 | 297, 381 | bitr4d 281 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
383 | 382 | pm5.32da 579 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
384 | 383 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
385 | 232, 384 | bitrid 282 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
386 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑥 = (𝑃 − (2 · 𝑢))) |
387 | 341, 17 | zsubcld 12431 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ) |
388 | | elfzle2 13260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → 𝑢 ≤ 𝑀) |
389 | 388 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ≤ 𝑀) |
390 | 389, 122 | breqtrdi 5115 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ≤ ((𝑃 − 1) / 2)) |
391 | | lemuldiv2 11856 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑢 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧
(2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑢) ≤ (𝑃 − 1) ↔ 𝑢 ≤ ((𝑃 − 1) / 2))) |
392 | 325, 337,
313, 314, 391 | syl112anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) ≤ (𝑃 − 1) ↔ 𝑢 ≤ ((𝑃 − 1) / 2))) |
393 | 390, 392 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ≤ (𝑃 − 1)) |
394 | 335 | ltm1d 11907 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) < 𝑃) |
395 | 18, 337, 335, 393, 394 | lelttrd 11133 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) < 𝑃) |
396 | 18, 335 | posdifd 11562 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) < 𝑃 ↔ 0 < (𝑃 − (2 · 𝑢)))) |
397 | 395, 396 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < (𝑃 − (2 · 𝑢))) |
398 | | elnnz 12329 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑃 − (2 · 𝑢)) ∈ ℕ ↔ ((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ 0 <
(𝑃 − (2 ·
𝑢)))) |
399 | 387, 397,
398 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℕ) |
400 | 63, 65, 289 | sub32d 11364 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) − 1) = ((𝑃 − 1) − (2 · 𝑢))) |
401 | 122, 122 | oveq12i 7287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑀 + 𝑀) = (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) |
402 | 62 | nnzd 12425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ) |
403 | 402, 204 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℤ) |
404 | 403 | zcnd 12427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℂ) |
405 | 404 | 2halvesd 12219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1)) |
406 | 401, 405 | eqtrid 2790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 + 𝑀) = (𝑃 − 1)) |
407 | 406 | oveq1d 7290 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 + 𝑀) − 𝑀) = ((𝑃 − 1) − 𝑀)) |
408 | 158 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℂ) |
409 | 408, 408 | pncan2d 11334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 + 𝑀) − 𝑀) = 𝑀) |
410 | 407, 409 | eqtr3d 2780 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − 𝑀) = 𝑀) |
411 | 410, 333 | eqbrtrd 5096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − 𝑀) < (2 · 𝑢)) |
412 | 337, 321,
18, 411 | ltsub23d 11580 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − (2 · 𝑢)) < 𝑀) |
413 | 400, 412 | eqbrtrd 5096 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) − 1) < 𝑀) |
414 | 123 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℕ) |
415 | 414 | nnzd 12425 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℤ) |
416 | | zlem1lt 12372 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑃 − (2 · 𝑢)) ≤ 𝑀 ↔ ((𝑃 − (2 · 𝑢)) − 1) < 𝑀)) |
417 | 387, 415,
416 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) ≤ 𝑀 ↔ ((𝑃 − (2 · 𝑢)) − 1) < 𝑀)) |
418 | 413, 417 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ≤ 𝑀) |
419 | | fznn 13324 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀 ∈ ℤ → ((𝑃 − (2 · 𝑢)) ∈ (1...𝑀) ↔ ((𝑃 − (2 · 𝑢)) ∈ ℕ ∧ (𝑃 − (2 · 𝑢)) ≤ 𝑀))) |
420 | 415, 419 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) ∈ (1...𝑀) ↔ ((𝑃 − (2 · 𝑢)) ∈ ℕ ∧ (𝑃 − (2 · 𝑢)) ≤ 𝑀))) |
421 | 399, 418,
420 | mpbir2and 710 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ (1...𝑀)) |
422 | 421 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑃 − (2 · 𝑢)) ∈ (1...𝑀)) |
423 | 386, 422 | eqeltrd 2839 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑥 ∈ (1...𝑀)) |
424 | 423 | biantrurd 533 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...𝑁) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)))) |
425 | 364 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑁 ∈ ℤ) |
426 | | fznn 13324 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℤ → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁))) |
427 | 425, 426 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁))) |
428 | 424, 427 | bitr3d 280 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁))) |
429 | 386 | oveq1d 7290 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑥 · 𝑄) = ((𝑃 − (2 · 𝑢)) · 𝑄)) |
430 | 429 | breq2d 5086 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑦 · 𝑃) < (𝑥 · 𝑄) ↔ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) |
431 | 428, 430 | anbi12d 631 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ ((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)))) |
432 | 373 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ) |
433 | | fznn 13324 |
. . . . . . . . . . . . . . . . . . 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 282 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (〈𝑥, 𝑦〉 ∈ 𝑆 ↔ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
437 | 436 | pm5.32da 579 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑥 = (𝑃 − (2 · 𝑢)) ∧ 〈𝑥, 𝑦〉 ∈ 𝑆) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))) |
438 | | vex 3436 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑥 ∈ V |
439 | | vex 3436 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑦 ∈ V |
440 | 438, 439 | op1std 7841 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) |
441 | 440 | eqeq1d 2740 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((1st ‘𝑧) = (𝑃 − (2 · 𝑢)) ↔ 𝑥 = (𝑃 − (2 · 𝑢)))) |
442 | 441 | elrab 3624 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ↔ (〈𝑥, 𝑦〉 ∈ 𝑆 ∧ 𝑥 = (𝑃 − (2 · 𝑢)))) |
443 | 442 | biancomi 463 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 〈𝑥, 𝑦〉 ∈ 𝑆)) |
444 | | opelxp 5625 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 ·
𝑁) −
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 ∈ {(𝑃 − (2 · 𝑢))} ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
445 | | velsn 4577 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ {(𝑃 − (2 · 𝑢))} ↔ 𝑥 = (𝑃 − (2 · 𝑢))) |
446 | 445 | anbi1i 624 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ {(𝑃 − (2 · 𝑢))} ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
447 | 444, 446 | bitri 274 |
. . . . . . . . . . . . . . 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 5702 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → {𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))} = ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) |
450 | 449 | fveq2d 6778 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘{𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = (♯‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))) |
451 | | fzfid 13693 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin) |
452 | | xpsnen2g 8852 |
. . . . . . . . . . . . . 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 14062 |
. . . . . . . . . . . . 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 11826 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((2
· 𝑢) ∈ ℝ
∧ 𝑃 ∈ ℝ
∧ (𝑄 ∈ ℝ
∧ 0 < 𝑄)) → ((2
· 𝑢) < 𝑃 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃))) |
457 | 18, 335, 241, 351, 456 | syl112anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) < 𝑃 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃))) |
458 | 395, 457 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)) |
459 | | ltdivmul2 11852 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑄 · (2 · 𝑢)) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 <
𝑃)) → (((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃))) |
460 | 356, 241,
335, 357, 459 | syl112anc 1373 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃))) |
461 | 458, 460 | mpbird 256 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄) |
462 | 361, 461 | eqbrtrrd 5098 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄) |
463 | | fllt 13526 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑄 ∈ ℤ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄)) |
464 | 19, 269, 463 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄)) |
465 | 462, 464 | mpbid 231 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄) |
466 | | zltlem1 12373 |
. . . . . . . . . . . . . . . . 17
⊢
(((⌊‘((𝑄
/ 𝑃) · (2 ·
𝑢))) ∈ ℤ ∧
𝑄 ∈ ℤ) →
((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1))) |
467 | 20, 269, 466 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1))) |
468 | 465, 467 | mpbid 231 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1)) |
469 | 468, 287 | breqtrrd 5102 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (2 · 𝑁)) |
470 | | eluz2 12588 |
. . . . . . . . . . . . . 14
⊢ ((2
· 𝑁) ∈
(ℤ≥‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (2 · 𝑁) ∈ ℤ ∧
(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (2 · 𝑁))) |
471 | 20, 372, 469, 470 | syl3anbrc 1342 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈
(ℤ≥‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
472 | | uznn0sub 12617 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑁) ∈
(ℤ≥‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈
ℕ0) |
473 | | hashfz1 14060 |
. . . . . . . . . . . . 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 2782 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘{𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
476 | 475 | sumeq2dv 15415 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(♯‘{𝑧 ∈ 𝑆 ∣ (1st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
477 | 80, 224, 476 | 3eqtr3rd 2787 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) |
478 | 301 | nncnd 11989 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · 𝑁) ∈
ℂ) |
479 | 478 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℂ) |
480 | 5, 479, 290 | fsumsub 15500 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
481 | 477, 480 | eqtr3d 2780 |
. . . . . . . 8
⊢ (𝜑 → (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) |
482 | 481 | oveq2d 7291 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) =
(Σ𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) |
483 | 21 | zcnd 12427 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ) |
484 | 5, 372 | fsumzcl 15447 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) ∈ ℤ) |
485 | 484 | zcnd 12427 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) ∈ ℂ) |
486 | 483, 485 | pncan3d 11335 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁)) |
487 | | fsumconst 15502 |
. . . . . . . . 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 14071 |
. . . . . . . . . . 11
⊢
((((⌊‘(𝑀
/ 2)) + 1)...𝑀) ∈ Fin
→ (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈
ℕ0) |
490 | 5, 489 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈
ℕ0) |
491 | 490 | nn0cnd 12295 |
. . . . . . . . 9
⊢ (𝜑 →
(♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℂ) |
492 | | 2cnd 12051 |
. . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℂ) |
493 | 491, 492,
307 | mul12d 11184 |
. . . . . . . 8
⊢ (𝜑 →
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)) = (2 ·
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) |
494 | 488, 493 | eqtrd 2778 |
. . . . . . 7
⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = (2 ·
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) |
495 | 482, 486,
494 | 3eqtrd 2782 |
. . . . . 6
⊢ (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})) = (2 ·
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) |
496 | 495 | oveq2d 7291 |
. . . . 5
⊢ (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) = (-1↑(2
· ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))) |
497 | 13 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 2 ∈
ℤ) |
498 | 490 | nn0zd 12424 |
. . . . . . 7
⊢ (𝜑 →
(♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℤ) |
499 | 498, 364 | zmulcld 12432 |
. . . . . 6
⊢ (𝜑 →
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ) |
500 | | expmulz 13829 |
. . . . . 6
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ)) → (-1↑(2
· ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) =
((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) |
501 | 2, 4, 497, 499, 500 | syl22anc 836 |
. . . . 5
⊢ (𝜑 → (-1↑(2 ·
((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) =
((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) |
502 | | neg1sqe1 13913 |
. . . . . . 7
⊢
(-1↑2) = 1 |
503 | 502 | oveq1i 7285 |
. . . . . 6
⊢
((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) =
(1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) |
504 | | 1exp 13812 |
. . . . . . 7
⊢
(((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ →
(1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1) |
505 | 499, 504 | syl 17 |
. . . . . 6
⊢ (𝜑 →
(1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1) |
506 | 503, 505 | eqtrid 2790 |
. . . . 5
⊢ (𝜑 →
((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1) |
507 | 496, 501,
506 | 3eqtrd 2782 |
. . . 4
⊢ (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) =
1) |
508 | 41, 52, 507 | 3eqtr4d 2788 |
. . 3
⊢ (𝜑 →
((-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) =
(-1↑(Σ𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})))) |
509 | | expaddz 13827 |
. . . 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 836 |
. . 3
⊢ (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) =
((-1↑Σ𝑢 ∈
(((⌊‘(𝑀 / 2)) +
1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})))) |
511 | 508, 510 | eqtr2d 2779 |
. 2
⊢ (𝜑 → ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) =
((-1↑(♯‘{𝑧
∈ 𝑆 ∣ ¬ 2
∥ (1st ‘𝑧)})) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)})))) |
512 | 22, 38, 38, 40, 511 | mulcan2ad 11611 |
1
⊢ (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st
‘𝑧)}))) |