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 473 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑁 ∈ ℕ) |
7 | 4 | adantr 473 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ¬ 2 ∥ 𝑁) |
8 | | simprl 759 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑚 ∈ (ℙ ∖
{2})) |
9 | | eldifi 3988 |
. . . . . 6
⊢ (𝑚 ∈ (ℙ ∖ {2})
→ 𝑚 ∈
ℙ) |
10 | 8, 9 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑚 ∈ ℙ) |
11 | | prmnn 15873 |
. . . . 5
⊢ (𝑚 ∈ ℙ → 𝑚 ∈
ℕ) |
12 | 10, 11 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑚 ∈ ℕ) |
13 | | eldifsni 4593 |
. . . . . . . 8
⊢ (𝑚 ∈ (ℙ ∖ {2})
→ 𝑚 ≠
2) |
14 | 8, 13 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑚 ≠ 2) |
15 | 14 | necomd 3017 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 2 ≠ 𝑚) |
16 | 15 | neneqd 2967 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ¬ 2 = 𝑚) |
17 | | 2z 11826 |
. . . . . . 7
⊢ 2 ∈
ℤ |
18 | | uzid 12072 |
. . . . . . 7
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
19 | 17, 18 | ax-mp 5 |
. . . . . 6
⊢ 2 ∈
(ℤ≥‘2) |
20 | | dvdsprm 15902 |
. . . . . 6
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝑚 ∈ ℙ) → (2 ∥ 𝑚 ↔ 2 = 𝑚)) |
21 | 19, 10, 20 | sylancr 579 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (2 ∥ 𝑚 ↔ 2 = 𝑚)) |
22 | 16, 21 | mtbird 317 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ¬ 2 ∥ 𝑚) |
23 | 6 | nnzd 11898 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑁 ∈ ℤ) |
24 | 12 | nnzd 11898 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑚 ∈ ℤ) |
25 | | gcdcom 15721 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑁 gcd 𝑚) = (𝑚 gcd 𝑁)) |
26 | 23, 24, 25 | syl2anc 576 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑁 gcd 𝑚) = (𝑚 gcd 𝑁)) |
27 | | simprr 761 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑚 gcd 𝑁) = 1) |
28 | 26, 27 | eqtrd 2809 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑁 gcd 𝑚) = 1) |
29 | | simprl 759 |
. . . . 5
⊢ (((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) ∧ (𝑛 ∈ (ℙ ∖ {2}) ∧ (𝑛 gcd 𝑚) = 1)) → 𝑛 ∈ (ℙ ∖
{2})) |
30 | 8 | adantr 473 |
. . . . 5
⊢ (((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) ∧ (𝑛 ∈ (ℙ ∖ {2}) ∧ (𝑛 gcd 𝑚) = 1)) → 𝑚 ∈ (ℙ ∖
{2})) |
31 | | eldifi 3988 |
. . . . . . . 8
⊢ (𝑛 ∈ (ℙ ∖ {2})
→ 𝑛 ∈
ℙ) |
32 | | prmrp 15911 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℙ ∧ 𝑚 ∈ ℙ) → ((𝑛 gcd 𝑚) = 1 ↔ 𝑛 ≠ 𝑚)) |
33 | 31, 10, 32 | syl2anr 588 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) ∧ 𝑛 ∈ (ℙ ∖ {2})) → ((𝑛 gcd 𝑚) = 1 ↔ 𝑛 ≠ 𝑚)) |
34 | 33 | biimpd 221 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) ∧ 𝑛 ∈ (ℙ ∖ {2})) → ((𝑛 gcd 𝑚) = 1 → 𝑛 ≠ 𝑚)) |
35 | 34 | impr 447 |
. . . . 5
⊢ (((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) ∧ (𝑛 ∈ (ℙ ∖ {2}) ∧ (𝑛 gcd 𝑚) = 1)) → 𝑛 ≠ 𝑚) |
36 | | lgsquad 25677 |
. . . . 5
⊢ ((𝑛 ∈ (ℙ ∖ {2})
∧ 𝑚 ∈ (ℙ
∖ {2}) ∧ 𝑛 ≠
𝑚) → ((𝑛 /L 𝑚) · (𝑚 /L 𝑛)) = (-1↑(((𝑛 − 1) / 2) · ((𝑚 − 1) /
2)))) |
37 | 29, 30, 35, 36 | syl3anc 1352 |
. . . 4
⊢ (((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) ∧ (𝑛 ∈ (ℙ ∖ {2}) ∧ (𝑛 gcd 𝑚) = 1)) → ((𝑛 /L 𝑚) · (𝑚 /L 𝑛)) = (-1↑(((𝑛 − 1) / 2) · ((𝑚 − 1) /
2)))) |
38 | | biid 253 |
. . . 4
⊢
(∀𝑥 ∈
(1...𝑦)((𝑥 gcd (2 · 𝑚)) = 1 → ((𝑥 /L 𝑚) · (𝑚 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑚 − 1) / 2)))) ↔
∀𝑥 ∈ (1...𝑦)((𝑥 gcd (2 · 𝑚)) = 1 → ((𝑥 /L 𝑚) · (𝑚 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑚 − 1) /
2))))) |
39 | 6, 7, 12, 22, 28, 37, 38 | lgsquad2lem2 25679 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ((𝑁 /L 𝑚) · (𝑚 /L 𝑁)) = (-1↑(((𝑁 − 1) / 2) · ((𝑚 − 1) /
2)))) |
40 | | lgscl 25605 |
. . . . 5
⊢ ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑚 /L 𝑁) ∈
ℤ) |
41 | 24, 23, 40 | syl2anc 576 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑚 /L 𝑁) ∈ ℤ) |
42 | | lgscl 25605 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑁 /L 𝑚) ∈
ℤ) |
43 | 23, 24, 42 | syl2anc 576 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑁 /L 𝑚) ∈ ℤ) |
44 | | zcn 11797 |
. . . . 5
⊢ ((𝑚 /L 𝑁) ∈ ℤ → (𝑚 /L 𝑁) ∈
ℂ) |
45 | | zcn 11797 |
. . . . 5
⊢ ((𝑁 /L 𝑚) ∈ ℤ → (𝑁 /L 𝑚) ∈
ℂ) |
46 | | mulcom 10420 |
. . . . 5
⊢ (((𝑚 /L 𝑁) ∈ ℂ ∧ (𝑁 /L 𝑚) ∈ ℂ) → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = ((𝑁 /L 𝑚) · (𝑚 /L 𝑁))) |
47 | 44, 45, 46 | syl2an 587 |
. . . 4
⊢ (((𝑚 /L 𝑁) ∈ ℤ ∧ (𝑁 /L 𝑚) ∈ ℤ) → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = ((𝑁 /L 𝑚) · (𝑚 /L 𝑁))) |
48 | 41, 43, 47 | syl2anc 576 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = ((𝑁 /L 𝑚) · (𝑚 /L 𝑁))) |
49 | 12 | nncnd 11456 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑚 ∈ ℂ) |
50 | | ax-1cn 10392 |
. . . . . . 7
⊢ 1 ∈
ℂ |
51 | | subcl 10684 |
. . . . . . 7
⊢ ((𝑚 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑚 −
1) ∈ ℂ) |
52 | 49, 50, 51 | sylancl 578 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑚 − 1) ∈ ℂ) |
53 | 52 | halfcld 11691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ((𝑚 − 1) / 2) ∈
ℂ) |
54 | 6 | nncnd 11456 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑁 ∈ ℂ) |
55 | | subcl 10684 |
. . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑁 −
1) ∈ ℂ) |
56 | 54, 50, 55 | sylancl 578 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑁 − 1) ∈ ℂ) |
57 | 56 | halfcld 11691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ((𝑁 − 1) / 2) ∈
ℂ) |
58 | 53, 57 | mulcomd 10460 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)) = (((𝑁 − 1) / 2) · ((𝑚 − 1) /
2))) |
59 | 58 | oveq2d 6991 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (-1↑(((𝑚 − 1) / 2) ·
((𝑁 − 1) / 2))) =
(-1↑(((𝑁 − 1) /
2) · ((𝑚 − 1)
/ 2)))) |
60 | 39, 48, 59 | 3eqtr4d 2819 |
. 2
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)))) |
61 | | biid 253 |
. 2
⊢
(∀𝑥 ∈
(1...𝑦)((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))) ↔ ∀𝑥 ∈ (1...𝑦)((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2))))) |
62 | 1, 2, 3, 4, 5, 60,
61 | lgsquad2lem2 25679 |
1
⊢ (𝜑 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) /
2)))) |