Proof of Theorem lgsquad3
Step | Hyp | Ref
| Expression |
1 | | simplrl 775 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → 𝑁 ∈ ℕ) |
2 | | nnz 11998 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
3 | 1, 2 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → 𝑁 ∈ ℤ) |
4 | | nnz 11998 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
5 | 4 | ad3antrrr 728 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → 𝑀 ∈ ℤ) |
6 | | lgscl 25881 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 /L 𝑀) ∈
ℤ) |
7 | 3, 5, 6 | syl2anc 586 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑁 /L 𝑀) ∈ ℤ) |
8 | 7 | zred 12081 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑁 /L 𝑀) ∈ ℝ) |
9 | | absresq 14656 |
. . . . . . 7
⊢ ((𝑁 /L 𝑀) ∈ ℝ →
((abs‘(𝑁
/L 𝑀))↑2) = ((𝑁 /L 𝑀)↑2)) |
10 | 8, 9 | syl 17 |
. . . . . 6
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((abs‘(𝑁 /L 𝑀))↑2) = ((𝑁 /L 𝑀)↑2)) |
11 | | gcdcom 15856 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁)) |
12 | 3, 5, 11 | syl2anc 586 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁)) |
13 | | simpr 487 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑀 gcd 𝑁) = 1) |
14 | 12, 13 | eqtrd 2856 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑁 gcd 𝑀) = 1) |
15 | | lgsabs1 25906 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) →
((abs‘(𝑁
/L 𝑀)) =
1 ↔ (𝑁 gcd 𝑀) = 1)) |
16 | 3, 5, 15 | syl2anc 586 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((abs‘(𝑁 /L 𝑀)) = 1 ↔ (𝑁 gcd 𝑀) = 1)) |
17 | 14, 16 | mpbird 259 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (abs‘(𝑁 /L 𝑀)) = 1) |
18 | 17 | oveq1d 7165 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((abs‘(𝑁 /L 𝑀))↑2) = (1↑2)) |
19 | | sq1 13552 |
. . . . . . 7
⊢
(1↑2) = 1 |
20 | 18, 19 | syl6eq 2872 |
. . . . . 6
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((abs‘(𝑁 /L 𝑀))↑2) = 1) |
21 | 7 | zcnd 12082 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑁 /L 𝑀) ∈ ℂ) |
22 | 21 | sqvald 13501 |
. . . . . 6
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((𝑁 /L 𝑀)↑2) = ((𝑁 /L 𝑀) · (𝑁 /L 𝑀))) |
23 | 10, 20, 22 | 3eqtr3d 2864 |
. . . . 5
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → 1 = ((𝑁 /L 𝑀) · (𝑁 /L 𝑀))) |
24 | 23 | oveq2d 7166 |
. . . 4
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((𝑀 /L 𝑁) · 1) = ((𝑀 /L 𝑁) · ((𝑁 /L 𝑀) · (𝑁 /L 𝑀)))) |
25 | | lgscl 25881 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 /L 𝑁) ∈
ℤ) |
26 | 5, 3, 25 | syl2anc 586 |
. . . . . 6
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑀 /L 𝑁) ∈ ℤ) |
27 | 26 | zcnd 12082 |
. . . . 5
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑀 /L 𝑁) ∈ ℂ) |
28 | 27, 21, 21 | mulassd 10658 |
. . . 4
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) · (𝑁 /L 𝑀)) = ((𝑀 /L 𝑁) · ((𝑁 /L 𝑀) · (𝑁 /L 𝑀)))) |
29 | 24, 28 | eqtr4d 2859 |
. . 3
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((𝑀 /L 𝑁) · 1) = (((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) · (𝑁 /L 𝑀))) |
30 | 27 | mulid1d 10652 |
. . 3
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((𝑀 /L 𝑁) · 1) = (𝑀 /L 𝑁)) |
31 | | simplll 773 |
. . . . 5
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → 𝑀 ∈ ℕ) |
32 | | simpllr 774 |
. . . . 5
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ¬ 2 ∥ 𝑀) |
33 | | simplrr 776 |
. . . . 5
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ¬ 2 ∥ 𝑁) |
34 | 31, 32, 1, 33, 13 | lgsquad2 25956 |
. . . 4
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) /
2)))) |
35 | 34 | oveq1d 7165 |
. . 3
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) · (𝑁 /L 𝑀)) = ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) ·
(𝑁 /L
𝑀))) |
36 | 29, 30, 35 | 3eqtr3d 2864 |
. 2
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑀 /L 𝑁) = ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) ·
(𝑁 /L
𝑀))) |
37 | | neg1cn 11745 |
. . . . . 6
⊢ -1 ∈
ℂ |
38 | 37 | a1i 11 |
. . . . 5
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → -1 ∈
ℂ) |
39 | | neg1ne0 11747 |
. . . . . 6
⊢ -1 ≠
0 |
40 | 39 | a1i 11 |
. . . . 5
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → -1 ≠ 0) |
41 | 4 | ad3antrrr 728 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → 𝑀 ∈ ℤ) |
42 | | simpllr 774 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → ¬ 2 ∥ 𝑀) |
43 | | 1zzd 12007 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → 1 ∈
ℤ) |
44 | | 2prm 16030 |
. . . . . . . . 9
⊢ 2 ∈
ℙ |
45 | | nprmdvds1 16044 |
. . . . . . . . 9
⊢ (2 ∈
ℙ → ¬ 2 ∥ 1) |
46 | 44, 45 | mp1i 13 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → ¬ 2 ∥
1) |
47 | | omoe 15707 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ ¬ 2
∥ 𝑀) ∧ (1 ∈
ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝑀 − 1)) |
48 | 41, 42, 43, 46, 47 | syl22anc 836 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → 2 ∥ (𝑀 − 1)) |
49 | | 2z 12008 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
50 | | 2ne0 11735 |
. . . . . . . 8
⊢ 2 ≠
0 |
51 | | peano2zm 12019 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) |
52 | 41, 51 | syl 17 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → (𝑀 − 1) ∈ ℤ) |
53 | | dvdsval2 15604 |
. . . . . . . 8
⊢ ((2
∈ ℤ ∧ 2 ≠ 0 ∧ (𝑀 − 1) ∈ ℤ) → (2
∥ (𝑀 − 1)
↔ ((𝑀 − 1) / 2)
∈ ℤ)) |
54 | 49, 50, 52, 53 | mp3an12i 1461 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → (2 ∥ (𝑀 − 1) ↔ ((𝑀 − 1) / 2) ∈
ℤ)) |
55 | 48, 54 | mpbid 234 |
. . . . . 6
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → ((𝑀 − 1) / 2) ∈
ℤ) |
56 | 2 | adantr 483 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → 𝑁 ∈
ℤ) |
57 | 56 | ad2antlr 725 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → 𝑁 ∈ ℤ) |
58 | | simplrr 776 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → ¬ 2 ∥ 𝑁) |
59 | | omoe 15707 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁) ∧ (1 ∈
ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝑁 − 1)) |
60 | 57, 58, 43, 46, 59 | syl22anc 836 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → 2 ∥ (𝑁 − 1)) |
61 | | peano2zm 12019 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
62 | 57, 61 | syl 17 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → (𝑁 − 1) ∈ ℤ) |
63 | | dvdsval2 15604 |
. . . . . . . 8
⊢ ((2
∈ ℤ ∧ 2 ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → (2
∥ (𝑁 − 1)
↔ ((𝑁 − 1) / 2)
∈ ℤ)) |
64 | 49, 50, 62, 63 | mp3an12i 1461 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → (2 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 2) ∈
ℤ)) |
65 | 60, 64 | mpbid 234 |
. . . . . 6
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → ((𝑁 − 1) / 2) ∈
ℤ) |
66 | 55, 65 | zmulcld 12087 |
. . . . 5
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → (((𝑀 − 1) / 2) · ((𝑁 − 1) / 2)) ∈
ℤ) |
67 | 38, 40, 66 | expclzd 13509 |
. . . 4
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) ∈
ℂ) |
68 | 67 | mul01d 10833 |
. . 3
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) · 0) =
0) |
69 | | lgsne0 25905 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑁 /L 𝑀) ≠ 0 ↔ (𝑁 gcd 𝑀) = 1)) |
70 | 11 | eqeq1d 2823 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑁 gcd 𝑀) = 1 ↔ (𝑀 gcd 𝑁) = 1)) |
71 | 69, 70 | bitrd 281 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑁 /L 𝑀) ≠ 0 ↔ (𝑀 gcd 𝑁) = 1)) |
72 | 2, 4, 71 | syl2anr 598 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 /L 𝑀) ≠ 0 ↔ (𝑀 gcd 𝑁) = 1)) |
73 | 72 | necon1bbid 3055 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (¬
(𝑀 gcd 𝑁) = 1 ↔ (𝑁 /L 𝑀) = 0)) |
74 | 73 | ad2ant2r 745 |
. . . . 5
⊢ (((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) → (¬
(𝑀 gcd 𝑁) = 1 ↔ (𝑁 /L 𝑀) = 0)) |
75 | 74 | biimpa 479 |
. . . 4
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → (𝑁 /L 𝑀) = 0) |
76 | 75 | oveq2d 7166 |
. . 3
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) ·
(𝑁 /L
𝑀)) = ((-1↑(((𝑀 − 1) / 2) ·
((𝑁 − 1) / 2)))
· 0)) |
77 | | lgsne0 25905 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 /L 𝑁) ≠ 0 ↔ (𝑀 gcd 𝑁) = 1)) |
78 | 77 | necon1bbid 3055 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬
(𝑀 gcd 𝑁) = 1 ↔ (𝑀 /L 𝑁) = 0)) |
79 | 4, 2, 78 | syl2an 597 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (¬
(𝑀 gcd 𝑁) = 1 ↔ (𝑀 /L 𝑁) = 0)) |
80 | 79 | ad2ant2r 745 |
. . . 4
⊢ (((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) → (¬
(𝑀 gcd 𝑁) = 1 ↔ (𝑀 /L 𝑁) = 0)) |
81 | 80 | biimpa 479 |
. . 3
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → (𝑀 /L 𝑁) = 0) |
82 | 68, 76, 81 | 3eqtr4rd 2867 |
. 2
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → (𝑀 /L 𝑁) = ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) ·
(𝑁 /L
𝑀))) |
83 | 36, 82 | pm2.61dan 811 |
1
⊢ (((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) → (𝑀 /L 𝑁) = ((-1↑(((𝑀 − 1) / 2) ·
((𝑁 − 1) / 2)))
· (𝑁
/L 𝑀))) |