Proof of Theorem gcd0id
| Step | Hyp | Ref
| Expression |
| 1 | | gcd0val 16534 |
. . . 4
⊢ (0 gcd 0)
= 0 |
| 2 | | oveq2 7439 |
. . . 4
⊢ (𝑁 = 0 → (0 gcd 𝑁) = (0 gcd 0)) |
| 3 | | fveq2 6906 |
. . . . 5
⊢ (𝑁 = 0 → (abs‘𝑁) =
(abs‘0)) |
| 4 | | abs0 15324 |
. . . . 5
⊢
(abs‘0) = 0 |
| 5 | 3, 4 | eqtrdi 2793 |
. . . 4
⊢ (𝑁 = 0 → (abs‘𝑁) = 0) |
| 6 | 1, 2, 5 | 3eqtr4a 2803 |
. . 3
⊢ (𝑁 = 0 → (0 gcd 𝑁) = (abs‘𝑁)) |
| 7 | 6 | adantl 481 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 = 0) → (0 gcd 𝑁) = (abs‘𝑁)) |
| 8 | | 0z 12624 |
. . . . . . 7
⊢ 0 ∈
ℤ |
| 9 | | gcddvds 16540 |
. . . . . . 7
⊢ ((0
∈ ℤ ∧ 𝑁
∈ ℤ) → ((0 gcd 𝑁) ∥ 0 ∧ (0 gcd 𝑁) ∥ 𝑁)) |
| 10 | 8, 9 | mpan 690 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → ((0 gcd
𝑁) ∥ 0 ∧ (0 gcd
𝑁) ∥ 𝑁)) |
| 11 | 10 | simprd 495 |
. . . . 5
⊢ (𝑁 ∈ ℤ → (0 gcd
𝑁) ∥ 𝑁) |
| 12 | 11 | adantr 480 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (0 gcd 𝑁) ∥ 𝑁) |
| 13 | | gcdcl 16543 |
. . . . . . . 8
⊢ ((0
∈ ℤ ∧ 𝑁
∈ ℤ) → (0 gcd 𝑁) ∈
ℕ0) |
| 14 | 8, 13 | mpan 690 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → (0 gcd
𝑁) ∈
ℕ0) |
| 15 | 14 | nn0zd 12639 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (0 gcd
𝑁) ∈
ℤ) |
| 16 | | dvdsleabs 16348 |
. . . . . 6
⊢ (((0 gcd
𝑁) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
𝑁 ≠ 0) → ((0 gcd
𝑁) ∥ 𝑁 → (0 gcd 𝑁) ≤ (abs‘𝑁))) |
| 17 | 15, 16 | syl3an1 1164 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((0 gcd 𝑁) ∥ 𝑁 → (0 gcd 𝑁) ≤ (abs‘𝑁))) |
| 18 | 17 | 3anidm12 1421 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((0 gcd 𝑁) ∥ 𝑁 → (0 gcd 𝑁) ≤ (abs‘𝑁))) |
| 19 | 12, 18 | mpd 15 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (0 gcd 𝑁) ≤ (abs‘𝑁)) |
| 20 | | zabscl 15352 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ →
(abs‘𝑁) ∈
ℤ) |
| 21 | | dvds0 16309 |
. . . . . . 7
⊢
((abs‘𝑁)
∈ ℤ → (abs‘𝑁) ∥ 0) |
| 22 | 20, 21 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈ ℤ →
(abs‘𝑁) ∥
0) |
| 23 | | iddvds 16307 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → 𝑁 ∥ 𝑁) |
| 24 | | absdvdsb 16312 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∥ 𝑁 ↔ (abs‘𝑁) ∥ 𝑁)) |
| 25 | 24 | anidms 566 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → (𝑁 ∥ 𝑁 ↔ (abs‘𝑁) ∥ 𝑁)) |
| 26 | 23, 25 | mpbid 232 |
. . . . . 6
⊢ (𝑁 ∈ ℤ →
(abs‘𝑁) ∥ 𝑁) |
| 27 | 22, 26 | jca 511 |
. . . . 5
⊢ (𝑁 ∈ ℤ →
((abs‘𝑁) ∥ 0
∧ (abs‘𝑁) ∥
𝑁)) |
| 28 | 27 | adantr 480 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) →
((abs‘𝑁) ∥ 0
∧ (abs‘𝑁) ∥
𝑁)) |
| 29 | | eqid 2737 |
. . . . . . . 8
⊢ 0 =
0 |
| 30 | 29 | biantrur 530 |
. . . . . . 7
⊢ (𝑁 = 0 ↔ (0 = 0 ∧ 𝑁 = 0)) |
| 31 | 30 | necon3abii 2987 |
. . . . . 6
⊢ (𝑁 ≠ 0 ↔ ¬ (0 = 0
∧ 𝑁 =
0)) |
| 32 | | dvdslegcd 16541 |
. . . . . . . . 9
⊢
((((abs‘𝑁)
∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (0 = 0 ∧
𝑁 = 0)) →
(((abs‘𝑁) ∥ 0
∧ (abs‘𝑁) ∥
𝑁) → (abs‘𝑁) ≤ (0 gcd 𝑁))) |
| 33 | 32 | ex 412 |
. . . . . . . 8
⊢
(((abs‘𝑁)
∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (0 = 0 ∧
𝑁 = 0) →
(((abs‘𝑁) ∥ 0
∧ (abs‘𝑁) ∥
𝑁) → (abs‘𝑁) ≤ (0 gcd 𝑁)))) |
| 34 | 8, 33 | mp3an2 1451 |
. . . . . . 7
⊢
(((abs‘𝑁)
∈ ℤ ∧ 𝑁
∈ ℤ) → (¬ (0 = 0 ∧ 𝑁 = 0) → (((abs‘𝑁) ∥ 0 ∧ (abs‘𝑁) ∥ 𝑁) → (abs‘𝑁) ≤ (0 gcd 𝑁)))) |
| 35 | 20, 34 | mpancom 688 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (¬ (0
= 0 ∧ 𝑁 = 0) →
(((abs‘𝑁) ∥ 0
∧ (abs‘𝑁) ∥
𝑁) → (abs‘𝑁) ≤ (0 gcd 𝑁)))) |
| 36 | 31, 35 | biimtrid 242 |
. . . . 5
⊢ (𝑁 ∈ ℤ → (𝑁 ≠ 0 →
(((abs‘𝑁) ∥ 0
∧ (abs‘𝑁) ∥
𝑁) → (abs‘𝑁) ≤ (0 gcd 𝑁)))) |
| 37 | 36 | imp 406 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) →
(((abs‘𝑁) ∥ 0
∧ (abs‘𝑁) ∥
𝑁) → (abs‘𝑁) ≤ (0 gcd 𝑁))) |
| 38 | 28, 37 | mpd 15 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ≤ (0 gcd 𝑁)) |
| 39 | 15 | zred 12722 |
. . . . 5
⊢ (𝑁 ∈ ℤ → (0 gcd
𝑁) ∈
ℝ) |
| 40 | 20 | zred 12722 |
. . . . 5
⊢ (𝑁 ∈ ℤ →
(abs‘𝑁) ∈
ℝ) |
| 41 | 39, 40 | letri3d 11403 |
. . . 4
⊢ (𝑁 ∈ ℤ → ((0 gcd
𝑁) = (abs‘𝑁) ↔ ((0 gcd 𝑁) ≤ (abs‘𝑁) ∧ (abs‘𝑁) ≤ (0 gcd 𝑁)))) |
| 42 | 41 | adantr 480 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((0 gcd 𝑁) = (abs‘𝑁) ↔ ((0 gcd 𝑁) ≤ (abs‘𝑁) ∧ (abs‘𝑁) ≤ (0 gcd 𝑁)))) |
| 43 | 19, 38, 42 | mpbir2and 713 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (0 gcd 𝑁) = (abs‘𝑁)) |
| 44 | 7, 43 | pm2.61dane 3029 |
1
⊢ (𝑁 ∈ ℤ → (0 gcd
𝑁) = (abs‘𝑁)) |