Metamath Proof Explorer


Theorem 12gcd5e1

Description: The gcd of 12 and 5 is 1. (Contributed by metakunt, 25-Apr-2024)

Ref Expression
Assertion 12gcd5e1
|- ( ; 1 2 gcd 5 ) = 1

Proof

Step Hyp Ref Expression
1 2lt5
 |-  2 < 5
2 1 olci
 |-  ( 5 < 2 \/ 2 < 5 )
3 5re
 |-  5 e. RR
4 2re
 |-  2 e. RR
5 lttri2
 |-  ( ( 5 e. RR /\ 2 e. RR ) -> ( 5 =/= 2 <-> ( 5 < 2 \/ 2 < 5 ) ) )
6 3 4 5 mp2an
 |-  ( 5 =/= 2 <-> ( 5 < 2 \/ 2 < 5 ) )
7 2 6 mpbir
 |-  5 =/= 2
8 5prm
 |-  5 e. Prime
9 2prm
 |-  2 e. Prime
10 prmrp
 |-  ( ( 5 e. Prime /\ 2 e. Prime ) -> ( ( 5 gcd 2 ) = 1 <-> 5 =/= 2 ) )
11 8 9 10 mp2an
 |-  ( ( 5 gcd 2 ) = 1 <-> 5 =/= 2 )
12 7 11 mpbir
 |-  ( 5 gcd 2 ) = 1
13 5nn
 |-  5 e. NN
14 2nn
 |-  2 e. NN
15 14 nnzi
 |-  2 e. ZZ
16 13 14 15 gcdaddmzz2nncomi
 |-  ( 5 gcd 2 ) = ( 5 gcd ( ( 2 x. 5 ) + 2 ) )
17 13 14 mulcomnni
 |-  ( 5 x. 2 ) = ( 2 x. 5 )
18 5t2e10
 |-  ( 5 x. 2 ) = ; 1 0
19 17 18 eqtr3i
 |-  ( 2 x. 5 ) = ; 1 0
20 19 oveq1i
 |-  ( ( 2 x. 5 ) + 2 ) = ( ; 1 0 + 2 )
21 1nn0
 |-  1 e. NN0
22 0nn0
 |-  0 e. NN0
23 14 nnnn0i
 |-  2 e. NN0
24 eqid
 |-  ; 1 0 = ; 1 0
25 23 dec0h
 |-  2 = ; 0 2
26 1p0e1
 |-  ( 1 + 0 ) = 1
27 2cn
 |-  2 e. CC
28 27 addid2i
 |-  ( 0 + 2 ) = 2
29 21 22 22 23 24 25 26 28 decadd
 |-  ( ; 1 0 + 2 ) = ; 1 2
30 20 29 eqtri
 |-  ( ( 2 x. 5 ) + 2 ) = ; 1 2
31 30 oveq2i
 |-  ( 5 gcd ( ( 2 x. 5 ) + 2 ) ) = ( 5 gcd ; 1 2 )
32 16 31 eqtri
 |-  ( 5 gcd 2 ) = ( 5 gcd ; 1 2 )
33 12 32 eqtr3i
 |-  1 = ( 5 gcd ; 1 2 )
34 21 14 decnncl
 |-  ; 1 2 e. NN
35 13 34 gcdcomnni
 |-  ( 5 gcd ; 1 2 ) = ( ; 1 2 gcd 5 )
36 33 35 eqtr2i
 |-  ( ; 1 2 gcd 5 ) = 1