Metamath Proof Explorer

Theorem gcd0id

Description: The gcd of 0 and an integer is the integer's absolute value. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion gcd0id ⊢ N ∈ ℤ → 0 gcd N = N

Proof

Step Hyp Ref Expression
1 gcd0val ⊢ 0 gcd 0 = 0
2 oveq2 ⊢ N = 0 → 0 gcd N = 0 gcd 0
3 fveq2 ⊢ N = 0 → N = 0
4 abs0 ⊢ 0 = 0
5 3 4 eqtrdi ⊢ N = 0 → N = 0
6 1 2 5 3eqtr4a ⊢ N = 0 → 0 gcd N = N
7 6 adantl ⊢ N ∈ ℤ ∧ N = 0 → 0 gcd N = N
8 0z ⊢ 0 ∈ ℤ
9 gcddvds ⊢ 0 ∈ ℤ ∧ N ∈ ℤ → 0 gcd N ∥ 0 ∧ 0 gcd N ∥ N
10 8 9 mpan ⊢ N ∈ ℤ → 0 gcd N ∥ 0 ∧ 0 gcd N ∥ N
11 10 simprd ⊢ N ∈ ℤ → 0 gcd N ∥ N
12 11 adantr ⊢ N ∈ ℤ ∧ N ≠ 0 → 0 gcd N ∥ N
13 gcdcl ⊢ 0 ∈ ℤ ∧ N ∈ ℤ → 0 gcd N ∈ ℕ 0
14 8 13 mpan ⊢ N ∈ ℤ → 0 gcd N ∈ ℕ 0
15 14 nn0zd ⊢ N ∈ ℤ → 0 gcd N ∈ ℤ
16 dvdsleabs ⊢ 0 gcd N ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → 0 gcd N ∥ N → 0 gcd N ≤ N
17 15 16 syl3an1 ⊢ N ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → 0 gcd N ∥ N → 0 gcd N ≤ N
18 17 3anidm12 ⊢ N ∈ ℤ ∧ N ≠ 0 → 0 gcd N ∥ N → 0 gcd N ≤ N
19 12 18 mpd ⊢ N ∈ ℤ ∧ N ≠ 0 → 0 gcd N ≤ N
20 zabscl ⊢ N ∈ ℤ → N ∈ ℤ
21 dvds0 ⊢ N ∈ ℤ → N ∥ 0
22 20 21 syl ⊢ N ∈ ℤ → N ∥ 0
23 iddvds ⊢ N ∈ ℤ → N ∥ N
24 absdvdsb ⊢ N ∈ ℤ ∧ N ∈ ℤ → N ∥ N ↔ N ∥ N
25 24 anidms ⊢ N ∈ ℤ → N ∥ N ↔ N ∥ N
26 23 25 mpbid ⊢ N ∈ ℤ → N ∥ N
27 22 26 jca ⊢ N ∈ ℤ → N ∥ 0 ∧ N ∥ N
28 27 adantr ⊢ N ∈ ℤ ∧ N ≠ 0 → N ∥ 0 ∧ N ∥ N
29 eqid ⊢ 0 = 0
30 29 biantrur ⊢ N = 0 ↔ 0 = 0 ∧ N = 0
31 30 necon3abii ⊢ N ≠ 0 ↔ ¬ 0 = 0 ∧ N = 0
32 dvdslegcd ⊢ N ∈ ℤ ∧ 0 ∈ ℤ ∧ N ∈ ℤ ∧ ¬ 0 = 0 ∧ N = 0 → N ∥ 0 ∧ N ∥ N → N ≤ 0 gcd N
33 32 ex ⊢ N ∈ ℤ ∧ 0 ∈ ℤ ∧ N ∈ ℤ → ¬ 0 = 0 ∧ N = 0 → N ∥ 0 ∧ N ∥ N → N ≤ 0 gcd N
34 8 33 mp3an2 ⊢ N ∈ ℤ ∧ N ∈ ℤ → ¬ 0 = 0 ∧ N = 0 → N ∥ 0 ∧ N ∥ N → N ≤ 0 gcd N
35 20 34 mpancom ⊢ N ∈ ℤ → ¬ 0 = 0 ∧ N = 0 → N ∥ 0 ∧ N ∥ N → N ≤ 0 gcd N
36 31 35 biimtrid ⊢ N ∈ ℤ → N ≠ 0 → N ∥ 0 ∧ N ∥ N → N ≤ 0 gcd N
37 36 imp ⊢ N ∈ ℤ ∧ N ≠ 0 → N ∥ 0 ∧ N ∥ N → N ≤ 0 gcd N
38 28 37 mpd ⊢ N ∈ ℤ ∧ N ≠ 0 → N ≤ 0 gcd N
39 15 zred ⊢ N ∈ ℤ → 0 gcd N ∈ ℝ
40 20 zred ⊢ N ∈ ℤ → N ∈ ℝ
41 39 40 letri3d ⊢ N ∈ ℤ → 0 gcd N = N ↔ 0 gcd N ≤ N ∧ N ≤ 0 gcd N
42 41 adantr ⊢ N ∈ ℤ ∧ N ≠ 0 → 0 gcd N = N ↔ 0 gcd N ≤ N ∧ N ≤ 0 gcd N
43 19 38 42 mpbir2and ⊢ N ∈ ℤ ∧ N ≠ 0 → 0 gcd N = N
44 7 43 pm2.61dane ⊢ N ∈ ℤ → 0 gcd N = N