This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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