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∈ℤ→0gcdN=N

Proof

Step Hyp Ref Expression
1 gcd0val ⊢0gcd0=0
2 oveq2 ⊢N=0→0gcdN=0gcd0
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→0gcdN=N
7 6 adantl ⊢N∈ℤ∧N=0→0gcdN=N
8 0z ⊢0∈ℤ
9 gcddvds ⊢0∈ℤ∧N∈ℤ→0gcdN∥0∧0gcdN∥N
10 8 9 mpan ⊢N∈ℤ→0gcdN∥0∧0gcdN∥N
11 10 simprd ⊢N∈ℤ→0gcdN∥N
12 11 adantr ⊢N∈ℤ∧N≠0→0gcdN∥N
13 gcdcl ⊢0∈ℤ∧N∈ℤ→0gcdN∈ℕ0
14 8 13 mpan ⊢N∈ℤ→0gcdN∈ℕ0
15 14 nn0zd ⊢N∈ℤ→0gcdN∈ℤ
16 dvdsleabs ⊢0gcdN∈ℤ∧N∈ℤ∧N≠0→0gcdN∥N→0gcdN≤N
17 15 16 syl3an1 ⊢N∈ℤ∧N∈ℤ∧N≠0→0gcdN∥N→0gcdN≤N
18 17 3anidm12 ⊢N∈ℤ∧N≠0→0gcdN∥N→0gcdN≤N
19 12 18 mpd ⊢N∈ℤ∧N≠0→0gcdN≤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≤0gcdN
33 32 ex ⊢N∈ℤ∧0∈ℤ∧N∈ℤ→¬0=0∧N=0→N∥0∧N∥N→N≤0gcdN
34 8 33 mp3an2 ⊢N∈ℤ∧N∈ℤ→¬0=0∧N=0→N∥0∧N∥N→N≤0gcdN
35 20 34 mpancom ⊢N∈ℤ→¬0=0∧N=0→N∥0∧N∥N→N≤0gcdN
36 31 35 biimtrid ⊢N∈ℤ→N≠0→N∥0∧N∥N→N≤0gcdN
37 36 imp ⊢N∈ℤ∧N≠0→N∥0∧N∥N→N≤0gcdN
38 28 37 mpd ⊢N∈ℤ∧N≠0→N≤0gcdN
39 15 zred ⊢N∈ℤ→0gcdN∈ℝ
40 20 zred ⊢N∈ℤ→N∈ℝ
41 39 40 letri3d ⊢N∈ℤ→0gcdN=N↔0gcdN≤N∧N≤0gcdN
42 41 adantr ⊢N∈ℤ∧N≠0→0gcdN=N↔0gcdN≤N∧N≤0gcdN
43 19 38 42 mpbir2and ⊢N∈ℤ∧N≠0→0gcdN=N
44 7 43 pm2.61dane ⊢N∈ℤ→0gcdN=N