Step | Hyp | Ref
| Expression |
1 | | lgsquad2.1 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) |
2 | | 2nn 11789 |
. . . . 5
⊢ 2 ∈
ℕ |
3 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → 2 ∈
ℕ) |
4 | | lgsquad2.3 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℕ) |
5 | 1 | nnzd 12167 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
6 | | 2z 12095 |
. . . . . 6
⊢ 2 ∈
ℤ |
7 | | gcdcom 15956 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 2 ∈
ℤ) → (𝑀 gcd 2) =
(2 gcd 𝑀)) |
8 | 5, 6, 7 | sylancl 589 |
. . . . 5
⊢ (𝜑 → (𝑀 gcd 2) = (2 gcd 𝑀)) |
9 | | lgsquad2.2 |
. . . . . 6
⊢ (𝜑 → ¬ 2 ∥ 𝑀) |
10 | | 2prm 16133 |
. . . . . . 7
⊢ 2 ∈
ℙ |
11 | | coprm 16152 |
. . . . . . 7
⊢ ((2
∈ ℙ ∧ 𝑀
∈ ℤ) → (¬ 2 ∥ 𝑀 ↔ (2 gcd 𝑀) = 1)) |
12 | 10, 5, 11 | sylancr 590 |
. . . . . 6
⊢ (𝜑 → (¬ 2 ∥ 𝑀 ↔ (2 gcd 𝑀) = 1)) |
13 | 9, 12 | mpbid 235 |
. . . . 5
⊢ (𝜑 → (2 gcd 𝑀) = 1) |
14 | 8, 13 | eqtrd 2773 |
. . . 4
⊢ (𝜑 → (𝑀 gcd 2) = 1) |
15 | | rpmulgcd 16002 |
. . . 4
⊢ (((𝑀 ∈ ℕ ∧ 2 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ (𝑀 gcd 2) =
1) → (𝑀 gcd (2
· 𝑁)) = (𝑀 gcd 𝑁)) |
16 | 1, 3, 4, 14, 15 | syl31anc 1374 |
. . 3
⊢ (𝜑 → (𝑀 gcd (2 · 𝑁)) = (𝑀 gcd 𝑁)) |
17 | | lgsquad2.5 |
. . 3
⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) |
18 | 16, 17 | eqtrd 2773 |
. 2
⊢ (𝜑 → (𝑀 gcd (2 · 𝑁)) = 1) |
19 | | oveq1 7177 |
. . . . . . . 8
⊢ (𝑚 = 1 → (𝑚 /L 𝑁) = (1 /L 𝑁)) |
20 | | oveq2 7178 |
. . . . . . . 8
⊢ (𝑚 = 1 → (𝑁 /L 𝑚) = (𝑁 /L 1)) |
21 | 19, 20 | oveq12d 7188 |
. . . . . . 7
⊢ (𝑚 = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = ((1 /L 𝑁) · (𝑁 /L 1))) |
22 | | oveq1 7177 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → (𝑚 − 1) = (1 − 1)) |
23 | | 1m1e0 11788 |
. . . . . . . . . . . 12
⊢ (1
− 1) = 0 |
24 | 22, 23 | eqtrdi 2789 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → (𝑚 − 1) = 0) |
25 | 24 | oveq1d 7185 |
. . . . . . . . . 10
⊢ (𝑚 = 1 → ((𝑚 − 1) / 2) = (0 / 2)) |
26 | | 2cn 11791 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
27 | | 2ne0 11820 |
. . . . . . . . . . 11
⊢ 2 ≠
0 |
28 | 26, 27 | div0i 11452 |
. . . . . . . . . 10
⊢ (0 / 2) =
0 |
29 | 25, 28 | eqtrdi 2789 |
. . . . . . . . 9
⊢ (𝑚 = 1 → ((𝑚 − 1) / 2) = 0) |
30 | 29 | oveq1d 7185 |
. . . . . . . 8
⊢ (𝑚 = 1 → (((𝑚 − 1) / 2) ·
((𝑁 − 1) / 2)) = (0
· ((𝑁 − 1) /
2))) |
31 | 30 | oveq2d 7186 |
. . . . . . 7
⊢ (𝑚 = 1 → (-1↑(((𝑚 − 1) / 2) ·
((𝑁 − 1) / 2))) =
(-1↑(0 · ((𝑁
− 1) / 2)))) |
32 | 21, 31 | eqeq12d 2754 |
. . . . . 6
⊢ (𝑚 = 1 → (((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))) ↔ ((1
/L 𝑁)
· (𝑁
/L 1)) = (-1↑(0 · ((𝑁 − 1) / 2))))) |
33 | 32 | imbi2d 344 |
. . . . 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 344 |
. . . 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 7177 |
. . . . . . 7
⊢ (𝑚 = 𝑥 → (𝑚 gcd (2 · 𝑁)) = (𝑥 gcd (2 · 𝑁))) |
36 | 35 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑚 = 𝑥 → ((𝑚 gcd (2 · 𝑁)) = 1 ↔ (𝑥 gcd (2 · 𝑁)) = 1)) |
37 | | oveq1 7177 |
. . . . . . . 8
⊢ (𝑚 = 𝑥 → (𝑚 /L 𝑁) = (𝑥 /L 𝑁)) |
38 | | oveq2 7178 |
. . . . . . . 8
⊢ (𝑚 = 𝑥 → (𝑁 /L 𝑚) = (𝑁 /L 𝑥)) |
39 | 37, 38 | oveq12d 7188 |
. . . . . . 7
⊢ (𝑚 = 𝑥 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = ((𝑥 /L 𝑁) · (𝑁 /L 𝑥))) |
40 | | oveq1 7177 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑥 → (𝑚 − 1) = (𝑥 − 1)) |
41 | 40 | oveq1d 7185 |
. . . . . . . . 9
⊢ (𝑚 = 𝑥 → ((𝑚 − 1) / 2) = ((𝑥 − 1) / 2)) |
42 | 41 | oveq1d 7185 |
. . . . . . . 8
⊢ (𝑚 = 𝑥 → (((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)) = (((𝑥 − 1) / 2) · ((𝑁 − 1) / 2))) |
43 | 42 | oveq2d 7186 |
. . . . . . 7
⊢ (𝑚 = 𝑥 → (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))) = (-1↑(((𝑥 − 1) / 2) ·
((𝑁 − 1) /
2)))) |
44 | 39, 43 | eqeq12d 2754 |
. . . . . 6
⊢ (𝑚 = 𝑥 → (((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))) ↔ ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2))))) |
45 | 36, 44 | imbi12d 348 |
. . . . 5
⊢ (𝑚 = 𝑥 → (((𝑚 gcd (2 · 𝑁)) = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)))) ↔ ((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))))) |
46 | 45 | imbi2d 344 |
. . . 4
⊢ (𝑚 = 𝑥 → ((𝜑 → ((𝑚 gcd (2 · 𝑁)) = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))))) ↔ (𝜑 → ((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2))))))) |
47 | | oveq1 7177 |
. . . . . . 7
⊢ (𝑚 = 𝑦 → (𝑚 gcd (2 · 𝑁)) = (𝑦 gcd (2 · 𝑁))) |
48 | 47 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑚 = 𝑦 → ((𝑚 gcd (2 · 𝑁)) = 1 ↔ (𝑦 gcd (2 · 𝑁)) = 1)) |
49 | | oveq1 7177 |
. . . . . . . 8
⊢ (𝑚 = 𝑦 → (𝑚 /L 𝑁) = (𝑦 /L 𝑁)) |
50 | | oveq2 7178 |
. . . . . . . 8
⊢ (𝑚 = 𝑦 → (𝑁 /L 𝑚) = (𝑁 /L 𝑦)) |
51 | 49, 50 | oveq12d 7188 |
. . . . . . 7
⊢ (𝑚 = 𝑦 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = ((𝑦 /L 𝑁) · (𝑁 /L 𝑦))) |
52 | | oveq1 7177 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑦 → (𝑚 − 1) = (𝑦 − 1)) |
53 | 52 | oveq1d 7185 |
. . . . . . . . 9
⊢ (𝑚 = 𝑦 → ((𝑚 − 1) / 2) = ((𝑦 − 1) / 2)) |
54 | 53 | oveq1d 7185 |
. . . . . . . 8
⊢ (𝑚 = 𝑦 → (((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)) = (((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))) |
55 | 54 | oveq2d 7186 |
. . . . . . 7
⊢ (𝑚 = 𝑦 → (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))) = (-1↑(((𝑦 − 1) / 2) ·
((𝑁 − 1) /
2)))) |
56 | 51, 55 | eqeq12d 2754 |
. . . . . 6
⊢ (𝑚 = 𝑦 → (((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))) ↔ ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))) |
57 | 48, 56 | imbi12d 348 |
. . . . 5
⊢ (𝑚 = 𝑦 → (((𝑚 gcd (2 · 𝑁)) = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)))) ↔ ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2)))))) |
58 | 57 | imbi2d 344 |
. . . 4
⊢ (𝑚 = 𝑦 → ((𝜑 → ((𝑚 gcd (2 · 𝑁)) = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))))) ↔ (𝜑 → ((𝑦 gcd (2 · 𝑁)) = 1 → ((𝑦 /L 𝑁) · (𝑁 /L 𝑦)) = (-1↑(((𝑦 − 1) / 2) · ((𝑁 − 1) / 2))))))) |
59 | | oveq1 7177 |
. . . . . . 7
⊢ (𝑚 = (𝑥 · 𝑦) → (𝑚 gcd (2 · 𝑁)) = ((𝑥 · 𝑦) gcd (2 · 𝑁))) |
60 | 59 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑚 = (𝑥 · 𝑦) → ((𝑚 gcd (2 · 𝑁)) = 1 ↔ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1)) |
61 | | oveq1 7177 |
. . . . . . . 8
⊢ (𝑚 = (𝑥 · 𝑦) → (𝑚 /L 𝑁) = ((𝑥 · 𝑦) /L 𝑁)) |
62 | | oveq2 7178 |
. . . . . . . 8
⊢ (𝑚 = (𝑥 · 𝑦) → (𝑁 /L 𝑚) = (𝑁 /L (𝑥 · 𝑦))) |
63 | 61, 62 | oveq12d 7188 |
. . . . . . 7
⊢ (𝑚 = (𝑥 · 𝑦) → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (((𝑥 · 𝑦) /L 𝑁) · (𝑁 /L (𝑥 · 𝑦)))) |
64 | | oveq1 7177 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑥 · 𝑦) → (𝑚 − 1) = ((𝑥 · 𝑦) − 1)) |
65 | 64 | oveq1d 7185 |
. . . . . . . . 9
⊢ (𝑚 = (𝑥 · 𝑦) → ((𝑚 − 1) / 2) = (((𝑥 · 𝑦) − 1) / 2)) |
66 | 65 | oveq1d 7185 |
. . . . . . . 8
⊢ (𝑚 = (𝑥 · 𝑦) → (((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)) = ((((𝑥 · 𝑦) − 1) / 2) · ((𝑁 − 1) /
2))) |
67 | 66 | oveq2d 7186 |
. . . . . . 7
⊢ (𝑚 = (𝑥 · 𝑦) → (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))) = (-1↑((((𝑥 · 𝑦) − 1) / 2) · ((𝑁 − 1) /
2)))) |
68 | 63, 67 | eqeq12d 2754 |
. . . . . 6
⊢ (𝑚 = (𝑥 · 𝑦) → (((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))) ↔ (((𝑥 · 𝑦) /L 𝑁) · (𝑁 /L (𝑥 · 𝑦))) = (-1↑((((𝑥 · 𝑦) − 1) / 2) · ((𝑁 − 1) /
2))))) |
69 | 60, 68 | imbi12d 348 |
. . . . 5
⊢ (𝑚 = (𝑥 · 𝑦) → (((𝑚 gcd (2 · 𝑁)) = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)))) ↔ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 → (((𝑥 · 𝑦) /L 𝑁) · (𝑁 /L (𝑥 · 𝑦))) = (-1↑((((𝑥 · 𝑦) − 1) / 2) · ((𝑁 − 1) /
2)))))) |
70 | 69 | imbi2d 344 |
. . . 4
⊢ (𝑚 = (𝑥 · 𝑦) → ((𝜑 → ((𝑚 gcd (2 · 𝑁)) = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))))) ↔ (𝜑 → (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 → (((𝑥 · 𝑦) /L 𝑁) · (𝑁 /L (𝑥 · 𝑦))) = (-1↑((((𝑥 · 𝑦) − 1) / 2) · ((𝑁 − 1) /
2))))))) |
71 | | oveq1 7177 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (𝑚 gcd (2 · 𝑁)) = (𝑀 gcd (2 · 𝑁))) |
72 | 71 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑚 = 𝑀 → ((𝑚 gcd (2 · 𝑁)) = 1 ↔ (𝑀 gcd (2 · 𝑁)) = 1)) |
73 | | oveq1 7177 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (𝑚 /L 𝑁) = (𝑀 /L 𝑁)) |
74 | | oveq2 7178 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (𝑁 /L 𝑚) = (𝑁 /L 𝑀)) |
75 | 73, 74 | oveq12d 7188 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = ((𝑀 /L 𝑁) · (𝑁 /L 𝑀))) |
76 | | oveq1 7177 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑀 → (𝑚 − 1) = (𝑀 − 1)) |
77 | 76 | oveq1d 7185 |
. . . . . . . . 9
⊢ (𝑚 = 𝑀 → ((𝑚 − 1) / 2) = ((𝑀 − 1) / 2)) |
78 | 77 | oveq1d 7185 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)) = (((𝑀 − 1) / 2) · ((𝑁 − 1) /
2))) |
79 | 78 | oveq2d 7186 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))) = (-1↑(((𝑀 − 1) / 2) ·
((𝑁 − 1) /
2)))) |
80 | 75, 79 | eqeq12d 2754 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))) ↔ ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) /
2))))) |
81 | 72, 80 | imbi12d 348 |
. . . . 5
⊢ (𝑚 = 𝑀 → (((𝑚 gcd (2 · 𝑁)) = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)))) ↔ ((𝑀 gcd (2 · 𝑁)) = 1 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) /
2)))))) |
82 | 81 | imbi2d 344 |
. . . 4
⊢ (𝑚 = 𝑀 → ((𝜑 → ((𝑚 gcd (2 · 𝑁)) = 1 → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))))) ↔ (𝜑 → ((𝑀 gcd (2 · 𝑁)) = 1 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) /
2))))))) |
83 | | 1t1e1 11878 |
. . . . . . 7
⊢ (1
· 1) = 1 |
84 | | neg1cn 11830 |
. . . . . . . 8
⊢ -1 ∈
ℂ |
85 | | exp0 13525 |
. . . . . . . 8
⊢ (-1
∈ ℂ → (-1↑0) = 1) |
86 | 84, 85 | ax-mp 5 |
. . . . . . 7
⊢
(-1↑0) = 1 |
87 | 83, 86 | eqtr4i 2764 |
. . . . . 6
⊢ (1
· 1) = (-1↑0) |
88 | | sq1 13650 |
. . . . . . . . 9
⊢
(1↑2) = 1 |
89 | 88 | oveq1i 7180 |
. . . . . . . 8
⊢
((1↑2) /L 𝑁) = (1 /L 𝑁) |
90 | | 1z 12093 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
91 | | ax-1ne0 10684 |
. . . . . . . . . 10
⊢ 1 ≠
0 |
92 | 90, 91 | pm3.2i 474 |
. . . . . . . . 9
⊢ (1 ∈
ℤ ∧ 1 ≠ 0) |
93 | 4 | nnzd 12167 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℤ) |
94 | | 1gcd 15977 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → (1 gcd
𝑁) = 1) |
95 | 93, 94 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (1 gcd 𝑁) = 1) |
96 | | lgssq 26073 |
. . . . . . . . 9
⊢ (((1
∈ ℤ ∧ 1 ≠ 0) ∧ 𝑁 ∈ ℤ ∧ (1 gcd 𝑁) = 1) → ((1↑2)
/L 𝑁) =
1) |
97 | 92, 93, 95, 96 | mp3an2i 1467 |
. . . . . . . 8
⊢ (𝜑 → ((1↑2)
/L 𝑁) =
1) |
98 | 89, 97 | eqtr3id 2787 |
. . . . . . 7
⊢ (𝜑 → (1 /L
𝑁) = 1) |
99 | 88 | oveq2i 7181 |
. . . . . . . 8
⊢ (𝑁 /L
(1↑2)) = (𝑁
/L 1) |
100 | | 1nn 11727 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ |
101 | 100 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℕ) |
102 | | gcd1 15971 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → (𝑁 gcd 1) = 1) |
103 | 93, 102 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 gcd 1) = 1) |
104 | | lgssq2 26074 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 1 ∈
ℕ ∧ (𝑁 gcd 1) =
1) → (𝑁
/L (1↑2)) = 1) |
105 | 93, 101, 103, 104 | syl3anc 1372 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 /L (1↑2)) =
1) |
106 | 99, 105 | eqtr3id 2787 |
. . . . . . 7
⊢ (𝜑 → (𝑁 /L 1) =
1) |
107 | 98, 106 | oveq12d 7188 |
. . . . . 6
⊢ (𝜑 → ((1 /L
𝑁) · (𝑁 /L 1)) = (1
· 1)) |
108 | | nnm1nn0 12017 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
109 | 4, 108 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
110 | 109 | nn0cnd 12038 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 − 1) ∈ ℂ) |
111 | 110 | halfcld 11961 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 − 1) / 2) ∈
ℂ) |
112 | 111 | mul02d 10916 |
. . . . . . 7
⊢ (𝜑 → (0 · ((𝑁 − 1) / 2)) =
0) |
113 | 112 | oveq2d 7186 |
. . . . . 6
⊢ (𝜑 → (-1↑(0 ·
((𝑁 − 1) / 2))) =
(-1↑0)) |
114 | 87, 107, 113 | 3eqtr4a 2799 |
. . . . 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 16116 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℙ → 𝑚 ∈
ℤ) |
118 | 117 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → 𝑚 ∈ ℤ) |
119 | 6 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → 2 ∈
ℤ) |
120 | 4 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → 𝑁 ∈ ℕ) |
121 | 120 | nnzd 12167 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → 𝑁 ∈ ℤ) |
122 | | zmulcl 12112 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ) → (2 · 𝑁) ∈ ℤ) |
123 | 6, 121, 122 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → (2 · 𝑁) ∈
ℤ) |
124 | | simprr 773 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → (𝑚 gcd (2 · 𝑁)) = 1) |
125 | | dvdsmul1 15723 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ) → 2 ∥ (2 · 𝑁)) |
126 | 6, 121, 125 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → 2 ∥ (2 · 𝑁)) |
127 | | rpdvds 16101 |
. . . . . . . . . . 11
⊢ (((𝑚 ∈ ℤ ∧ 2 ∈
ℤ ∧ (2 · 𝑁) ∈ ℤ) ∧ ((𝑚 gcd (2 · 𝑁)) = 1 ∧ 2 ∥ (2 · 𝑁))) → (𝑚 gcd 2) = 1) |
128 | 118, 119,
123, 124, 126, 127 | syl32anc 1379 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → (𝑚 gcd 2) = 1) |
129 | | prmrp 16153 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℙ ∧ 2 ∈
ℙ) → ((𝑚 gcd 2)
= 1 ↔ 𝑚 ≠
2)) |
130 | 116, 10, 129 | sylancl 589 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → ((𝑚 gcd 2) = 1 ↔ 𝑚 ≠ 2)) |
131 | 128, 130 | mpbid 235 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → 𝑚 ≠ 2) |
132 | | eldifsn 4675 |
. . . . . . . . 9
⊢ (𝑚 ∈ (ℙ ∖ {2})
↔ (𝑚 ∈ ℙ
∧ 𝑚 ≠
2)) |
133 | 116, 131,
132 | sylanbrc 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → 𝑚 ∈ (ℙ ∖
{2})) |
134 | | prmnn 16115 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℙ → 𝑚 ∈
ℕ) |
135 | 134 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → 𝑚 ∈ ℕ) |
136 | 2 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → 2 ∈
ℕ) |
137 | | rpmulgcd 16002 |
. . . . . . . . . 10
⊢ (((𝑚 ∈ ℕ ∧ 2 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ (𝑚 gcd 2) =
1) → (𝑚 gcd (2
· 𝑁)) = (𝑚 gcd 𝑁)) |
138 | 135, 136,
120, 128, 137 | syl31anc 1374 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → (𝑚 gcd (2 · 𝑁)) = (𝑚 gcd 𝑁)) |
139 | 138, 124 | eqtr3d 2775 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → (𝑚 gcd 𝑁) = 1) |
140 | 133, 139 | jca 515 |
. . . . . . 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 594 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ ℙ ∧ (𝑚 gcd (2 · 𝑁)) = 1)) → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)))) |
143 | 142 | exp32 424 |
. . . . 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 521 |
. . . . 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 12366 |
. . . . . . . . . . . 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 12366 |
. . . . . . . . . . . 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 11769 |
. . . . . . . . . 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 15813 |
. . . . . . . . . . . 12
⊢ ¬ 2
∥ 1 |
154 | 93 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → 𝑁 ∈ ℤ) |
155 | 6, 154, 125 | sylancr 590 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → 2 ∥ (2 · 𝑁)) |
156 | | eluzelz 12334 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈
(ℤ≥‘2) → 𝑥 ∈ ℤ) |
157 | | eluzelz 12334 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈
(ℤ≥‘2) → 𝑦 ∈ ℤ) |
158 | 156, 157 | anim12i 616 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈
(ℤ≥‘2) ∧ 𝑦 ∈ (ℤ≥‘2))
→ (𝑥 ∈ ℤ
∧ 𝑦 ∈
ℤ)) |
159 | 158 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) |
160 | | zmulcl 12112 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 · 𝑦) ∈ ℤ) |
161 | 159, 160 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → (𝑥 · 𝑦) ∈ ℤ) |
162 | 6, 154, 122 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → (2 · 𝑁) ∈ ℤ) |
163 | | dvdsgcd 15988 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℤ ∧ (𝑥
· 𝑦) ∈ ℤ
∧ (2 · 𝑁) ∈
ℤ) → ((2 ∥ (𝑥 · 𝑦) ∧ 2 ∥ (2 · 𝑁)) → 2 ∥ ((𝑥 · 𝑦) gcd (2 · 𝑁)))) |
164 | 6, 161, 162, 163 | mp3an2i 1467 |
. . . . . . . . . . . . . 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 488 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) |
167 | 166 | breq2d 5042 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → (2 ∥ ((𝑥 · 𝑦) gcd (2 · 𝑁)) ↔ 2 ∥ 1)) |
168 | 165, 167 | sylibd 242 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → (2 ∥ (𝑥 · 𝑦) → 2 ∥ 1)) |
169 | 153, 168 | mtoi 202 |
. . . . . . . . . . 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 15724 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ) → 𝑁
∥ (2 · 𝑁)) |
175 | 6, 154, 174 | sylancr 590 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → 𝑁 ∥ (2 · 𝑁)) |
176 | | rpdvds 16101 |
. . . . . . . . . . . 12
⊢ ((((𝑥 · 𝑦) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (2 · 𝑁) ∈ ℤ) ∧ (((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1 ∧ 𝑁 ∥ (2 · 𝑁))) → ((𝑥 · 𝑦) gcd 𝑁) = 1) |
177 | 161, 154,
162, 166, 175, 176 | syl32anc 1379 |
. . . . . . . . . . 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 2739 |
. . . . . . . . . 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 498 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → 𝑥 ∈ ℤ) |
181 | 180, 162 | gcdcomd 15957 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → (𝑥 gcd (2 · 𝑁)) = ((2 · 𝑁) gcd 𝑥)) |
182 | 162, 161 | gcdcomd 15957 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → ((2 · 𝑁) gcd (𝑥 · 𝑦)) = ((𝑥 · 𝑦) gcd (2 · 𝑁))) |
183 | 182, 166 | eqtrd 2773 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → ((2 · 𝑁) gcd (𝑥 · 𝑦)) = 1) |
184 | | dvdsmul1 15723 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑥 ∥ (𝑥 · 𝑦)) |
185 | 159, 184 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → 𝑥 ∥ (𝑥 · 𝑦)) |
186 | | rpdvds 16101 |
. . . . . . . . . . . . . 14
⊢ ((((2
· 𝑁) ∈ ℤ
∧ 𝑥 ∈ ℤ
∧ (𝑥 · 𝑦) ∈ ℤ) ∧ (((2
· 𝑁) gcd (𝑥 · 𝑦)) = 1 ∧ 𝑥 ∥ (𝑥 · 𝑦))) → ((2 · 𝑁) gcd 𝑥) = 1) |
187 | 162, 180,
161, 183, 185, 186 | syl32anc 1379 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → ((2 · 𝑁) gcd 𝑥) = 1) |
188 | 181, 187 | eqtrd 2773 |
. . . . . . . . . . . 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 499 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → 𝑦 ∈ ℤ) |
193 | 192, 162 | gcdcomd 15957 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → (𝑦 gcd (2 · 𝑁)) = ((2 · 𝑁) gcd 𝑦)) |
194 | | dvdsmul2 15724 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑦 ∥ (𝑥 · 𝑦)) |
195 | 159, 194 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → 𝑦 ∥ (𝑥 · 𝑦)) |
196 | | rpdvds 16101 |
. . . . . . . . . . . . . 14
⊢ ((((2
· 𝑁) ∈ ℤ
∧ 𝑦 ∈ ℤ
∧ (𝑥 · 𝑦) ∈ ℤ) ∧ (((2
· 𝑁) gcd (𝑥 · 𝑦)) = 1 ∧ 𝑦 ∥ (𝑥 · 𝑦))) → ((2 · 𝑁) gcd 𝑦) = 1) |
197 | 162, 192,
161, 183, 195, 196 | syl32anc 1379 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘2)
∧ 𝑦 ∈
(ℤ≥‘2))) ∧ ((𝑥 · 𝑦) gcd (2 · 𝑁)) = 1) → ((2 · 𝑁) gcd 𝑦) = 1) |
198 | 193, 197 | eqtrd 2773 |
. . . . . . . . . . . 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 26120 |
. . . . . . . . 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 424 |
. . . . . . . 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 417 |
. . . . . 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 | syl5bir 246 |
. . . 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 16127 |
. . 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)))) |