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