| Step | Hyp | Ref
| Expression |
| 1 | | lgsquad2.1 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 2 | | 2nn 12339 |
. . . . 5
⊢ 2 ∈
ℕ |
| 3 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → 2 ∈
ℕ) |
| 4 | | lgsquad2.3 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 5 | 1 | nnzd 12640 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 6 | | 2z 12649 |
. . . . . 6
⊢ 2 ∈
ℤ |
| 7 | | gcdcom 16550 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 2 ∈
ℤ) → (𝑀 gcd 2) =
(2 gcd 𝑀)) |
| 8 | 5, 6, 7 | sylancl 586 |
. . . . 5
⊢ (𝜑 → (𝑀 gcd 2) = (2 gcd 𝑀)) |
| 9 | | lgsquad2.2 |
. . . . . 6
⊢ (𝜑 → ¬ 2 ∥ 𝑀) |
| 10 | | 2prm 16729 |
. . . . . . 7
⊢ 2 ∈
ℙ |
| 11 | | coprm 16748 |
. . . . . . 7
⊢ ((2
∈ ℙ ∧ 𝑀
∈ ℤ) → (¬ 2 ∥ 𝑀 ↔ (2 gcd 𝑀) = 1)) |
| 12 | 10, 5, 11 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → (¬ 2 ∥ 𝑀 ↔ (2 gcd 𝑀) = 1)) |
| 13 | 9, 12 | mpbid 232 |
. . . . 5
⊢ (𝜑 → (2 gcd 𝑀) = 1) |
| 14 | 8, 13 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (𝑀 gcd 2) = 1) |
| 15 | | rpmulgcd 16594 |
. . . 4
⊢ (((𝑀 ∈ ℕ ∧ 2 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ (𝑀 gcd 2) =
1) → (𝑀 gcd (2
· 𝑁)) = (𝑀 gcd 𝑁)) |
| 16 | 1, 3, 4, 14, 15 | syl31anc 1375 |
. . 3
⊢ (𝜑 → (𝑀 gcd (2 · 𝑁)) = (𝑀 gcd 𝑁)) |
| 17 | | lgsquad2.5 |
. . 3
⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) |
| 18 | 16, 17 | eqtrd 2777 |
. 2
⊢ (𝜑 → (𝑀 gcd (2 · 𝑁)) = 1) |
| 19 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑚 = 1 → (𝑚 /L 𝑁) = (1 /L 𝑁)) |
| 20 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑚 = 1 → (𝑁 /L 𝑚) = (𝑁 /L 1)) |
| 21 | 19, 20 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑚 = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = ((1 /L 𝑁) · (𝑁 /L 1))) |
| 22 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → (𝑚 − 1) = (1 − 1)) |
| 23 | | 1m1e0 12338 |
. . . . . . . . . . . 12
⊢ (1
− 1) = 0 |
| 24 | 22, 23 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → (𝑚 − 1) = 0) |
| 25 | 24 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑚 = 1 → ((𝑚 − 1) / 2) = (0 / 2)) |
| 26 | | 2cn 12341 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
| 27 | | 2ne0 12370 |
. . . . . . . . . . 11
⊢ 2 ≠
0 |
| 28 | 26, 27 | div0i 12001 |
. . . . . . . . . 10
⊢ (0 / 2) =
0 |
| 29 | 25, 28 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑚 = 1 → ((𝑚 − 1) / 2) = 0) |
| 30 | 29 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑚 = 1 → (((𝑚 − 1) / 2) ·
((𝑁 − 1) / 2)) = (0
· ((𝑁 − 1) /
2))) |
| 31 | 30 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑚 = 1 → (-1↑(((𝑚 − 1) / 2) ·
((𝑁 − 1) / 2))) =
(-1↑(0 · ((𝑁
− 1) / 2)))) |
| 32 | 21, 31 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑚 = 1 → (((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))) ↔ ((1
/L 𝑁)
· (𝑁
/L 1)) = (-1↑(0 · ((𝑁 − 1) / 2))))) |
| 33 | 32 | imbi2d 340 |
. . . . 5
⊢ (𝑚 = 1 → (((𝑚 gcd (2 · 𝑁)) = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)))) ↔ ((𝑚 gcd (2 · 𝑁)) = 1 → ((1
/L 𝑁)
· (𝑁
/L 1)) = (-1↑(0 · ((𝑁 − 1) / 2)))))) |
| 34 | 33 | imbi2d 340 |
. . . 4
⊢ (𝑚 = 1 → ((𝜑 → ((𝑚 gcd (2 · 𝑁)) = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))))) ↔ (𝜑 → ((𝑚 gcd (2 · 𝑁)) = 1 → ((1 /L 𝑁) · (𝑁 /L 1)) = (-1↑(0
· ((𝑁 − 1) /
2))))))) |
| 35 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑚 = 𝑥 → (𝑚 gcd (2 · 𝑁)) = (𝑥 gcd (2 · 𝑁))) |
| 36 | 35 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑚 = 𝑥 → ((𝑚 gcd (2 · 𝑁)) = 1 ↔ (𝑥 gcd (2 · 𝑁)) = 1)) |
| 37 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑚 = 𝑥 → (𝑚 /L 𝑁) = (𝑥 /L 𝑁)) |
| 38 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑚 = 𝑥 → (𝑁 /L 𝑚) = (𝑁 /L 𝑥)) |
| 39 | 37, 38 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑚 = 𝑥 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = ((𝑥 /L 𝑁) · (𝑁 /L 𝑥))) |
| 40 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑥 → (𝑚 − 1) = (𝑥 − 1)) |
| 41 | 40 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑚 = 𝑥 → ((𝑚 − 1) / 2) = ((𝑥 − 1) / 2)) |
| 42 | 41 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑚 = 𝑥 → (((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)) = (((𝑥 − 1) / 2) · ((𝑁 − 1) / 2))) |
| 43 | 42 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑚 = 𝑥 → (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))) = (-1↑(((𝑥 − 1) / 2) ·
((𝑁 − 1) /
2)))) |
| 44 | 39, 43 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑚 = 𝑥 → (((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))) ↔ ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2))))) |
| 45 | 36, 44 | imbi12d 344 |
. . . . 5
⊢ (𝑚 = 𝑥 → (((𝑚 gcd (2 · 𝑁)) = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)))) ↔ ((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))))) |
| 46 | 45 | imbi2d 340 |
. . . 4
⊢ (𝑚 = 𝑥 → ((𝜑 → ((𝑚 gcd (2 · 𝑁)) = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))))) ↔ (𝜑 → ((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2))))))) |
| 47 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑚 = 𝑦 → (𝑚 gcd (2 · 𝑁)) = (𝑦 gcd (2 · 𝑁))) |
| 48 | 47 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑚 = 𝑦 → ((𝑚 gcd (2 · 𝑁)) = 1 ↔ (𝑦 gcd (2 · 𝑁)) = 1)) |
| 49 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑚 = 𝑦 → (𝑚 /L 𝑁) = (𝑦 /L 𝑁)) |
| 50 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑚 = 𝑦 → (𝑁 /L 𝑚) = (𝑁 /L 𝑦)) |
| 51 | 49, 50 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑚 = 𝑦 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = ((𝑦 /L 𝑁) · (𝑁 /L 𝑦))) |
| 52 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑦 → (𝑚 − 1) = (𝑦 − 1)) |
| 53 | 52 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑚 = 𝑦 → ((𝑚 − 1) / 2) = ((𝑦 − 1) / 2)) |
| 54 | 53 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑚 = 𝑦 → (((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)) = (((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))) |
| 55 | 54 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑚 = 𝑦 → (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))) = (-1↑(((𝑦 − 1) / 2) ·
((𝑁 − 1) /
2)))) |
| 56 | 51, 55 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑚 = 𝑦 → (((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))) ↔ ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))) |
| 57 | 48, 56 | imbi12d 344 |
. . . . 5
⊢ (𝑚 = 𝑦 → (((𝑚 gcd (2 · 𝑁)) = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)))) ↔ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2)))))) |
| 58 | 57 | imbi2d 340 |
. . . 4
⊢ (𝑚 = 𝑦 → ((𝜑 → ((𝑚 gcd (2 · 𝑁)) = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))))) ↔ (𝜑 → ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))))) |
| 59 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑚 = (𝑥 · 𝑦) → (𝑚 gcd (2 · 𝑁)) = ((𝑥 · 𝑦) gcd (2 · 𝑁))) |
| 60 | 59 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑚 = (𝑥 · 𝑦) → ((𝑚 gcd (2 · 𝑁)) = 1 ↔ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1)) |
| 61 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑚 = (𝑥 · 𝑦) → (𝑚 /L 𝑁) = ((𝑥 · 𝑦) /L 𝑁)) |
| 62 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑚 = (𝑥 · 𝑦) → (𝑁 /L 𝑚) = (𝑁 /L (𝑥 · 𝑦))) |
| 63 | 61, 62 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑚 = (𝑥 · 𝑦) → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (((𝑥 · 𝑦) /L 𝑁) · (𝑁 /L (𝑥 · 𝑦)))) |
| 64 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑥 · 𝑦) → (𝑚 − 1) = ((𝑥 · 𝑦) − 1)) |
| 65 | 64 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑚 = (𝑥 · 𝑦) → ((𝑚 − 1) / 2) = (((𝑥 · 𝑦) − 1) / 2)) |
| 66 | 65 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑚 = (𝑥 · 𝑦) → (((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)) = ((((𝑥 · 𝑦) − 1) / 2) · ((𝑁 − 1) /
2))) |
| 67 | 66 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑚 = (𝑥 · 𝑦) → (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))) = (-1↑((((𝑥 · 𝑦) − 1) / 2) · ((𝑁 − 1) /
2)))) |
| 68 | 63, 67 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑚 = (𝑥 · 𝑦) → (((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))) ↔ (((𝑥 · 𝑦) /L 𝑁) · (𝑁 /L (𝑥 · 𝑦))) = (-1↑((((𝑥 · 𝑦) − 1) / 2) · ((𝑁 − 1) /
2))))) |
| 69 | 60, 68 | imbi12d 344 |
. . . . 5
⊢ (𝑚 = (𝑥 · 𝑦) → (((𝑚 gcd (2 · 𝑁)) = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)))) ↔ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 → (((𝑥 · 𝑦) /L 𝑁) · (𝑁 /L (𝑥 · 𝑦))) = (-1↑((((𝑥 · 𝑦) − 1) / 2) · ((𝑁 − 1) /
2)))))) |
| 70 | 69 | imbi2d 340 |
. . . 4
⊢ (𝑚 = (𝑥 · 𝑦) → ((𝜑 → ((𝑚 gcd (2 · 𝑁)) = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))))) ↔ (𝜑 → (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 → (((𝑥 · 𝑦) /L 𝑁) · (𝑁 /L (𝑥 · 𝑦))) = (-1↑((((𝑥 · 𝑦) − 1) / 2) · ((𝑁 − 1) /
2))))))) |
| 71 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (𝑚 gcd (2 · 𝑁)) = (𝑀 gcd (2 · 𝑁))) |
| 72 | 71 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑚 = 𝑀 → ((𝑚 gcd (2 · 𝑁)) = 1 ↔ (𝑀 gcd (2 · 𝑁)) = 1)) |
| 73 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (𝑚 /L 𝑁) = (𝑀 /L 𝑁)) |
| 74 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (𝑁 /L 𝑚) = (𝑁 /L 𝑀)) |
| 75 | 73, 74 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = ((𝑀 /L 𝑁) · (𝑁 /L 𝑀))) |
| 76 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑀 → (𝑚 − 1) = (𝑀 − 1)) |
| 77 | 76 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑚 = 𝑀 → ((𝑚 − 1) / 2) = ((𝑀 − 1) / 2)) |
| 78 | 77 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)) = (((𝑀 − 1) / 2) · ((𝑁 − 1) /
2))) |
| 79 | 78 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))) = (-1↑(((𝑀 − 1) / 2) ·
((𝑁 − 1) /
2)))) |
| 80 | 75, 79 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))) ↔ ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) /
2))))) |
| 81 | 72, 80 | imbi12d 344 |
. . . . 5
⊢ (𝑚 = 𝑀 → (((𝑚 gcd (2 · 𝑁)) = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)))) ↔ ((𝑀 gcd (2 · 𝑁)) = 1 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) /
2)))))) |
| 82 | 81 | imbi2d 340 |
. . . 4
⊢ (𝑚 = 𝑀 → ((𝜑 → ((𝑚 gcd (2 · 𝑁)) = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))))) ↔ (𝜑 → ((𝑀 gcd (2 · 𝑁)) = 1 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) /
2))))))) |
| 83 | | 1t1e1 12428 |
. . . . . . 7
⊢ (1
· 1) = 1 |
| 84 | | neg1cn 12380 |
. . . . . . . 8
⊢ -1 ∈
ℂ |
| 85 | | exp0 14106 |
. . . . . . . 8
⊢ (-1
∈ ℂ → (-1↑0) = 1) |
| 86 | 84, 85 | ax-mp 5 |
. . . . . . 7
⊢
(-1↑0) = 1 |
| 87 | 83, 86 | eqtr4i 2768 |
. . . . . 6
⊢ (1
· 1) = (-1↑0) |
| 88 | | sq1 14234 |
. . . . . . . . 9
⊢
(1↑2) = 1 |
| 89 | 88 | oveq1i 7441 |
. . . . . . . 8
⊢
((1↑2) /L 𝑁) = (1 /L 𝑁) |
| 90 | | 1z 12647 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
| 91 | | ax-1ne0 11224 |
. . . . . . . . . 10
⊢ 1 ≠
0 |
| 92 | 90, 91 | pm3.2i 470 |
. . . . . . . . 9
⊢ (1 ∈
ℤ ∧ 1 ≠ 0) |
| 93 | 4 | nnzd 12640 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 94 | | 1gcd 16570 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → (1 gcd
𝑁) = 1) |
| 95 | 93, 94 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (1 gcd 𝑁) = 1) |
| 96 | | lgssq 27381 |
. . . . . . . . 9
⊢ (((1
∈ ℤ ∧ 1 ≠ 0) ∧ 𝑁 ∈ ℤ ∧ (1 gcd 𝑁) = 1) → ((1↑2)
/L 𝑁) =
1) |
| 97 | 92, 93, 95, 96 | mp3an2i 1468 |
. . . . . . . 8
⊢ (𝜑 → ((1↑2)
/L 𝑁) =
1) |
| 98 | 89, 97 | eqtr3id 2791 |
. . . . . . 7
⊢ (𝜑 → (1 /L
𝑁) = 1) |
| 99 | 88 | oveq2i 7442 |
. . . . . . . 8
⊢ (𝑁 /L
(1↑2)) = (𝑁
/L 1) |
| 100 | | 1nn 12277 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ |
| 101 | 100 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℕ) |
| 102 | | gcd1 16565 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → (𝑁 gcd 1) = 1) |
| 103 | 93, 102 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 gcd 1) = 1) |
| 104 | | lgssq2 27382 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 1 ∈
ℕ ∧ (𝑁 gcd 1) =
1) → (𝑁
/L (1↑2)) = 1) |
| 105 | 93, 101, 103, 104 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 /L (1↑2)) =
1) |
| 106 | 99, 105 | eqtr3id 2791 |
. . . . . . 7
⊢ (𝜑 → (𝑁 /L 1) =
1) |
| 107 | 98, 106 | oveq12d 7449 |
. . . . . 6
⊢ (𝜑 → ((1 /L
𝑁) · (𝑁 /L 1)) = (1
· 1)) |
| 108 | | nnm1nn0 12567 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
| 109 | 4, 108 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
| 110 | 109 | nn0cnd 12589 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 − 1) ∈ ℂ) |
| 111 | 110 | halfcld 12511 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 − 1) / 2) ∈
ℂ) |
| 112 | 111 | mul02d 11459 |
. . . . . . 7
⊢ (𝜑 → (0 · ((𝑁 − 1) / 2)) =
0) |
| 113 | 112 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → (-1↑(0 ·
((𝑁 − 1) / 2))) =
(-1↑0)) |
| 114 | 87, 107, 113 | 3eqtr4a 2803 |
. . . . 5
⊢ (𝜑 → ((1 /L
𝑁) · (𝑁 /L 1)) =
(-1↑(0 · ((𝑁
− 1) / 2)))) |
| 115 | 114 | a1d 25 |
. . . 4
⊢ (𝜑 → ((𝑚 gcd (2 · 𝑁)) = 1 → ((1 /L 𝑁) · (𝑁 /L 1)) = (-1↑(0
· ((𝑁 − 1) /
2))))) |
| 116 | | simprl 771 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → 𝑚 ∈ ℙ) |
| 117 | | prmz 16712 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℙ → 𝑚 ∈
ℤ) |
| 118 | 117 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → 𝑚 ∈ ℤ) |
| 119 | 6 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → 2 ∈
ℤ) |
| 120 | 4 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → 𝑁 ∈ ℕ) |
| 121 | 120 | nnzd 12640 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → 𝑁 ∈ ℤ) |
| 122 | | zmulcl 12666 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ) → (2 · 𝑁) ∈ ℤ) |
| 123 | 6, 121, 122 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → (2 · 𝑁) ∈
ℤ) |
| 124 | | simprr 773 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → (𝑚 gcd (2 · 𝑁)) = 1) |
| 125 | | dvdsmul1 16315 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ) → 2 ∥ (2 · 𝑁)) |
| 126 | 6, 121, 125 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → 2 ∥ (2 · 𝑁)) |
| 127 | | rpdvds 16697 |
. . . . . . . . . . 11
⊢ (((𝑚 ∈ ℤ ∧ 2 ∈
ℤ ∧ (2 · 𝑁) ∈ ℤ) ∧ ((𝑚 gcd (2 · 𝑁)) = 1 ∧ 2 ∥ (2 · 𝑁))) → (𝑚 gcd 2) = 1) |
| 128 | 118, 119,
123, 124, 126, 127 | syl32anc 1380 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → (𝑚 gcd 2) = 1) |
| 129 | | prmrp 16749 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℙ ∧ 2 ∈
ℙ) → ((𝑚 gcd 2)
= 1 ↔ 𝑚 ≠
2)) |
| 130 | 116, 10, 129 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → ((𝑚 gcd 2) = 1 ↔ 𝑚 ≠ 2)) |
| 131 | 128, 130 | mpbid 232 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → 𝑚 ≠ 2) |
| 132 | | eldifsn 4786 |
. . . . . . . . 9
⊢ (𝑚 ∈ (ℙ ∖ {2})
↔ (𝑚 ∈ ℙ
∧ 𝑚 ≠
2)) |
| 133 | 116, 131,
132 | sylanbrc 583 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → 𝑚 ∈ (ℙ ∖
{2})) |
| 134 | | prmnn 16711 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℙ → 𝑚 ∈
ℕ) |
| 135 | 134 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → 𝑚 ∈ ℕ) |
| 136 | 2 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → 2 ∈
ℕ) |
| 137 | | rpmulgcd 16594 |
. . . . . . . . . 10
⊢ (((𝑚 ∈ ℕ ∧ 2 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ (𝑚 gcd 2) =
1) → (𝑚 gcd (2
· 𝑁)) = (𝑚 gcd 𝑁)) |
| 138 | 135, 136,
120, 128, 137 | syl31anc 1375 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → (𝑚 gcd (2 · 𝑁)) = (𝑚 gcd 𝑁)) |
| 139 | 138, 124 | eqtr3d 2779 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → (𝑚 gcd 𝑁) = 1) |
| 140 | 133, 139 | jca 511 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) |
| 141 | | lgsquad2lem2.f |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)))) |
| 142 | 140, 141 | syldan 591 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)))) |
| 143 | 142 | exp32 420 |
. . . . 5
⊢ (𝜑 → (𝑚 ∈ ℙ → ((𝑚 gcd (2 · 𝑁)) = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)))))) |
| 144 | 143 | com12 32 |
. . . 4
⊢ (𝑚 ∈ ℙ → (𝜑 → ((𝑚 gcd (2 · 𝑁)) = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)))))) |
| 145 | | jcab 517 |
. . . . 5
⊢ ((𝜑 → (((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2)))))) ↔ ((𝜑 → ((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2))))) ∧ (𝜑 → ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))))) |
| 146 | | simplrl 777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 ∧ (((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))))) → 𝑥 ∈
(ℤ≥‘2)) |
| 147 | | eluz2nn 12924 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
(ℤ≥‘2) → 𝑥 ∈ ℕ) |
| 148 | 146, 147 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 ∧ (((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))))) → 𝑥 ∈
ℕ) |
| 149 | | simplrr 778 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 ∧ (((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))))) → 𝑦 ∈
(ℤ≥‘2)) |
| 150 | | eluz2nn 12924 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈
(ℤ≥‘2) → 𝑦 ∈ ℕ) |
| 151 | 149, 150 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 ∧ (((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))))) → 𝑦 ∈
ℕ) |
| 152 | 148, 151 | nnmulcld 12319 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 ∧ (((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))))) → (𝑥 · 𝑦) ∈ ℕ) |
| 153 | | n2dvds1 16405 |
. . . . . . . . . . . 12
⊢ ¬ 2
∥ 1 |
| 154 | 93 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → 𝑁 ∈ ℤ) |
| 155 | 6, 154, 125 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → 2 ∥ (2 · 𝑁)) |
| 156 | | eluzelz 12888 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈
(ℤ≥‘2) → 𝑥 ∈ ℤ) |
| 157 | | eluzelz 12888 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈
(ℤ≥‘2) → 𝑦 ∈ ℤ) |
| 158 | 156, 157 | anim12i 613 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈
(ℤ≥‘2) ∧ 𝑦 ∈ (ℤ≥‘2))
→ (𝑥 ∈ ℤ
∧ 𝑦 ∈
ℤ)) |
| 159 | 158 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) |
| 160 | | zmulcl 12666 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 · 𝑦) ∈ ℤ) |
| 161 | 159, 160 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → (𝑥 · 𝑦) ∈ ℤ) |
| 162 | 6, 154, 122 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → (2 · 𝑁) ∈ ℤ) |
| 163 | | dvdsgcd 16581 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℤ ∧ (𝑥
· 𝑦) ∈ ℤ
∧ (2 · 𝑁) ∈
ℤ) → ((2 ∥ (𝑥 · 𝑦) ∧ 2 ∥ (2 · 𝑁)) → 2 ∥ ((𝑥 · 𝑦) gcd (2 · 𝑁)))) |
| 164 | 6, 161, 162, 163 | mp3an2i 1468 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → ((2 ∥ (𝑥 · 𝑦) ∧ 2 ∥ (2 · 𝑁)) → 2 ∥ ((𝑥 · 𝑦) gcd (2 · 𝑁)))) |
| 165 | 155, 164 | mpan2d 694 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → (2 ∥ (𝑥 · 𝑦) → 2 ∥ ((𝑥 · 𝑦) gcd (2 · 𝑁)))) |
| 166 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) |
| 167 | 166 | breq2d 5155 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → (2 ∥ ((𝑥 · 𝑦) gcd (2 · 𝑁)) ↔ 2 ∥ 1)) |
| 168 | 165, 167 | sylibd 239 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → (2 ∥ (𝑥 · 𝑦) → 2 ∥ 1)) |
| 169 | 153, 168 | mtoi 199 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → ¬ 2 ∥ (𝑥 · 𝑦)) |
| 170 | 169 | adantrr 717 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 ∧ (((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))))) → ¬ 2
∥ (𝑥 · 𝑦)) |
| 171 | 4 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 ∧ (((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))))) → 𝑁 ∈
ℕ) |
| 172 | | lgsquad2.4 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 2 ∥ 𝑁) |
| 173 | 172 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 ∧ (((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))))) → ¬ 2
∥ 𝑁) |
| 174 | | dvdsmul2 16316 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ) → 𝑁
∥ (2 · 𝑁)) |
| 175 | 6, 154, 174 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → 𝑁 ∥ (2 · 𝑁)) |
| 176 | | rpdvds 16697 |
. . . . . . . . . . . 12
⊢ ((((𝑥 · 𝑦) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (2 · 𝑁) ∈ ℤ) ∧ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 ∧ 𝑁 ∥ (2 · 𝑁))) → ((𝑥 · 𝑦) gcd 𝑁) = 1) |
| 177 | 161, 154,
162, 166, 175, 176 | syl32anc 1380 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → ((𝑥 · 𝑦) gcd 𝑁) = 1) |
| 178 | 177 | adantrr 717 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 ∧ (((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))))) → ((𝑥 · 𝑦) gcd 𝑁) = 1) |
| 179 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 ∧ (((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))))) → (𝑥 · 𝑦) = (𝑥 · 𝑦)) |
| 180 | 159 | simpld 494 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → 𝑥 ∈ ℤ) |
| 181 | 180, 162 | gcdcomd 16551 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → (𝑥 gcd (2 · 𝑁)) = ((2 · 𝑁) gcd 𝑥)) |
| 182 | 162, 161 | gcdcomd 16551 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → ((2 · 𝑁) gcd (𝑥 · 𝑦)) = ((𝑥 · 𝑦) gcd (2 · 𝑁))) |
| 183 | 182, 166 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → ((2 · 𝑁) gcd (𝑥 · 𝑦)) = 1) |
| 184 | | dvdsmul1 16315 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑥 ∥ (𝑥 · 𝑦)) |
| 185 | 159, 184 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → 𝑥 ∥ (𝑥 · 𝑦)) |
| 186 | | rpdvds 16697 |
. . . . . . . . . . . . . 14
⊢ ((((2
· 𝑁) ∈ ℤ
∧ 𝑥 ∈ ℤ
∧ (𝑥 · 𝑦) ∈ ℤ) ∧ (((2
· 𝑁) gcd (𝑥 · 𝑦)) = 1 ∧ 𝑥 ∥ (𝑥 · 𝑦))) → ((2 · 𝑁) gcd 𝑥) = 1) |
| 187 | 162, 180,
161, 183, 185, 186 | syl32anc 1380 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → ((2 · 𝑁) gcd 𝑥) = 1) |
| 188 | 181, 187 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → (𝑥 gcd (2 · 𝑁)) = 1) |
| 189 | 188 | adantrr 717 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 ∧ (((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))))) → (𝑥 gcd (2 · 𝑁)) = 1) |
| 190 | | simprrl 781 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 ∧ (((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))))) → ((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2))))) |
| 191 | 189, 190 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 ∧ (((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))))) → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) |
| 192 | 159 | simprd 495 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → 𝑦 ∈ ℤ) |
| 193 | 192, 162 | gcdcomd 16551 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → (𝑦 gcd (2 · 𝑁)) = ((2 · 𝑁) gcd 𝑦)) |
| 194 | | dvdsmul2 16316 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑦 ∥ (𝑥 · 𝑦)) |
| 195 | 159, 194 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → 𝑦 ∥ (𝑥 · 𝑦)) |
| 196 | | rpdvds 16697 |
. . . . . . . . . . . . . 14
⊢ ((((2
· 𝑁) ∈ ℤ
∧ 𝑦 ∈ ℤ
∧ (𝑥 · 𝑦) ∈ ℤ) ∧ (((2
· 𝑁) gcd (𝑥 · 𝑦)) = 1 ∧ 𝑦 ∥ (𝑥 · 𝑦))) → ((2 · 𝑁) gcd 𝑦) = 1) |
| 197 | 162, 192,
161, 183, 195, 196 | syl32anc 1380 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → ((2 · 𝑁) gcd 𝑦) = 1) |
| 198 | 193, 197 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → (𝑦 gcd (2 · 𝑁)) = 1) |
| 199 | 198 | adantrr 717 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 ∧ (((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))))) → (𝑦 gcd (2 · 𝑁)) = 1) |
| 200 | | simprrr 782 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 ∧ (((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))))) → ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))) |
| 201 | 199, 200 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 ∧ (((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))))) → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2)))) |
| 202 | 152, 170,
171, 173, 178, 148, 151, 179, 191, 201 | lgsquad2lem1 27428 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 ∧ (((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))))) → (((𝑥 · 𝑦) /L 𝑁) · (𝑁 /L (𝑥 · 𝑦))) = (-1↑((((𝑥 · 𝑦) − 1) / 2) · ((𝑁 − 1) /
2)))) |
| 203 | 202 | exp32 420 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) → (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 → ((((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))) → (((𝑥 · 𝑦) /L 𝑁) · (𝑁 /L (𝑥 · 𝑦))) = (-1↑((((𝑥 · 𝑦) − 1) / 2) · ((𝑁 − 1) /
2)))))) |
| 204 | 203 | com23 86 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) → ((((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))) → (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 → (((𝑥 · 𝑦) /L 𝑁) · (𝑁 /L (𝑥 · 𝑦))) = (-1↑((((𝑥 · 𝑦) − 1) / 2) · ((𝑁 − 1) /
2)))))) |
| 205 | 204 | expcom 413 |
. . . . . 6
⊢ ((𝑥 ∈
(ℤ≥‘2) ∧ 𝑦 ∈ (ℤ≥‘2))
→ (𝜑 → ((((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))) → (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 → (((𝑥 · 𝑦) /L 𝑁) · (𝑁 /L (𝑥 · 𝑦))) = (-1↑((((𝑥 · 𝑦) − 1) / 2) · ((𝑁 − 1) /
2))))))) |
| 206 | 205 | a2d 29 |
. . . . 5
⊢ ((𝑥 ∈
(ℤ≥‘2) ∧ 𝑦 ∈ (ℤ≥‘2))
→ ((𝜑 → (((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ∧ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2)))))) → (𝜑 → (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 → (((𝑥 · 𝑦) /L 𝑁) · (𝑁 /L (𝑥 · 𝑦))) = (-1↑((((𝑥 · 𝑦) − 1) / 2) · ((𝑁 − 1) /
2))))))) |
| 207 | 145, 206 | biimtrrid 243 |
. . . 4
⊢ ((𝑥 ∈
(ℤ≥‘2) ∧ 𝑦 ∈ (ℤ≥‘2))
→ (((𝜑 → ((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2))))) ∧ (𝜑 → ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2)))))) → (𝜑 → (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 → (((𝑥 · 𝑦) /L 𝑁) · (𝑁 /L (𝑥 · 𝑦))) = (-1↑((((𝑥 · 𝑦) − 1) / 2) · ((𝑁 − 1) /
2))))))) |
| 208 | 34, 46, 58, 70, 82, 115, 144, 207 | prmind 16723 |
. . 3
⊢ (𝑀 ∈ ℕ → (𝜑 → ((𝑀 gcd (2 · 𝑁)) = 1 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) /
2)))))) |
| 209 | 1, 208 | mpcom 38 |
. 2
⊢ (𝜑 → ((𝑀 gcd (2 · 𝑁)) = 1 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) /
2))))) |
| 210 | 18, 209 | mpd 15 |
1
⊢ (𝜑 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) /
2)))) |