# Metamath Proof Explorer

## Theorem ex-gcd

Description: Example for df-gcd . (Contributed by AV, 5-Sep-2021)

Ref Expression
Assertion ex-gcd ${⊢}-6\mathrm{gcd}9=3$

### Proof

Step Hyp Ref Expression
1 6nn ${⊢}6\in ℕ$
2 1 nnzi ${⊢}6\in ℤ$
3 9nn ${⊢}9\in ℕ$
4 3 nnzi ${⊢}9\in ℤ$
5 neggcd ${⊢}\left(6\in ℤ\wedge 9\in ℤ\right)\to -6\mathrm{gcd}9=6\mathrm{gcd}9$
6 2 4 5 mp2an ${⊢}-6\mathrm{gcd}9=6\mathrm{gcd}9$
7 6cn ${⊢}6\in ℂ$
8 3cn ${⊢}3\in ℂ$
9 6p3e9 ${⊢}6+3=9$
10 7 8 9 addcomli ${⊢}3+6=9$
11 10 eqcomi ${⊢}9=3+6$
12 11 oveq2i ${⊢}6\mathrm{gcd}9=6\mathrm{gcd}\left(3+6\right)$
13 3z ${⊢}3\in ℤ$
14 gcdcom ${⊢}\left(6\in ℤ\wedge 3\in ℤ\right)\to 6\mathrm{gcd}3=3\mathrm{gcd}6$
15 2 13 14 mp2an ${⊢}6\mathrm{gcd}3=3\mathrm{gcd}6$
16 3p3e6 ${⊢}3+3=6$
17 16 eqcomi ${⊢}6=3+3$
18 17 oveq2i ${⊢}3\mathrm{gcd}6=3\mathrm{gcd}\left(3+3\right)$
19 15 18 eqtri ${⊢}6\mathrm{gcd}3=3\mathrm{gcd}\left(3+3\right)$
20 gcdadd ${⊢}\left(6\in ℤ\wedge 3\in ℤ\right)\to 6\mathrm{gcd}3=6\mathrm{gcd}\left(3+6\right)$
21 2 13 20 mp2an ${⊢}6\mathrm{gcd}3=6\mathrm{gcd}\left(3+6\right)$
22 gcdid ${⊢}3\in ℤ\to 3\mathrm{gcd}3=\left|3\right|$
23 13 22 ax-mp ${⊢}3\mathrm{gcd}3=\left|3\right|$
24 gcdadd ${⊢}\left(3\in ℤ\wedge 3\in ℤ\right)\to 3\mathrm{gcd}3=3\mathrm{gcd}\left(3+3\right)$
25 13 13 24 mp2an ${⊢}3\mathrm{gcd}3=3\mathrm{gcd}\left(3+3\right)$
26 3re ${⊢}3\in ℝ$
27 0re ${⊢}0\in ℝ$
28 3pos ${⊢}0<3$
29 27 26 28 ltleii ${⊢}0\le 3$
30 absid ${⊢}\left(3\in ℝ\wedge 0\le 3\right)\to \left|3\right|=3$
31 26 29 30 mp2an ${⊢}\left|3\right|=3$
32 23 25 31 3eqtr3i ${⊢}3\mathrm{gcd}\left(3+3\right)=3$
33 19 21 32 3eqtr3i ${⊢}6\mathrm{gcd}\left(3+6\right)=3$
34 12 33 eqtri ${⊢}6\mathrm{gcd}9=3$
35 6 34 eqtri ${⊢}-6\mathrm{gcd}9=3$