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 ∈ ℝ
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 ) = 1 0
19 17 18 eqtr3i ( 2 · 5 ) = 1 0
20 19 oveq1i ( ( 2 · 5 ) + 2 ) = ( 1 0 + 2 )
21 1nn0 1 ∈ ℕ0
22 0nn0 0 ∈ ℕ0
23 14 nnnn0i 2 ∈ ℕ0
24 eqid 1 0 = 1 0
25 23 dec0h 2 = 0 2
26 1p0e1 ( 1 + 0 ) = 1
27 2cn 2 ∈ ℂ
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 · 5 ) + 2 ) = 1 2
31 30 oveq2i ( 5 gcd ( ( 2 · 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 ∈ ℕ
35 13 34 gcdcomnni ( 5 gcd 1 2 ) = ( 1 2 gcd 5 )
36 33 35 eqtr2i ( 1 2 gcd 5 ) = 1