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 ∈ ℕ
2	1	nnzi	⊢ 6 ∈ ℤ
3		9nn	⊢ 9 ∈ ℕ
4	3	nnzi	⊢ 9 ∈ ℤ
5		neggcd	⊢ ( ( 6 ∈ ℤ ∧ 9 ∈ ℤ ) → ( - 6 gcd 9 ) = ( 6 gcd 9 ) )
6	2 4 5	mp2an	⊢ ( - 6 gcd 9 ) = ( 6 gcd 9 )
7		6cn	⊢ 6 ∈ ℂ
8		3cn	⊢ 3 ∈ ℂ
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 ( 3 + 6 ) )
13		3z	⊢ 3 ∈ ℤ
14		gcdcom	⊢ ( ( 6 ∈ ℤ ∧ 3 ∈ ℤ ) → ( 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 ( 3 + 3 ) )
19	15 18	eqtri	⊢ ( 6 gcd 3 ) = ( 3 gcd ( 3 + 3 ) )
20		gcdadd	⊢ ( ( 6 ∈ ℤ ∧ 3 ∈ ℤ ) → ( 6 gcd 3 ) = ( 6 gcd ( 3 + 6 ) ) )
21	2 13 20	mp2an	⊢ ( 6 gcd 3 ) = ( 6 gcd ( 3 + 6 ) )
22		gcdid	⊢ ( 3 ∈ ℤ → ( 3 gcd 3 ) = ( abs ‘ 3 ) )
23	13 22	ax-mp	⊢ ( 3 gcd 3 ) = ( abs ‘ 3 )
24		gcdadd	⊢ ( ( 3 ∈ ℤ ∧ 3 ∈ ℤ ) → ( 3 gcd 3 ) = ( 3 gcd ( 3 + 3 ) ) )
25	13 13 24	mp2an	⊢ ( 3 gcd 3 ) = ( 3 gcd ( 3 + 3 ) )
26		3re	⊢ 3 ∈ ℝ
27		0re	⊢ 0 ∈ ℝ
28		3pos	⊢ 0 < 3
29	27 26 28	ltleii	⊢ 0 ≤ 3
30		absid	⊢ ( ( 3 ∈ ℝ ∧ 0 ≤ 3 ) → ( abs ‘ 3 ) = 3 )
31	26 29 30	mp2an	⊢ ( abs ‘ 3 ) = 3
32	23 25 31	3eqtr3i	⊢ ( 3 gcd ( 3 + 3 ) ) = 3
33	19 21 32	3eqtr3i	⊢ ( 6 gcd ( 3 + 6 ) ) = 3
34	12 33	eqtri	⊢ ( 6 gcd 9 ) = 3
35	6 34	eqtri	⊢ ( - 6 gcd 9 ) = 3