Proof of Theorem sqgcd
| Step | Hyp | Ref
| Expression |
| 1 | | gcdnncl 16544 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℕ) |
| 2 | 1 | nnsqcld 14283 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁)↑2) ∈ ℕ) |
| 3 | 2 | nncnd 12282 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁)↑2) ∈ ℂ) |
| 4 | 3 | mulridd 11278 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 gcd 𝑁)↑2) · 1) = ((𝑀 gcd 𝑁)↑2)) |
| 5 | | nnsqcl 14168 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (𝑀↑2) ∈
ℕ) |
| 6 | 5 | nnzd 12640 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (𝑀↑2) ∈
ℤ) |
| 7 | 6 | adantr 480 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀↑2) ∈
ℤ) |
| 8 | | nnsqcl 14168 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁↑2) ∈
ℕ) |
| 9 | 8 | nnzd 12640 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑁↑2) ∈
ℤ) |
| 10 | 9 | adantl 481 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁↑2) ∈
ℤ) |
| 11 | | nnz 12634 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
| 12 | | nnz 12634 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
| 13 | | gcddvds 16540 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) |
| 14 | 11, 12, 13 | syl2an 596 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) |
| 15 | 14 | simpld 494 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∥ 𝑀) |
| 16 | 1 | nnzd 12640 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℤ) |
| 17 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℤ) |
| 18 | | dvdssqim 16591 |
. . . . . . 7
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 → ((𝑀 gcd 𝑁)↑2) ∥ (𝑀↑2))) |
| 19 | 16, 17, 18 | syl2anc 584 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑀 → ((𝑀 gcd 𝑁)↑2) ∥ (𝑀↑2))) |
| 20 | 15, 19 | mpd 15 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁)↑2) ∥ (𝑀↑2)) |
| 21 | 14 | simprd 495 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∥ 𝑁) |
| 22 | 12 | adantl 481 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℤ) |
| 23 | | dvdssqim 16591 |
. . . . . . 7
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑁 → ((𝑀 gcd 𝑁)↑2) ∥ (𝑁↑2))) |
| 24 | 16, 22, 23 | syl2anc 584 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑁 → ((𝑀 gcd 𝑁)↑2) ∥ (𝑁↑2))) |
| 25 | 21, 24 | mpd 15 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁)↑2) ∥ (𝑁↑2)) |
| 26 | | gcddiv 16588 |
. . . . 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 1380 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀↑2) gcd (𝑁↑2)) / ((𝑀 gcd 𝑁)↑2)) = (((𝑀↑2) / ((𝑀 gcd 𝑁)↑2)) gcd ((𝑁↑2) / ((𝑀 gcd 𝑁)↑2)))) |
| 28 | | nncn 12274 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
| 29 | 28 | adantr 480 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℂ) |
| 30 | 1 | nncnd 12282 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℂ) |
| 31 | 1 | nnne0d 12316 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ≠ 0) |
| 32 | 29, 30, 31 | sqdivd 14199 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 / (𝑀 gcd 𝑁))↑2) = ((𝑀↑2) / ((𝑀 gcd 𝑁)↑2))) |
| 33 | | nncn 12274 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
| 34 | 33 | adantl 481 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℂ) |
| 35 | 34, 30, 31 | sqdivd 14199 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 / (𝑀 gcd 𝑁))↑2) = ((𝑁↑2) / ((𝑀 gcd 𝑁)↑2))) |
| 36 | 32, 35 | oveq12d 7449 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 / (𝑀 gcd 𝑁))↑2) gcd ((𝑁 / (𝑀 gcd 𝑁))↑2)) = (((𝑀↑2) / ((𝑀 gcd 𝑁)↑2)) gcd ((𝑁↑2) / ((𝑀 gcd 𝑁)↑2)))) |
| 37 | | gcddiv 16588 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 gcd 𝑁) ∈ ℕ) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) → ((𝑀 gcd 𝑁) / (𝑀 gcd 𝑁)) = ((𝑀 / (𝑀 gcd 𝑁)) gcd (𝑁 / (𝑀 gcd 𝑁)))) |
| 38 | 17, 22, 1, 14, 37 | syl31anc 1375 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) / (𝑀 gcd 𝑁)) = ((𝑀 / (𝑀 gcd 𝑁)) gcd (𝑁 / (𝑀 gcd 𝑁)))) |
| 39 | 30, 31 | dividd 12041 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) / (𝑀 gcd 𝑁)) = 1) |
| 40 | 38, 39 | eqtr3d 2779 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 / (𝑀 gcd 𝑁)) gcd (𝑁 / (𝑀 gcd 𝑁))) = 1) |
| 41 | | dvdsval2 16293 |
. . . . . . . . 9
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ (𝑀 gcd 𝑁) ≠ 0 ∧ 𝑀 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ↔ (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ)) |
| 42 | 16, 31, 17, 41 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ↔ (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ)) |
| 43 | 15, 42 | mpbid 232 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ) |
| 44 | | nnre 12273 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
| 45 | 44 | adantr 480 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℝ) |
| 46 | 1 | nnred 12281 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℝ) |
| 47 | | nngt0 12297 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → 0 <
𝑀) |
| 48 | 47 | adantr 480 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 <
𝑀) |
| 49 | 1 | nngt0d 12315 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 <
(𝑀 gcd 𝑁)) |
| 50 | 45, 46, 48, 49 | divgt0d 12203 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 <
(𝑀 / (𝑀 gcd 𝑁))) |
| 51 | | elnnz 12623 |
. . . . . . 7
⊢ ((𝑀 / (𝑀 gcd 𝑁)) ∈ ℕ ↔ ((𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ ∧ 0 < (𝑀 / (𝑀 gcd 𝑁)))) |
| 52 | 43, 50, 51 | sylanbrc 583 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 / (𝑀 gcd 𝑁)) ∈ ℕ) |
| 53 | | dvdsval2 16293 |
. . . . . . . . 9
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ (𝑀 gcd 𝑁) ≠ 0 ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑁 ↔ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ)) |
| 54 | 16, 31, 22, 53 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑁 ↔ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ)) |
| 55 | 21, 54 | mpbid 232 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ) |
| 56 | | nnre 12273 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
| 57 | 56 | adantl 481 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ) |
| 58 | | nngt0 12297 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
| 59 | 58 | adantl 481 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 <
𝑁) |
| 60 | 57, 46, 59, 49 | divgt0d 12203 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 <
(𝑁 / (𝑀 gcd 𝑁))) |
| 61 | | elnnz 12623 |
. . . . . . 7
⊢ ((𝑁 / (𝑀 gcd 𝑁)) ∈ ℕ ↔ ((𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ ∧ 0 < (𝑁 / (𝑀 gcd 𝑁)))) |
| 62 | 55, 60, 61 | sylanbrc 583 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 / (𝑀 gcd 𝑁)) ∈ ℕ) |
| 63 | | 2nn 12339 |
. . . . . . 7
⊢ 2 ∈
ℕ |
| 64 | | rppwr 16597 |
. . . . . . 7
⊢ (((𝑀 / (𝑀 gcd 𝑁)) ∈ ℕ ∧ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℕ ∧ 2 ∈ ℕ)
→ (((𝑀 / (𝑀 gcd 𝑁)) gcd (𝑁 / (𝑀 gcd 𝑁))) = 1 → (((𝑀 / (𝑀 gcd 𝑁))↑2) gcd ((𝑁 / (𝑀 gcd 𝑁))↑2)) = 1)) |
| 65 | 63, 64 | mp3an3 1452 |
. . . . . 6
⊢ (((𝑀 / (𝑀 gcd 𝑁)) ∈ ℕ ∧ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℕ) → (((𝑀 / (𝑀 gcd 𝑁)) gcd (𝑁 / (𝑀 gcd 𝑁))) = 1 → (((𝑀 / (𝑀 gcd 𝑁))↑2) gcd ((𝑁 / (𝑀 gcd 𝑁))↑2)) = 1)) |
| 66 | 52, 62, 65 | syl2anc 584 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 / (𝑀 gcd 𝑁)) gcd (𝑁 / (𝑀 gcd 𝑁))) = 1 → (((𝑀 / (𝑀 gcd 𝑁))↑2) gcd ((𝑁 / (𝑀 gcd 𝑁))↑2)) = 1)) |
| 67 | 40, 66 | mpd 15 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 / (𝑀 gcd 𝑁))↑2) gcd ((𝑁 / (𝑀 gcd 𝑁))↑2)) = 1) |
| 68 | 27, 36, 67 | 3eqtr2d 2783 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀↑2) gcd (𝑁↑2)) / ((𝑀 gcd 𝑁)↑2)) = 1) |
| 69 | 6, 9 | anim12i 613 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀↑2) ∈ ℤ ∧
(𝑁↑2) ∈
ℤ)) |
| 70 | 5 | nnne0d 12316 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑀↑2) ≠
0) |
| 71 | 70 | neneqd 2945 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ¬
(𝑀↑2) =
0) |
| 72 | 71 | intnanrd 489 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ¬
((𝑀↑2) = 0 ∧
(𝑁↑2) =
0)) |
| 73 | 72 | adantr 480 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ¬
((𝑀↑2) = 0 ∧
(𝑁↑2) =
0)) |
| 74 | | gcdn0cl 16539 |
. . . . . 6
⊢ ((((𝑀↑2) ∈ ℤ ∧
(𝑁↑2) ∈ ℤ)
∧ ¬ ((𝑀↑2) = 0
∧ (𝑁↑2) = 0))
→ ((𝑀↑2) gcd
(𝑁↑2)) ∈
ℕ) |
| 75 | 69, 73, 74 | syl2anc 584 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀↑2) gcd (𝑁↑2)) ∈ ℕ) |
| 76 | 75 | nncnd 12282 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀↑2) gcd (𝑁↑2)) ∈ ℂ) |
| 77 | 2 | nnne0d 12316 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁)↑2) ≠ 0) |
| 78 | | ax-1cn 11213 |
. . . . 5
⊢ 1 ∈
ℂ |
| 79 | | divmul 11925 |
. . . . 5
⊢ ((((𝑀↑2) gcd (𝑁↑2)) ∈ ℂ ∧ 1 ∈
ℂ ∧ (((𝑀 gcd
𝑁)↑2) ∈ ℂ
∧ ((𝑀 gcd 𝑁)↑2) ≠ 0)) →
((((𝑀↑2) gcd (𝑁↑2)) / ((𝑀 gcd 𝑁)↑2)) = 1 ↔ (((𝑀 gcd 𝑁)↑2) · 1) = ((𝑀↑2) gcd (𝑁↑2)))) |
| 80 | 78, 79 | mp3an2 1451 |
. . . 4
⊢ ((((𝑀↑2) gcd (𝑁↑2)) ∈ ℂ ∧ (((𝑀 gcd 𝑁)↑2) ∈ ℂ ∧ ((𝑀 gcd 𝑁)↑2) ≠ 0)) → ((((𝑀↑2) gcd (𝑁↑2)) / ((𝑀 gcd 𝑁)↑2)) = 1 ↔ (((𝑀 gcd 𝑁)↑2) · 1) = ((𝑀↑2) gcd (𝑁↑2)))) |
| 81 | 76, 3, 77, 80 | syl12anc 837 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
((((𝑀↑2) gcd (𝑁↑2)) / ((𝑀 gcd 𝑁)↑2)) = 1 ↔ (((𝑀 gcd 𝑁)↑2) · 1) = ((𝑀↑2) gcd (𝑁↑2)))) |
| 82 | 68, 81 | mpbid 232 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 gcd 𝑁)↑2) · 1) = ((𝑀↑2) gcd (𝑁↑2))) |
| 83 | 4, 82 | eqtr3d 2779 |
1
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁)↑2) = ((𝑀↑2) gcd (𝑁↑2))) |