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 ( 𝑁 ∈ ℤ → ( 0 gcd 𝑁 ) = ( abs ‘ 𝑁 ) )

Proof

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