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

Metamath Proof Explorer

Theorem 6gcd4e2

Description: The greatest common divisor of six and four is two. To calculate this gcd, a simple form of Euclid's algorithm is used: ( 6 gcd 4 ) = ( ( 4 + 2 ) gcd 4 ) = ( 2 gcd 4 ) and ( 2 gcd 4 ) = ( 2 gcd ( 2 + 2 ) ) = ( 2 gcd 2 ) = 2 . (Contributed by AV, 27-Aug-2020)

Ref Expression
Assertion 6gcd4e2 
|- ( 6 gcd 4 ) = 2

Proof

Step Hyp Ref Expression
1 6nn 
 |-  6 e. NN
2 1 nnzi 
 |-  6 e. ZZ
3 4z 
 |-  4 e. ZZ
4 gcdcom 
 |-  ( ( 6 e. ZZ /\ 4 e. ZZ ) -> ( 6 gcd 4 ) = ( 4 gcd 6 ) )
5 2 3 4 mp2an 
 |-  ( 6 gcd 4 ) = ( 4 gcd 6 )
6 4cn 
 |-  4 e. CC
7 2cn 
 |-  2 e. CC
8 4p2e6 
 |-  ( 4 + 2 ) = 6
9 6 7 8 addcomli 
 |-  ( 2 + 4 ) = 6
10 9 oveq2i 
 |-  ( 4 gcd ( 2 + 4 ) ) = ( 4 gcd 6 )
11 2z 
 |-  2 e. ZZ
12 gcdadd 
 |-  ( ( 2 e. ZZ /\ 2 e. ZZ ) -> ( 2 gcd 2 ) = ( 2 gcd ( 2 + 2 ) ) )
13 11 11 12 mp2an 
 |-  ( 2 gcd 2 ) = ( 2 gcd ( 2 + 2 ) )
14 2p2e4 
 |-  ( 2 + 2 ) = 4
15 14 oveq2i 
 |-  ( 2 gcd ( 2 + 2 ) ) = ( 2 gcd 4 )
16 gcdcom 
 |-  ( ( 2 e. ZZ /\ 4 e. ZZ ) -> ( 2 gcd 4 ) = ( 4 gcd 2 ) )
17 11 3 16 mp2an 
 |-  ( 2 gcd 4 ) = ( 4 gcd 2 )
18 15 17 eqtri 
 |-  ( 2 gcd ( 2 + 2 ) ) = ( 4 gcd 2 )
19 13 18 eqtri 
 |-  ( 2 gcd 2 ) = ( 4 gcd 2 )
20 gcdid 
 |-  ( 2 e. ZZ -> ( 2 gcd 2 ) = ( abs ` 2 ) )
21 11 20 ax-mp 
 |-  ( 2 gcd 2 ) = ( abs ` 2 )
22 2re 
 |-  2 e. RR
23 0le2 
 |-  0 <_ 2
24 absid 
 |-  ( ( 2 e. RR /\ 0 <_ 2 ) -> ( abs ` 2 ) = 2 )
25 22 23 24 mp2an 
 |-  ( abs ` 2 ) = 2
26 21 25 eqtri 
 |-  ( 2 gcd 2 ) = 2
27 gcdadd 
 |-  ( ( 4 e. ZZ /\ 2 e. ZZ ) -> ( 4 gcd 2 ) = ( 4 gcd ( 2 + 4 ) ) )
28 3 11 27 mp2an 
 |-  ( 4 gcd 2 ) = ( 4 gcd ( 2 + 4 ) )
29 19 26 28 3eqtr3ri 
 |-  ( 4 gcd ( 2 + 4 ) ) = 2
30 5 10 29 3eqtr2i 
 |-  ( 6 gcd 4 ) = 2