| Step | Hyp | Ref
| Expression |
| 1 | | lgsquad2.1 |
. 2
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 2 | | lgsquad2.2 |
. 2
⊢ (𝜑 → ¬ 2 ∥ 𝑀) |
| 3 | | lgsquad2.3 |
. 2
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 4 | | lgsquad2.4 |
. 2
⊢ (𝜑 → ¬ 2 ∥ 𝑁) |
| 5 | | lgsquad2.5 |
. 2
⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) |
| 6 | 3 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑁 ∈ ℕ) |
| 7 | 4 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ¬ 2 ∥ 𝑁) |
| 8 | | simprl 771 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑚 ∈ (ℙ ∖
{2})) |
| 9 | | eldifi 4131 |
. . . . . 6
⊢ (𝑚 ∈ (ℙ ∖ {2})
→ 𝑚 ∈
ℙ) |
| 10 | 8, 9 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑚 ∈ ℙ) |
| 11 | | prmnn 16711 |
. . . . 5
⊢ (𝑚 ∈ ℙ → 𝑚 ∈
ℕ) |
| 12 | 10, 11 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑚 ∈ ℕ) |
| 13 | | eldifsni 4790 |
. . . . . . . 8
⊢ (𝑚 ∈ (ℙ ∖ {2})
→ 𝑚 ≠
2) |
| 14 | 8, 13 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑚 ≠ 2) |
| 15 | 14 | necomd 2996 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 2 ≠ 𝑚) |
| 16 | 15 | neneqd 2945 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ¬ 2 = 𝑚) |
| 17 | | 2z 12649 |
. . . . . . 7
⊢ 2 ∈
ℤ |
| 18 | | uzid 12893 |
. . . . . . 7
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
| 19 | 17, 18 | ax-mp 5 |
. . . . . 6
⊢ 2 ∈
(ℤ≥‘2) |
| 20 | | dvdsprm 16740 |
. . . . . 6
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝑚 ∈ ℙ) → (2 ∥ 𝑚 ↔ 2 = 𝑚)) |
| 21 | 19, 10, 20 | sylancr 587 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (2 ∥ 𝑚 ↔ 2 = 𝑚)) |
| 22 | 16, 21 | mtbird 325 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ¬ 2 ∥ 𝑚) |
| 23 | 6 | nnzd 12640 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑁 ∈ ℤ) |
| 24 | 12 | nnzd 12640 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑚 ∈ ℤ) |
| 25 | 23, 24 | gcdcomd 16551 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑁 gcd 𝑚) = (𝑚 gcd 𝑁)) |
| 26 | | simprr 773 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑚 gcd 𝑁) = 1) |
| 27 | 25, 26 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑁 gcd 𝑚) = 1) |
| 28 | | simprl 771 |
. . . . 5
⊢ (((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) ∧ (𝑛 ∈ (ℙ ∖ {2}) ∧ (𝑛 gcd 𝑚) = 1)) → 𝑛 ∈ (ℙ ∖
{2})) |
| 29 | 8 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) ∧ (𝑛 ∈ (ℙ ∖ {2}) ∧ (𝑛 gcd 𝑚) = 1)) → 𝑚 ∈ (ℙ ∖
{2})) |
| 30 | | eldifi 4131 |
. . . . . . . 8
⊢ (𝑛 ∈ (ℙ ∖ {2})
→ 𝑛 ∈
ℙ) |
| 31 | | prmrp 16749 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℙ ∧ 𝑚 ∈ ℙ) → ((𝑛 gcd 𝑚) = 1 ↔ 𝑛 ≠ 𝑚)) |
| 32 | 30, 10, 31 | syl2anr 597 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) ∧ 𝑛 ∈ (ℙ ∖ {2})) → ((𝑛 gcd 𝑚) = 1 ↔ 𝑛 ≠ 𝑚)) |
| 33 | 32 | biimpd 229 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) ∧ 𝑛 ∈ (ℙ ∖ {2})) → ((𝑛 gcd 𝑚) = 1 → 𝑛 ≠ 𝑚)) |
| 34 | 33 | impr 454 |
. . . . 5
⊢ (((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) ∧ (𝑛 ∈ (ℙ ∖ {2}) ∧ (𝑛 gcd 𝑚) = 1)) → 𝑛 ≠ 𝑚) |
| 35 | | lgsquad 27427 |
. . . . 5
⊢ ((𝑛 ∈ (ℙ ∖ {2})
∧ 𝑚 ∈ (ℙ
∖ {2}) ∧ 𝑛 ≠
𝑚) → ((𝑛 /L 𝑚) · (𝑚 /L 𝑛)) = (-1↑(((𝑛 − 1) / 2) · ((𝑚 − 1) /
2)))) |
| 36 | 28, 29, 34, 35 | syl3anc 1373 |
. . . 4
⊢ (((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) ∧ (𝑛 ∈ (ℙ ∖ {2}) ∧ (𝑛 gcd 𝑚) = 1)) → ((𝑛 /L 𝑚) · (𝑚 /L 𝑛)) = (-1↑(((𝑛 − 1) / 2) · ((𝑚 − 1) /
2)))) |
| 37 | | biid 261 |
. . . 4
⊢
(∀𝑥 ∈
(1...𝑦)((𝑥 gcd (2 · 𝑚)) = 1 → ((𝑥 /L 𝑚) · (𝑚 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑚 − 1) / 2)))) ↔
∀𝑥 ∈ (1...𝑦)((𝑥 gcd (2 · 𝑚)) = 1 → ((𝑥 /L 𝑚) · (𝑚 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑚 − 1) /
2))))) |
| 38 | 6, 7, 12, 22, 27, 36, 37 | lgsquad2lem2 27429 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ((𝑁 /L 𝑚) · (𝑚 /L 𝑁)) = (-1↑(((𝑁 − 1) / 2) · ((𝑚 − 1) /
2)))) |
| 39 | | lgscl 27355 |
. . . . 5
⊢ ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑚 /L 𝑁) ∈
ℤ) |
| 40 | 24, 23, 39 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑚 /L 𝑁) ∈ ℤ) |
| 41 | | lgscl 27355 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑁 /L 𝑚) ∈
ℤ) |
| 42 | 23, 24, 41 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑁 /L 𝑚) ∈ ℤ) |
| 43 | | zcn 12618 |
. . . . 5
⊢ ((𝑚 /L 𝑁) ∈ ℤ → (𝑚 /L 𝑁) ∈
ℂ) |
| 44 | | zcn 12618 |
. . . . 5
⊢ ((𝑁 /L 𝑚) ∈ ℤ → (𝑁 /L 𝑚) ∈
ℂ) |
| 45 | | mulcom 11241 |
. . . . 5
⊢ (((𝑚 /L 𝑁) ∈ ℂ ∧ (𝑁 /L 𝑚) ∈ ℂ) → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = ((𝑁 /L 𝑚) · (𝑚 /L 𝑁))) |
| 46 | 43, 44, 45 | syl2an 596 |
. . . 4
⊢ (((𝑚 /L 𝑁) ∈ ℤ ∧ (𝑁 /L 𝑚) ∈ ℤ) → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = ((𝑁 /L 𝑚) · (𝑚 /L 𝑁))) |
| 47 | 40, 42, 46 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = ((𝑁 /L 𝑚) · (𝑚 /L 𝑁))) |
| 48 | 12 | nncnd 12282 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑚 ∈ ℂ) |
| 49 | | ax-1cn 11213 |
. . . . . . 7
⊢ 1 ∈
ℂ |
| 50 | | subcl 11507 |
. . . . . . 7
⊢ ((𝑚 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑚 −
1) ∈ ℂ) |
| 51 | 48, 49, 50 | sylancl 586 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑚 − 1) ∈ ℂ) |
| 52 | 51 | halfcld 12511 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ((𝑚 − 1) / 2) ∈
ℂ) |
| 53 | 6 | nncnd 12282 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑁 ∈ ℂ) |
| 54 | | subcl 11507 |
. . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑁 −
1) ∈ ℂ) |
| 55 | 53, 49, 54 | sylancl 586 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑁 − 1) ∈ ℂ) |
| 56 | 55 | halfcld 12511 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ((𝑁 − 1) / 2) ∈
ℂ) |
| 57 | 52, 56 | mulcomd 11282 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)) = (((𝑁 − 1) / 2) · ((𝑚 − 1) /
2))) |
| 58 | 57 | oveq2d 7447 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (-1↑(((𝑚 − 1) / 2) ·
((𝑁 − 1) / 2))) =
(-1↑(((𝑁 − 1) /
2) · ((𝑚 − 1)
/ 2)))) |
| 59 | 38, 47, 58 | 3eqtr4d 2787 |
. 2
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)))) |
| 60 | | biid 261 |
. 2
⊢
(∀𝑥 ∈
(1...𝑦)((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ↔ ∀𝑥 ∈ (1...𝑦)((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2))))) |
| 61 | 1, 2, 3, 4, 5, 59,
60 | lgsquad2lem2 27429 |
1
⊢ (𝜑 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) /
2)))) |