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 syl5bi 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