Proof of Theorem lgsquad3
Step | Hyp | Ref
| Expression |
1 | | simplrl 797 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → 𝑁 ∈ ℕ) |
2 | | nnz 11728 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
3 | 1, 2 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → 𝑁 ∈ ℤ) |
4 | | nnz 11728 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
5 | 4 | ad3antrrr 723 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → 𝑀 ∈ ℤ) |
6 | | lgscl 25450 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 /L 𝑀) ∈
ℤ) |
7 | 3, 5, 6 | syl2anc 581 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑁 /L 𝑀) ∈ ℤ) |
8 | 7 | zred 11811 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑁 /L 𝑀) ∈ ℝ) |
9 | | absresq 14420 |
. . . . . . 7
⊢ ((𝑁 /L 𝑀) ∈ ℝ →
((abs‘(𝑁
/L 𝑀))↑2) = ((𝑁 /L 𝑀)↑2)) |
10 | 8, 9 | syl 17 |
. . . . . 6
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((abs‘(𝑁 /L 𝑀))↑2) = ((𝑁 /L 𝑀)↑2)) |
11 | | gcdcom 15609 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁)) |
12 | 3, 5, 11 | syl2anc 581 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁)) |
13 | | simpr 479 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑀 gcd 𝑁) = 1) |
14 | 12, 13 | eqtrd 2862 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑁 gcd 𝑀) = 1) |
15 | | lgsabs1 25475 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) →
((abs‘(𝑁
/L 𝑀)) =
1 ↔ (𝑁 gcd 𝑀) = 1)) |
16 | 3, 5, 15 | syl2anc 581 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((abs‘(𝑁 /L 𝑀)) = 1 ↔ (𝑁 gcd 𝑀) = 1)) |
17 | 14, 16 | mpbird 249 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (abs‘(𝑁 /L 𝑀)) = 1) |
18 | 17 | oveq1d 6921 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((abs‘(𝑁 /L 𝑀))↑2) = (1↑2)) |
19 | | sq1 13253 |
. . . . . . 7
⊢
(1↑2) = 1 |
20 | 18, 19 | syl6eq 2878 |
. . . . . 6
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((abs‘(𝑁 /L 𝑀))↑2) = 1) |
21 | 7 | zcnd 11812 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑁 /L 𝑀) ∈ ℂ) |
22 | 21 | sqvald 13300 |
. . . . . 6
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((𝑁 /L 𝑀)↑2) = ((𝑁 /L 𝑀) · (𝑁 /L 𝑀))) |
23 | 10, 20, 22 | 3eqtr3d 2870 |
. . . . 5
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → 1 = ((𝑁 /L 𝑀) · (𝑁 /L 𝑀))) |
24 | 23 | oveq2d 6922 |
. . . 4
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((𝑀 /L 𝑁) · 1) = ((𝑀 /L 𝑁) · ((𝑁 /L 𝑀) · (𝑁 /L 𝑀)))) |
25 | | lgscl 25450 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 /L 𝑁) ∈
ℤ) |
26 | 5, 3, 25 | syl2anc 581 |
. . . . . 6
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑀 /L 𝑁) ∈ ℤ) |
27 | 26 | zcnd 11812 |
. . . . 5
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑀 /L 𝑁) ∈ ℂ) |
28 | 27, 21, 21 | mulassd 10381 |
. . . 4
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) · (𝑁 /L 𝑀)) = ((𝑀 /L 𝑁) · ((𝑁 /L 𝑀) · (𝑁 /L 𝑀)))) |
29 | 24, 28 | eqtr4d 2865 |
. . 3
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((𝑀 /L 𝑁) · 1) = (((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) · (𝑁 /L 𝑀))) |
30 | 27 | mulid1d 10375 |
. . 3
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((𝑀 /L 𝑁) · 1) = (𝑀 /L 𝑁)) |
31 | | simplll 793 |
. . . . 5
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → 𝑀 ∈ ℕ) |
32 | | simpllr 795 |
. . . . 5
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ¬ 2 ∥ 𝑀) |
33 | | simplrr 798 |
. . . . 5
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ¬ 2 ∥ 𝑁) |
34 | 31, 32, 1, 33, 13 | lgsquad2 25525 |
. . . 4
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) /
2)))) |
35 | 34 | oveq1d 6921 |
. . 3
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) · (𝑁 /L 𝑀)) = ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) ·
(𝑁 /L
𝑀))) |
36 | 29, 30, 35 | 3eqtr3d 2870 |
. 2
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑀 /L 𝑁) = ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) ·
(𝑁 /L
𝑀))) |
37 | | neg1cn 11473 |
. . . . . 6
⊢ -1 ∈
ℂ |
38 | 37 | a1i 11 |
. . . . 5
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → -1 ∈
ℂ) |
39 | | neg1ne0 11475 |
. . . . . 6
⊢ -1 ≠
0 |
40 | 39 | a1i 11 |
. . . . 5
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → -1 ≠ 0) |
41 | 4 | ad3antrrr 723 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → 𝑀 ∈ ℤ) |
42 | | simpllr 795 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → ¬ 2 ∥ 𝑀) |
43 | | 1zzd 11737 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → 1 ∈
ℤ) |
44 | | 2prm 15778 |
. . . . . . . . 9
⊢ 2 ∈
ℙ |
45 | | nprmdvds1 15790 |
. . . . . . . . 9
⊢ (2 ∈
ℙ → ¬ 2 ∥ 1) |
46 | 44, 45 | mp1i 13 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → ¬ 2 ∥
1) |
47 | | omoe 15463 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ ¬ 2
∥ 𝑀) ∧ (1 ∈
ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝑀 − 1)) |
48 | 41, 42, 43, 46, 47 | syl22anc 874 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → 2 ∥ (𝑀 − 1)) |
49 | | 2z 11738 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
50 | 49 | a1i 11 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → 2 ∈
ℤ) |
51 | | 2ne0 11463 |
. . . . . . . . 9
⊢ 2 ≠
0 |
52 | 51 | a1i 11 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → 2 ≠ 0) |
53 | | peano2zm 11749 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) |
54 | 41, 53 | syl 17 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → (𝑀 − 1) ∈ ℤ) |
55 | | dvdsval2 15361 |
. . . . . . . 8
⊢ ((2
∈ ℤ ∧ 2 ≠ 0 ∧ (𝑀 − 1) ∈ ℤ) → (2
∥ (𝑀 − 1)
↔ ((𝑀 − 1) / 2)
∈ ℤ)) |
56 | 50, 52, 54, 55 | syl3anc 1496 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → (2 ∥ (𝑀 − 1) ↔ ((𝑀 − 1) / 2) ∈
ℤ)) |
57 | 48, 56 | mpbid 224 |
. . . . . 6
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → ((𝑀 − 1) / 2) ∈
ℤ) |
58 | 2 | adantr 474 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → 𝑁 ∈
ℤ) |
59 | 58 | ad2antlr 720 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → 𝑁 ∈ ℤ) |
60 | | simplrr 798 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → ¬ 2 ∥ 𝑁) |
61 | | omoe 15463 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁) ∧ (1 ∈
ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝑁 − 1)) |
62 | 59, 60, 43, 46, 61 | syl22anc 874 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → 2 ∥ (𝑁 − 1)) |
63 | | peano2zm 11749 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
64 | 59, 63 | syl 17 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → (𝑁 − 1) ∈ ℤ) |
65 | | dvdsval2 15361 |
. . . . . . . 8
⊢ ((2
∈ ℤ ∧ 2 ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → (2
∥ (𝑁 − 1)
↔ ((𝑁 − 1) / 2)
∈ ℤ)) |
66 | 50, 52, 64, 65 | syl3anc 1496 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → (2 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 2) ∈
ℤ)) |
67 | 62, 66 | mpbid 224 |
. . . . . 6
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → ((𝑁 − 1) / 2) ∈
ℤ) |
68 | 57, 67 | zmulcld 11817 |
. . . . 5
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → (((𝑀 − 1) / 2) · ((𝑁 − 1) / 2)) ∈
ℤ) |
69 | 38, 40, 68 | expclzd 13308 |
. . . 4
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) ∈
ℂ) |
70 | 69 | mul01d 10555 |
. . 3
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) · 0) =
0) |
71 | | lgsne0 25474 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑁 /L 𝑀) ≠ 0 ↔ (𝑁 gcd 𝑀) = 1)) |
72 | 11 | eqeq1d 2828 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑁 gcd 𝑀) = 1 ↔ (𝑀 gcd 𝑁) = 1)) |
73 | 71, 72 | bitrd 271 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑁 /L 𝑀) ≠ 0 ↔ (𝑀 gcd 𝑁) = 1)) |
74 | 2, 4, 73 | syl2anr 592 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 /L 𝑀) ≠ 0 ↔ (𝑀 gcd 𝑁) = 1)) |
75 | 74 | necon1bbid 3039 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (¬
(𝑀 gcd 𝑁) = 1 ↔ (𝑁 /L 𝑀) = 0)) |
76 | 75 | ad2ant2r 755 |
. . . . 5
⊢ (((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) → (¬
(𝑀 gcd 𝑁) = 1 ↔ (𝑁 /L 𝑀) = 0)) |
77 | 76 | biimpa 470 |
. . . 4
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → (𝑁 /L 𝑀) = 0) |
78 | 77 | oveq2d 6922 |
. . 3
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) ·
(𝑁 /L
𝑀)) = ((-1↑(((𝑀 − 1) / 2) ·
((𝑁 − 1) / 2)))
· 0)) |
79 | | lgsne0 25474 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 /L 𝑁) ≠ 0 ↔ (𝑀 gcd 𝑁) = 1)) |
80 | 79 | necon1bbid 3039 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬
(𝑀 gcd 𝑁) = 1 ↔ (𝑀 /L 𝑁) = 0)) |
81 | 4, 2, 80 | syl2an 591 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (¬
(𝑀 gcd 𝑁) = 1 ↔ (𝑀 /L 𝑁) = 0)) |
82 | 81 | ad2ant2r 755 |
. . . 4
⊢ (((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) → (¬
(𝑀 gcd 𝑁) = 1 ↔ (𝑀 /L 𝑁) = 0)) |
83 | 82 | biimpa 470 |
. . 3
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → (𝑀 /L 𝑁) = 0) |
84 | 70, 78, 83 | 3eqtr4rd 2873 |
. 2
⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) ∧ ¬
(𝑀 gcd 𝑁) = 1) → (𝑀 /L 𝑁) = ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) ·
(𝑁 /L
𝑀))) |
85 | 36, 84 | pm2.61dan 849 |
1
⊢ (((𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁)) → (𝑀 /L 𝑁) = ((-1↑(((𝑀 − 1) / 2) ·
((𝑁 − 1) / 2)))
· (𝑁
/L 𝑀))) |