Proof of Theorem sqgcd
Step | Hyp | Ref
| Expression |
1 | | nnz 11276 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
2 | | nnz 11276 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
3 | 1, 2 | anim12i 588 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ∈ ℤ ∧ 𝑁 ∈
ℤ)) |
4 | | nnne0 10930 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → 𝑀 ≠ 0) |
5 | 4 | neneqd 2787 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ¬
𝑀 = 0) |
6 | 5 | intnanrd 954 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ¬
(𝑀 = 0 ∧ 𝑁 = 0)) |
7 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ¬
(𝑀 = 0 ∧ 𝑁 = 0)) |
8 | | gcdn0cl 15062 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) ∈ ℕ) |
9 | 3, 7, 8 | syl2anc 691 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℕ) |
10 | 9 | nnsqcld 12891 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁)↑2) ∈ ℕ) |
11 | 10 | nncnd 10913 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁)↑2) ∈ ℂ) |
12 | 11 | mulid1d 9936 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 gcd 𝑁)↑2) · 1) = ((𝑀 gcd 𝑁)↑2)) |
13 | | nnsqcl 12795 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (𝑀↑2) ∈
ℕ) |
14 | 13 | nnzd 11357 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (𝑀↑2) ∈
ℤ) |
15 | 14 | adantr 480 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀↑2) ∈
ℤ) |
16 | | nnsqcl 12795 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁↑2) ∈
ℕ) |
17 | 16 | nnzd 11357 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑁↑2) ∈
ℤ) |
18 | 17 | adantl 481 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁↑2) ∈
ℤ) |
19 | | gcddvds 15063 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) |
20 | 1, 2, 19 | syl2an 493 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) |
21 | 20 | simpld 474 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∥ 𝑀) |
22 | 9 | nnzd 11357 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℤ) |
23 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℤ) |
24 | | dvdssqim 15111 |
. . . . . . 7
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 → ((𝑀 gcd 𝑁)↑2) ∥ (𝑀↑2))) |
25 | 22, 23, 24 | syl2anc 691 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑀 → ((𝑀 gcd 𝑁)↑2) ∥ (𝑀↑2))) |
26 | 21, 25 | mpd 15 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁)↑2) ∥ (𝑀↑2)) |
27 | 20 | simprd 478 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∥ 𝑁) |
28 | 2 | adantl 481 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℤ) |
29 | | dvdssqim 15111 |
. . . . . . 7
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑁 → ((𝑀 gcd 𝑁)↑2) ∥ (𝑁↑2))) |
30 | 22, 28, 29 | syl2anc 691 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑁 → ((𝑀 gcd 𝑁)↑2) ∥ (𝑁↑2))) |
31 | 27, 30 | mpd 15 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁)↑2) ∥ (𝑁↑2)) |
32 | | gcddiv 15106 |
. . . . 5
⊢ ((((𝑀↑2) ∈ ℤ ∧
(𝑁↑2) ∈ ℤ
∧ ((𝑀 gcd 𝑁)↑2) ∈ ℕ) ∧
(((𝑀 gcd 𝑁)↑2) ∥ (𝑀↑2) ∧ ((𝑀 gcd 𝑁)↑2) ∥ (𝑁↑2))) → (((𝑀↑2) gcd (𝑁↑2)) / ((𝑀 gcd 𝑁)↑2)) = (((𝑀↑2) / ((𝑀 gcd 𝑁)↑2)) gcd ((𝑁↑2) / ((𝑀 gcd 𝑁)↑2)))) |
33 | 15, 18, 10, 26, 31, 32 | syl32anc 1326 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀↑2) gcd (𝑁↑2)) / ((𝑀 gcd 𝑁)↑2)) = (((𝑀↑2) / ((𝑀 gcd 𝑁)↑2)) gcd ((𝑁↑2) / ((𝑀 gcd 𝑁)↑2)))) |
34 | | nncn 10905 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
35 | 34 | adantr 480 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℂ) |
36 | 9 | nncnd 10913 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℂ) |
37 | 9 | nnne0d 10942 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ≠ 0) |
38 | 35, 36, 37 | sqdivd 12883 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 / (𝑀 gcd 𝑁))↑2) = ((𝑀↑2) / ((𝑀 gcd 𝑁)↑2))) |
39 | | nncn 10905 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
40 | 39 | adantl 481 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℂ) |
41 | 40, 36, 37 | sqdivd 12883 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 / (𝑀 gcd 𝑁))↑2) = ((𝑁↑2) / ((𝑀 gcd 𝑁)↑2))) |
42 | 38, 41 | oveq12d 6567 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 / (𝑀 gcd 𝑁))↑2) gcd ((𝑁 / (𝑀 gcd 𝑁))↑2)) = (((𝑀↑2) / ((𝑀 gcd 𝑁)↑2)) gcd ((𝑁↑2) / ((𝑀 gcd 𝑁)↑2)))) |
43 | | gcddiv 15106 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 gcd 𝑁) ∈ ℕ) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) → ((𝑀 gcd 𝑁) / (𝑀 gcd 𝑁)) = ((𝑀 / (𝑀 gcd 𝑁)) gcd (𝑁 / (𝑀 gcd 𝑁)))) |
44 | 23, 28, 9, 20, 43 | syl31anc 1321 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) / (𝑀 gcd 𝑁)) = ((𝑀 / (𝑀 gcd 𝑁)) gcd (𝑁 / (𝑀 gcd 𝑁)))) |
45 | 36, 37 | dividd 10678 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) / (𝑀 gcd 𝑁)) = 1) |
46 | 44, 45 | eqtr3d 2646 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 / (𝑀 gcd 𝑁)) gcd (𝑁 / (𝑀 gcd 𝑁))) = 1) |
47 | | dvdsval2 14824 |
. . . . . . . . 9
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ (𝑀 gcd 𝑁) ≠ 0 ∧ 𝑀 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ↔ (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ)) |
48 | 22, 37, 23, 47 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ↔ (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ)) |
49 | 21, 48 | mpbid 221 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ) |
50 | | nnre 10904 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
51 | 50 | adantr 480 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℝ) |
52 | 9 | nnred 10912 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℝ) |
53 | | nngt0 10926 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → 0 <
𝑀) |
54 | 53 | adantr 480 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 <
𝑀) |
55 | 9 | nngt0d 10941 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 <
(𝑀 gcd 𝑁)) |
56 | 51, 52, 54, 55 | divgt0d 10838 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 <
(𝑀 / (𝑀 gcd 𝑁))) |
57 | | elnnz 11264 |
. . . . . . 7
⊢ ((𝑀 / (𝑀 gcd 𝑁)) ∈ ℕ ↔ ((𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ ∧ 0 < (𝑀 / (𝑀 gcd 𝑁)))) |
58 | 49, 56, 57 | sylanbrc 695 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 / (𝑀 gcd 𝑁)) ∈ ℕ) |
59 | | dvdsval2 14824 |
. . . . . . . . 9
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ (𝑀 gcd 𝑁) ≠ 0 ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑁 ↔ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ)) |
60 | 22, 37, 28, 59 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑁 ↔ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ)) |
61 | 27, 60 | mpbid 221 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ) |
62 | | nnre 10904 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
63 | 62 | adantl 481 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ) |
64 | | nngt0 10926 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
65 | 64 | adantl 481 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 <
𝑁) |
66 | 63, 52, 65, 55 | divgt0d 10838 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 <
(𝑁 / (𝑀 gcd 𝑁))) |
67 | | elnnz 11264 |
. . . . . . 7
⊢ ((𝑁 / (𝑀 gcd 𝑁)) ∈ ℕ ↔ ((𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ ∧ 0 < (𝑁 / (𝑀 gcd 𝑁)))) |
68 | 61, 66, 67 | sylanbrc 695 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 / (𝑀 gcd 𝑁)) ∈ ℕ) |
69 | | 2nn 11062 |
. . . . . . 7
⊢ 2 ∈
ℕ |
70 | | rppwr 15115 |
. . . . . . 7
⊢ (((𝑀 / (𝑀 gcd 𝑁)) ∈ ℕ ∧ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℕ ∧ 2 ∈ ℕ)
→ (((𝑀 / (𝑀 gcd 𝑁)) gcd (𝑁 / (𝑀 gcd 𝑁))) = 1 → (((𝑀 / (𝑀 gcd 𝑁))↑2) gcd ((𝑁 / (𝑀 gcd 𝑁))↑2)) = 1)) |
71 | 69, 70 | mp3an3 1405 |
. . . . . 6
⊢ (((𝑀 / (𝑀 gcd 𝑁)) ∈ ℕ ∧ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℕ) → (((𝑀 / (𝑀 gcd 𝑁)) gcd (𝑁 / (𝑀 gcd 𝑁))) = 1 → (((𝑀 / (𝑀 gcd 𝑁))↑2) gcd ((𝑁 / (𝑀 gcd 𝑁))↑2)) = 1)) |
72 | 58, 68, 71 | syl2anc 691 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 / (𝑀 gcd 𝑁)) gcd (𝑁 / (𝑀 gcd 𝑁))) = 1 → (((𝑀 / (𝑀 gcd 𝑁))↑2) gcd ((𝑁 / (𝑀 gcd 𝑁))↑2)) = 1)) |
73 | 46, 72 | mpd 15 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 / (𝑀 gcd 𝑁))↑2) gcd ((𝑁 / (𝑀 gcd 𝑁))↑2)) = 1) |
74 | 33, 42, 73 | 3eqtr2d 2650 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀↑2) gcd (𝑁↑2)) / ((𝑀 gcd 𝑁)↑2)) = 1) |
75 | 14, 17 | anim12i 588 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀↑2) ∈ ℤ ∧
(𝑁↑2) ∈
ℤ)) |
76 | 13 | nnne0d 10942 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑀↑2) ≠
0) |
77 | 76 | neneqd 2787 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ¬
(𝑀↑2) =
0) |
78 | 77 | intnanrd 954 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ¬
((𝑀↑2) = 0 ∧
(𝑁↑2) =
0)) |
79 | 78 | adantr 480 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ¬
((𝑀↑2) = 0 ∧
(𝑁↑2) =
0)) |
80 | | gcdn0cl 15062 |
. . . . . 6
⊢ ((((𝑀↑2) ∈ ℤ ∧
(𝑁↑2) ∈ ℤ)
∧ ¬ ((𝑀↑2) = 0
∧ (𝑁↑2) = 0))
→ ((𝑀↑2) gcd
(𝑁↑2)) ∈
ℕ) |
81 | 75, 79, 80 | syl2anc 691 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀↑2) gcd (𝑁↑2)) ∈ ℕ) |
82 | 81 | nncnd 10913 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀↑2) gcd (𝑁↑2)) ∈ ℂ) |
83 | 10 | nnne0d 10942 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁)↑2) ≠ 0) |
84 | | ax-1cn 9873 |
. . . . 5
⊢ 1 ∈
ℂ |
85 | | divmul 10567 |
. . . . 5
⊢ ((((𝑀↑2) gcd (𝑁↑2)) ∈ ℂ ∧ 1 ∈
ℂ ∧ (((𝑀 gcd
𝑁)↑2) ∈ ℂ
∧ ((𝑀 gcd 𝑁)↑2) ≠ 0)) →
((((𝑀↑2) gcd (𝑁↑2)) / ((𝑀 gcd 𝑁)↑2)) = 1 ↔ (((𝑀 gcd 𝑁)↑2) · 1) = ((𝑀↑2) gcd (𝑁↑2)))) |
86 | 84, 85 | mp3an2 1404 |
. . . 4
⊢ ((((𝑀↑2) gcd (𝑁↑2)) ∈ ℂ ∧ (((𝑀 gcd 𝑁)↑2) ∈ ℂ ∧ ((𝑀 gcd 𝑁)↑2) ≠ 0)) → ((((𝑀↑2) gcd (𝑁↑2)) / ((𝑀 gcd 𝑁)↑2)) = 1 ↔ (((𝑀 gcd 𝑁)↑2) · 1) = ((𝑀↑2) gcd (𝑁↑2)))) |
87 | 82, 11, 83, 86 | syl12anc 1316 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
((((𝑀↑2) gcd (𝑁↑2)) / ((𝑀 gcd 𝑁)↑2)) = 1 ↔ (((𝑀 gcd 𝑁)↑2) · 1) = ((𝑀↑2) gcd (𝑁↑2)))) |
88 | 74, 87 | mpbid 221 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 gcd 𝑁)↑2) · 1) = ((𝑀↑2) gcd (𝑁↑2))) |
89 | 12, 88 | eqtr3d 2646 |
1
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁)↑2) = ((𝑀↑2) gcd (𝑁↑2))) |