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	addlidi	⊢ ( 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