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