Metamath Proof Explorer

Theorem ex-gcd

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

Ref Expression
Assertion ex-gcd 
|- ( -u 6 gcd 9 ) = 3

Proof

Step Hyp Ref Expression
1 6nn 
 |-  6 e. NN
2 1 nnzi 
 |-  6 e. ZZ
3 9nn 
 |-  9 e. NN
4 3 nnzi 
 |-  9 e. ZZ
5 neggcd 
 |-  ( ( 6 e. ZZ /\ 9 e. ZZ ) -> ( -u 6 gcd 9 ) = ( 6 gcd 9 ) )
6 2 4 5 mp2an 
 |-  ( -u 6 gcd 9 ) = ( 6 gcd 9 )
7 6cn 
 |-  6 e. CC
8 3cn 
 |-  3 e. CC
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 e. ZZ
14 gcdcom 
 |-  ( ( 6 e. ZZ /\ 3 e. ZZ ) -> ( 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 e. ZZ /\ 3 e. ZZ ) -> ( 6 gcd 3 ) = ( 6 gcd ( 3 + 6 ) ) )
21 2 13 20 mp2an 
 |-  ( 6 gcd 3 ) = ( 6 gcd ( 3 + 6 ) )
22 gcdid 
 |-  ( 3 e. ZZ -> ( 3 gcd 3 ) = ( abs ` 3 ) )
23 13 22 ax-mp 
 |-  ( 3 gcd 3 ) = ( abs ` 3 )
24 gcdadd 
 |-  ( ( 3 e. ZZ /\ 3 e. ZZ ) -> ( 3 gcd 3 ) = ( 3 gcd ( 3 + 3 ) ) )
25 13 13 24 mp2an 
 |-  ( 3 gcd 3 ) = ( 3 gcd ( 3 + 3 ) )
26 3re 
 |-  3 e. RR
27 0re 
 |-  0 e. RR
28 3pos 
 |-  0 < 3
29 27 26 28 ltleii 
 |-  0 <_ 3
30 absid 
 |-  ( ( 3 e. RR /\ 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 
 |-  ( -u 6 gcd 9 ) = 3