Metamath Proof Explorer


Theorem 12gcd5e1

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

Ref Expression
Assertion 12gcd5e1 12 gcd 5 = 1

Proof

Step Hyp Ref Expression
1 2lt5 2 < 5
2 1 olci 5 < 2 2 < 5
3 5re 5
4 2re 2
5 lttri2 5 2 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
9 2prm 2
10 prmrp 5 2 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
14 2nn 2
15 14 nnzi 2
16 13 14 15 gcdaddmzz2nncomi 5 gcd 2 = 5 gcd 2 5 + 2
17 13 14 mulcomnni 5 2 = 2 5
18 5t2e10 5 2 = 10
19 17 18 eqtr3i 2 5 = 10
20 19 oveq1i 2 5 + 2 = 10 + 2
21 1nn0 1 0
22 0nn0 0 0
23 14 nnnn0i 2 0
24 eqid 10 = 10
25 23 dec0h 2 = 02
26 1p0e1 1 + 0 = 1
27 2cn 2
28 27 addid2i 0 + 2 = 2
29 21 22 22 23 24 25 26 28 decadd 10 + 2 = 12
30 20 29 eqtri 2 5 + 2 = 12
31 30 oveq2i 5 gcd 2 5 + 2 = 5 gcd 12
32 16 31 eqtri 5 gcd 2 = 5 gcd 12
33 12 32 eqtr3i 1 = 5 gcd 12
34 21 14 decnncl 12
35 13 34 gcdcomnni 5 gcd 12 = 12 gcd 5
36 33 35 eqtr2i 12 gcd 5 = 1