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	$$⊢\left(5<2\vee 2<5\right)$$
3		5re	$$⊢5\in ℝ$$
4		2re	$$⊢2\in ℝ$$
5		lttri2	$$⊢\left(5\in ℝ\wedge 2\in ℝ\right)\to \left(5\ne 2\leftrightarrow \left(5<2\vee 2<5\right)\right)$$
6	3 4 5	mp2an	$$⊢5\ne 2\leftrightarrow \left(5<2\vee 2<5\right)$$
7	2 6	mpbir	$$⊢5\ne 2$$
8		5prm	$$⊢5\in \mathbb{P}$$
9		2prm	$$⊢2\in \mathbb{P}$$
10		prmrp	$$⊢\left(5\in \mathbb{P}\wedge 2\in \mathbb{P}\right)\to \left(5\gcd 2=1\leftrightarrow 5\ne 2\right)$$
11	8 9 10	mp2an	$$⊢5\gcd 2=1\leftrightarrow 5\ne 2$$
12	7 11	mpbir	$$⊢5\gcd 2=1$$
13		5nn	$$⊢5\in \mathbb{N}$$
14		2nn	$$⊢2\in \mathbb{N}$$
15	14	nnzi	$$⊢2\in \mathbb{Z}$$
16	13 14 15	gcdaddmzz2nncomi	$$⊢5\gcd 2=5\gcd \left(2\cdot 5+2\right)$$
17	13 14	mulcomnni	$$⊢5\cdot 2=2\cdot 5$$
18		5t2e10	$$⊢5\cdot 2=10$$
19	17 18	eqtr3i	$$⊢2\cdot 5=10$$
20	19	oveq1i	$$⊢2\cdot 5+2=10+2$$
21		1nn0	$$⊢1\in {\mathbb{N}}_0$$
22		0nn0	$$⊢0\in {\mathbb{N}}_0$$
23	14	nnnn0i	$$⊢2\in {\mathbb{N}}_0$$
24		eqid	$$⊢10=10$$
25	23	dec0h	$$⊢2=02$$
26		1p0e1	$$⊢1+0=1$$
27		2cn	$$⊢2\in ℂ$$
28	27	addid2i	$$⊢0+2=2$$
29	21 22 22 23 24 25 26 28	decadd	$$⊢10+2=12$$
30	20 29	eqtri	$$⊢2\cdot 5+2=12$$
31	30	oveq2i	$$⊢5\gcd \left(2\cdot 5+2\right)=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\in \mathbb{N}$$
35	13 34	gcdcomnni	$$⊢5\gcd 12=12\gcd 5$$
36	33 35	eqtr2i	$$⊢12\gcd 5=1$$