Theorem ex-gcd

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

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

Proof

Step	Hyp	Ref	Expression
1		6nn	$$⊢6\in \mathbb{N}$$
2	1	nnzi	$$⊢6\in \mathbb{Z}$$
3		9nn	$$⊢9\in \mathbb{N}$$
4	3	nnzi	$$⊢9\in \mathbb{Z}$$
5		neggcd	$$⊢\left(6\in \mathbb{Z}\wedge 9\in \mathbb{Z}\right)\to -6\gcd 9=6\gcd 9$$
6	2 4 5	mp2an	$$⊢-6\gcd 9=6\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\gcd 9=6\gcd \left(3+6\right)$$
13		3z	$$⊢3\in \mathbb{Z}$$
14		gcdcom	$$⊢\left(6\in \mathbb{Z}\wedge 3\in \mathbb{Z}\right)\to 6\gcd 3=3\gcd 6$$
15	2 13 14	mp2an	$$⊢6\gcd 3=3\gcd 6$$
16		3p3e6	$$⊢3+3=6$$
17	16	eqcomi	$$⊢6=3+3$$
18	17	oveq2i	$$⊢3\gcd 6=3\gcd \left(3+3\right)$$
19	15 18	eqtri	$$⊢6\gcd 3=3\gcd \left(3+3\right)$$
20		gcdadd	$$⊢\left(6\in \mathbb{Z}\wedge 3\in \mathbb{Z}\right)\to 6\gcd 3=6\gcd \left(3+6\right)$$
21	2 13 20	mp2an	$$⊢6\gcd 3=6\gcd \left(3+6\right)$$
22		gcdid	$$⊢3\in \mathbb{Z}\to 3\gcd 3=\left|3\right|$$
23	13 22	ax-mp	$$⊢3\gcd 3=\left|3\right|$$
24		gcdadd	$$⊢\left(3\in \mathbb{Z}\wedge 3\in \mathbb{Z}\right)\to 3\gcd 3=3\gcd \left(3+3\right)$$
25	13 13 24	mp2an	$$⊢3\gcd 3=3\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\gcd \left(3+3\right)=3$$
33	19 21 32	3eqtr3i	$$⊢6\gcd \left(3+6\right)=3$$
34	12 33	eqtri	$$⊢6\gcd 9=3$$
35	6 34	eqtri	$$⊢-6\gcd 9=3$$