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 483 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑁 ∈ ℕ) |
7 | 4 | adantr 483 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ¬ 2 ∥ 𝑁) |
8 | | simprl 769 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑚 ∈ (ℙ ∖
{2})) |
9 | | eldifi 4102 |
. . . . . 6
⊢ (𝑚 ∈ (ℙ ∖ {2})
→ 𝑚 ∈
ℙ) |
10 | 8, 9 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑚 ∈ ℙ) |
11 | | prmnn 16017 |
. . . . 5
⊢ (𝑚 ∈ ℙ → 𝑚 ∈
ℕ) |
12 | 10, 11 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑚 ∈ ℕ) |
13 | | eldifsni 4721 |
. . . . . . . 8
⊢ (𝑚 ∈ (ℙ ∖ {2})
→ 𝑚 ≠
2) |
14 | 8, 13 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑚 ≠ 2) |
15 | 14 | necomd 3071 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 2 ≠ 𝑚) |
16 | 15 | neneqd 3021 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ¬ 2 = 𝑚) |
17 | | 2z 12013 |
. . . . . . 7
⊢ 2 ∈
ℤ |
18 | | uzid 12257 |
. . . . . . 7
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
19 | 17, 18 | ax-mp 5 |
. . . . . 6
⊢ 2 ∈
(ℤ≥‘2) |
20 | | dvdsprm 16046 |
. . . . . 6
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝑚 ∈ ℙ) → (2 ∥ 𝑚 ↔ 2 = 𝑚)) |
21 | 19, 10, 20 | sylancr 589 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (2 ∥ 𝑚 ↔ 2 = 𝑚)) |
22 | 16, 21 | mtbird 327 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ¬ 2 ∥ 𝑚) |
23 | 6 | nnzd 12085 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑁 ∈ ℤ) |
24 | 12 | nnzd 12085 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑚 ∈ ℤ) |
25 | | gcdcom 15861 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑁 gcd 𝑚) = (𝑚 gcd 𝑁)) |
26 | 23, 24, 25 | syl2anc 586 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑁 gcd 𝑚) = (𝑚 gcd 𝑁)) |
27 | | simprr 771 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑚 gcd 𝑁) = 1) |
28 | 26, 27 | eqtrd 2856 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑁 gcd 𝑚) = 1) |
29 | | simprl 769 |
. . . . 5
⊢ (((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) ∧ (𝑛 ∈ (ℙ ∖ {2}) ∧ (𝑛 gcd 𝑚) = 1)) → 𝑛 ∈ (ℙ ∖
{2})) |
30 | 8 | adantr 483 |
. . . . 5
⊢ (((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) ∧ (𝑛 ∈ (ℙ ∖ {2}) ∧ (𝑛 gcd 𝑚) = 1)) → 𝑚 ∈ (ℙ ∖
{2})) |
31 | | eldifi 4102 |
. . . . . . . 8
⊢ (𝑛 ∈ (ℙ ∖ {2})
→ 𝑛 ∈
ℙ) |
32 | | prmrp 16055 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℙ ∧ 𝑚 ∈ ℙ) → ((𝑛 gcd 𝑚) = 1 ↔ 𝑛 ≠ 𝑚)) |
33 | 31, 10, 32 | syl2anr 598 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) ∧ 𝑛 ∈ (ℙ ∖ {2})) → ((𝑛 gcd 𝑚) = 1 ↔ 𝑛 ≠ 𝑚)) |
34 | 33 | biimpd 231 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) ∧ 𝑛 ∈ (ℙ ∖ {2})) → ((𝑛 gcd 𝑚) = 1 → 𝑛 ≠ 𝑚)) |
35 | 34 | impr 457 |
. . . . 5
⊢ (((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) ∧ (𝑛 ∈ (ℙ ∖ {2}) ∧ (𝑛 gcd 𝑚) = 1)) → 𝑛 ≠ 𝑚) |
36 | | lgsquad 25958 |
. . . . 5
⊢ ((𝑛 ∈ (ℙ ∖ {2})
∧ 𝑚 ∈ (ℙ
∖ {2}) ∧ 𝑛 ≠
𝑚) → ((𝑛 /L 𝑚) · (𝑚 /L 𝑛)) = (-1↑(((𝑛 − 1) / 2) · ((𝑚 − 1) /
2)))) |
37 | 29, 30, 35, 36 | syl3anc 1367 |
. . . 4
⊢ (((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) ∧ (𝑛 ∈ (ℙ ∖ {2}) ∧ (𝑛 gcd 𝑚) = 1)) → ((𝑛 /L 𝑚) · (𝑚 /L 𝑛)) = (-1↑(((𝑛 − 1) / 2) · ((𝑚 − 1) /
2)))) |
38 | | biid 263 |
. . . 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 25960 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ((𝑁 /L 𝑚) · (𝑚 /L 𝑁)) = (-1↑(((𝑁 − 1) / 2) · ((𝑚 − 1) /
2)))) |
40 | | lgscl 25886 |
. . . . 5
⊢ ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑚 /L 𝑁) ∈
ℤ) |
41 | 24, 23, 40 | syl2anc 586 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑚 /L 𝑁) ∈ ℤ) |
42 | | lgscl 25886 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑁 /L 𝑚) ∈
ℤ) |
43 | 23, 24, 42 | syl2anc 586 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑁 /L 𝑚) ∈ ℤ) |
44 | | zcn 11985 |
. . . . 5
⊢ ((𝑚 /L 𝑁) ∈ ℤ → (𝑚 /L 𝑁) ∈
ℂ) |
45 | | zcn 11985 |
. . . . 5
⊢ ((𝑁 /L 𝑚) ∈ ℤ → (𝑁 /L 𝑚) ∈
ℂ) |
46 | | mulcom 10622 |
. . . . 5
⊢ (((𝑚 /L 𝑁) ∈ ℂ ∧ (𝑁 /L 𝑚) ∈ ℂ) → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = ((𝑁 /L 𝑚) · (𝑚 /L 𝑁))) |
47 | 44, 45, 46 | syl2an 597 |
. . . 4
⊢ (((𝑚 /L 𝑁) ∈ ℤ ∧ (𝑁 /L 𝑚) ∈ ℤ) → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = ((𝑁 /L 𝑚) · (𝑚 /L 𝑁))) |
48 | 41, 43, 47 | syl2anc 586 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = ((𝑁 /L 𝑚) · (𝑚 /L 𝑁))) |
49 | 12 | nncnd 11653 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑚 ∈ ℂ) |
50 | | ax-1cn 10594 |
. . . . . . 7
⊢ 1 ∈
ℂ |
51 | | subcl 10884 |
. . . . . . 7
⊢ ((𝑚 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑚 −
1) ∈ ℂ) |
52 | 49, 50, 51 | sylancl 588 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑚 − 1) ∈ ℂ) |
53 | 52 | halfcld 11881 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ((𝑚 − 1) / 2) ∈
ℂ) |
54 | 6 | nncnd 11653 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → 𝑁 ∈ ℂ) |
55 | | subcl 10884 |
. . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑁 −
1) ∈ ℂ) |
56 | 54, 50, 55 | sylancl 588 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (𝑁 − 1) ∈ ℂ) |
57 | 56 | halfcld 11881 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ((𝑁 − 1) / 2) ∈
ℂ) |
58 | 53, 57 | mulcomd 10661 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)) = (((𝑁 − 1) / 2) · ((𝑚 − 1) /
2))) |
59 | 58 | oveq2d 7171 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → (-1↑(((𝑚 − 1) / 2) ·
((𝑁 − 1) / 2))) =
(-1↑(((𝑁 − 1) /
2) · ((𝑚 − 1)
/ 2)))) |
60 | 39, 48, 59 | 3eqtr4d 2866 |
. 2
⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)))) |
61 | | biid 263 |
. 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 25960 |
1
⊢ (𝜑 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) /
2)))) |