Proof of Theorem sqgcd
Step | Hyp | Ref
| Expression |
1 | | gcdnncl 11922 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℕ) |
2 | 1 | nnsqcld 10630 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁)↑2) ∈ ℕ) |
3 | 2 | nncnd 8892 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁)↑2) ∈ ℂ) |
4 | 3 | mulid1d 7937 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 gcd 𝑁)↑2) · 1) = ((𝑀 gcd 𝑁)↑2)) |
5 | | nnsqcl 10545 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (𝑀↑2) ∈
ℕ) |
6 | 5 | nnzd 9333 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (𝑀↑2) ∈
ℤ) |
7 | 6 | adantr 274 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀↑2) ∈
ℤ) |
8 | | nnsqcl 10545 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁↑2) ∈
ℕ) |
9 | 8 | nnzd 9333 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑁↑2) ∈
ℤ) |
10 | 9 | adantl 275 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁↑2) ∈
ℤ) |
11 | | nnz 9231 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
12 | | nnz 9231 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
13 | | gcddvds 11918 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) |
14 | 11, 12, 13 | syl2an 287 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) |
15 | 14 | simpld 111 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∥ 𝑀) |
16 | 1 | nnzd 9333 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℤ) |
17 | 11 | adantr 274 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℤ) |
18 | | dvdssqim 11979 |
. . . . . . 7
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 → ((𝑀 gcd 𝑁)↑2) ∥ (𝑀↑2))) |
19 | 16, 17, 18 | syl2anc 409 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑀 → ((𝑀 gcd 𝑁)↑2) ∥ (𝑀↑2))) |
20 | 15, 19 | mpd 13 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁)↑2) ∥ (𝑀↑2)) |
21 | 14 | simprd 113 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∥ 𝑁) |
22 | 12 | adantl 275 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℤ) |
23 | | dvdssqim 11979 |
. . . . . . 7
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑁 → ((𝑀 gcd 𝑁)↑2) ∥ (𝑁↑2))) |
24 | 16, 22, 23 | syl2anc 409 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑁 → ((𝑀 gcd 𝑁)↑2) ∥ (𝑁↑2))) |
25 | 21, 24 | mpd 13 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁)↑2) ∥ (𝑁↑2)) |
26 | | gcddiv 11974 |
. . . . 5
⊢ ((((𝑀↑2) ∈ ℤ ∧
(𝑁↑2) ∈ ℤ
∧ ((𝑀 gcd 𝑁)↑2) ∈ ℕ) ∧
(((𝑀 gcd 𝑁)↑2) ∥ (𝑀↑2) ∧ ((𝑀 gcd 𝑁)↑2) ∥ (𝑁↑2))) → (((𝑀↑2) gcd (𝑁↑2)) / ((𝑀 gcd 𝑁)↑2)) = (((𝑀↑2) / ((𝑀 gcd 𝑁)↑2)) gcd ((𝑁↑2) / ((𝑀 gcd 𝑁)↑2)))) |
27 | 7, 10, 2, 20, 25, 26 | syl32anc 1241 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀↑2) gcd (𝑁↑2)) / ((𝑀 gcd 𝑁)↑2)) = (((𝑀↑2) / ((𝑀 gcd 𝑁)↑2)) gcd ((𝑁↑2) / ((𝑀 gcd 𝑁)↑2)))) |
28 | | nncn 8886 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
29 | 28 | adantr 274 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℂ) |
30 | 1 | nncnd 8892 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℂ) |
31 | 1 | nnap0d 8924 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) # 0) |
32 | 29, 30, 31 | sqdivapd 10622 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 / (𝑀 gcd 𝑁))↑2) = ((𝑀↑2) / ((𝑀 gcd 𝑁)↑2))) |
33 | | nncn 8886 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
34 | 33 | adantl 275 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℂ) |
35 | 34, 30, 31 | sqdivapd 10622 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 / (𝑀 gcd 𝑁))↑2) = ((𝑁↑2) / ((𝑀 gcd 𝑁)↑2))) |
36 | 32, 35 | oveq12d 5871 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 / (𝑀 gcd 𝑁))↑2) gcd ((𝑁 / (𝑀 gcd 𝑁))↑2)) = (((𝑀↑2) / ((𝑀 gcd 𝑁)↑2)) gcd ((𝑁↑2) / ((𝑀 gcd 𝑁)↑2)))) |
37 | | gcddiv 11974 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 gcd 𝑁) ∈ ℕ) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) → ((𝑀 gcd 𝑁) / (𝑀 gcd 𝑁)) = ((𝑀 / (𝑀 gcd 𝑁)) gcd (𝑁 / (𝑀 gcd 𝑁)))) |
38 | 17, 22, 1, 14, 37 | syl31anc 1236 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) / (𝑀 gcd 𝑁)) = ((𝑀 / (𝑀 gcd 𝑁)) gcd (𝑁 / (𝑀 gcd 𝑁)))) |
39 | 30, 31 | dividapd 8703 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) / (𝑀 gcd 𝑁)) = 1) |
40 | 38, 39 | eqtr3d 2205 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 / (𝑀 gcd 𝑁)) gcd (𝑁 / (𝑀 gcd 𝑁))) = 1) |
41 | 1 | nnne0d 8923 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ≠ 0) |
42 | | dvdsval2 11752 |
. . . . . . . . 9
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ (𝑀 gcd 𝑁) ≠ 0 ∧ 𝑀 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ↔ (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ)) |
43 | 16, 41, 17, 42 | syl3anc 1233 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ↔ (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ)) |
44 | 15, 43 | mpbid 146 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ) |
45 | | nnre 8885 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
46 | 45 | adantr 274 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℝ) |
47 | 1 | nnred 8891 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℝ) |
48 | | nngt0 8903 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → 0 <
𝑀) |
49 | 48 | adantr 274 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 <
𝑀) |
50 | 1 | nngt0d 8922 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 <
(𝑀 gcd 𝑁)) |
51 | 46, 47, 49, 50 | divgt0d 8851 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 <
(𝑀 / (𝑀 gcd 𝑁))) |
52 | | elnnz 9222 |
. . . . . . 7
⊢ ((𝑀 / (𝑀 gcd 𝑁)) ∈ ℕ ↔ ((𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ ∧ 0 < (𝑀 / (𝑀 gcd 𝑁)))) |
53 | 44, 51, 52 | sylanbrc 415 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 / (𝑀 gcd 𝑁)) ∈ ℕ) |
54 | | dvdsval2 11752 |
. . . . . . . . 9
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ (𝑀 gcd 𝑁) ≠ 0 ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑁 ↔ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ)) |
55 | 16, 41, 22, 54 | syl3anc 1233 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑁 ↔ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ)) |
56 | 21, 55 | mpbid 146 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ) |
57 | | nnre 8885 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
58 | 57 | adantl 275 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ) |
59 | | nngt0 8903 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
60 | 59 | adantl 275 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 <
𝑁) |
61 | 58, 47, 60, 50 | divgt0d 8851 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 <
(𝑁 / (𝑀 gcd 𝑁))) |
62 | | elnnz 9222 |
. . . . . . 7
⊢ ((𝑁 / (𝑀 gcd 𝑁)) ∈ ℕ ↔ ((𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ ∧ 0 < (𝑁 / (𝑀 gcd 𝑁)))) |
63 | 56, 61, 62 | sylanbrc 415 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 / (𝑀 gcd 𝑁)) ∈ ℕ) |
64 | | 2nn 9039 |
. . . . . . 7
⊢ 2 ∈
ℕ |
65 | | rppwr 11983 |
. . . . . . 7
⊢ (((𝑀 / (𝑀 gcd 𝑁)) ∈ ℕ ∧ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℕ ∧ 2 ∈ ℕ)
→ (((𝑀 / (𝑀 gcd 𝑁)) gcd (𝑁 / (𝑀 gcd 𝑁))) = 1 → (((𝑀 / (𝑀 gcd 𝑁))↑2) gcd ((𝑁 / (𝑀 gcd 𝑁))↑2)) = 1)) |
66 | 64, 65 | mp3an3 1321 |
. . . . . 6
⊢ (((𝑀 / (𝑀 gcd 𝑁)) ∈ ℕ ∧ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℕ) → (((𝑀 / (𝑀 gcd 𝑁)) gcd (𝑁 / (𝑀 gcd 𝑁))) = 1 → (((𝑀 / (𝑀 gcd 𝑁))↑2) gcd ((𝑁 / (𝑀 gcd 𝑁))↑2)) = 1)) |
67 | 53, 63, 66 | syl2anc 409 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 / (𝑀 gcd 𝑁)) gcd (𝑁 / (𝑀 gcd 𝑁))) = 1 → (((𝑀 / (𝑀 gcd 𝑁))↑2) gcd ((𝑁 / (𝑀 gcd 𝑁))↑2)) = 1)) |
68 | 40, 67 | mpd 13 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 / (𝑀 gcd 𝑁))↑2) gcd ((𝑁 / (𝑀 gcd 𝑁))↑2)) = 1) |
69 | 27, 36, 68 | 3eqtr2d 2209 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀↑2) gcd (𝑁↑2)) / ((𝑀 gcd 𝑁)↑2)) = 1) |
70 | 6, 9 | anim12i 336 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀↑2) ∈ ℤ ∧
(𝑁↑2) ∈
ℤ)) |
71 | 5 | nnne0d 8923 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑀↑2) ≠
0) |
72 | 71 | neneqd 2361 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ¬
(𝑀↑2) =
0) |
73 | 72 | intnanrd 927 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ¬
((𝑀↑2) = 0 ∧
(𝑁↑2) =
0)) |
74 | 73 | adantr 274 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ¬
((𝑀↑2) = 0 ∧
(𝑁↑2) =
0)) |
75 | | gcdn0cl 11917 |
. . . . . 6
⊢ ((((𝑀↑2) ∈ ℤ ∧
(𝑁↑2) ∈ ℤ)
∧ ¬ ((𝑀↑2) = 0
∧ (𝑁↑2) = 0))
→ ((𝑀↑2) gcd
(𝑁↑2)) ∈
ℕ) |
76 | 70, 74, 75 | syl2anc 409 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀↑2) gcd (𝑁↑2)) ∈ ℕ) |
77 | 76 | nncnd 8892 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀↑2) gcd (𝑁↑2)) ∈ ℂ) |
78 | 2 | nnap0d 8924 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁)↑2) # 0) |
79 | | ax-1cn 7867 |
. . . . 5
⊢ 1 ∈
ℂ |
80 | | divmulap 8592 |
. . . . 5
⊢ ((((𝑀↑2) gcd (𝑁↑2)) ∈ ℂ ∧ 1 ∈
ℂ ∧ (((𝑀 gcd
𝑁)↑2) ∈ ℂ
∧ ((𝑀 gcd 𝑁)↑2) # 0)) → ((((𝑀↑2) gcd (𝑁↑2)) / ((𝑀 gcd 𝑁)↑2)) = 1 ↔ (((𝑀 gcd 𝑁)↑2) · 1) = ((𝑀↑2) gcd (𝑁↑2)))) |
81 | 79, 80 | mp3an2 1320 |
. . . 4
⊢ ((((𝑀↑2) gcd (𝑁↑2)) ∈ ℂ ∧ (((𝑀 gcd 𝑁)↑2) ∈ ℂ ∧ ((𝑀 gcd 𝑁)↑2) # 0)) → ((((𝑀↑2) gcd (𝑁↑2)) / ((𝑀 gcd 𝑁)↑2)) = 1 ↔ (((𝑀 gcd 𝑁)↑2) · 1) = ((𝑀↑2) gcd (𝑁↑2)))) |
82 | 77, 3, 78, 81 | syl12anc 1231 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
((((𝑀↑2) gcd (𝑁↑2)) / ((𝑀 gcd 𝑁)↑2)) = 1 ↔ (((𝑀 gcd 𝑁)↑2) · 1) = ((𝑀↑2) gcd (𝑁↑2)))) |
83 | 69, 82 | mpbid 146 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 gcd 𝑁)↑2) · 1) = ((𝑀↑2) gcd (𝑁↑2))) |
84 | 4, 83 | eqtr3d 2205 |
1
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁)↑2) = ((𝑀↑2) gcd (𝑁↑2))) |