Theorem 60gcd7e1

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

	Ref	Expression
Assertion	60gcd7e1	⊢ ( ; 6 0 gcd 7 ) = 1

Proof

Step	Hyp	Ref	Expression
1		7nn	⊢ 7 ∈ ℕ
2		6nn	⊢ 6 ∈ ℕ
3	2	decnncl2	⊢ ; 6 0 ∈ ℕ
4	1 3	gcdcomnni	⊢ ( 7 gcd ; 6 0 ) = ( ; 6 0 gcd 7 )
5		1nn0	⊢ 1 ∈ ℕ0
6		1nn	⊢ 1 ∈ ℕ
7	5 6	decnncl	⊢ ; 1 1 ∈ ℕ
8	1	nnzi	⊢ 7 ∈ ℤ
9	1 7 8	gcdaddmzz2nni	⊢ ( 7 gcd ; 1 1 ) = ( 7 gcd ( ; 1 1 + ( 7 · 7 ) ) )
10		7t7e49	⊢ ( 7 · 7 ) = ; 4 9
11	10	oveq2i	⊢ ( ; 1 1 + ( 7 · 7 ) ) = ( ; 1 1 + ; 4 9 )
12		4nn0	⊢ 4 ∈ ℕ0
13		9nn0	⊢ 9 ∈ ℕ0
14		eqid	⊢ ; 1 1 = ; 1 1
15		eqid	⊢ ; 4 9 = ; 4 9
16		4cn	⊢ 4 ∈ ℂ
17		ax-1cn	⊢ 1 ∈ ℂ
18		4p1e5	⊢ ( 4 + 1 ) = 5
19	16 17 18	addcomli	⊢ ( 1 + 4 ) = 5
20	19	oveq1i	⊢ ( ( 1 + 4 ) + 1 ) = ( 5 + 1 )
21		5p1e6	⊢ ( 5 + 1 ) = 6
22	20 21	eqtri	⊢ ( ( 1 + 4 ) + 1 ) = 6
23		9cn	⊢ 9 ∈ ℂ
24		9p1e10	⊢ ( 9 + 1 ) = ; 1 0
25	23 17 24	addcomli	⊢ ( 1 + 9 ) = ; 1 0
26	5 5 12 13 14 15 22 25	decaddc2	⊢ ( ; 1 1 + ; 4 9 ) = ; 6 0
27	11 26	eqtri	⊢ ( ; 1 1 + ( 7 · 7 ) ) = ; 6 0
28	27	oveq2i	⊢ ( 7 gcd ( ; 1 1 + ( 7 · 7 ) ) ) = ( 7 gcd ; 6 0 )
29	9 28	eqtri	⊢ ( 7 gcd ; 1 1 ) = ( 7 gcd ; 6 0 )
30		7re	⊢ 7 ∈ ℝ
31	1	nnnn0i	⊢ 7 ∈ ℕ0
32	31	dec0h	⊢ 7 = ; 0 7
33		0nn0	⊢ 0 ∈ ℕ0
34		7lt9	⊢ 7 < 9
35		9re	⊢ 9 ∈ ℝ
36	30 35	pm3.2i	⊢ ( 7 ∈ ℝ ∧ 9 ∈ ℝ )
37		ltle	⊢ ( ( 7 ∈ ℝ ∧ 9 ∈ ℝ ) → ( 7 < 9 → 7 ≤ 9 ) )
38	36 37	ax-mp	⊢ ( 7 < 9 → 7 ≤ 9 )
39	34 38	ax-mp	⊢ 7 ≤ 9
40		0lt1	⊢ 0 < 1
41	33 5 31 5 39 40	declth	⊢ ; 0 7 < ; 1 1
42	32 41	eqbrtri	⊢ 7 < ; 1 1
43		ltne	⊢ ( ( 7 ∈ ℝ ∧ 7 < ; 1 1 ) → ; 1 1 ≠ 7 )
44	30 42 43	mp2an	⊢ ; 1 1 ≠ 7
45		necom	⊢ ( 7 ≠ ; 1 1 ↔ ; 1 1 ≠ 7 )
46	44 45	mpbir	⊢ 7 ≠ ; 1 1
47		7prm	⊢ 7 ∈ ℙ
48		11prm	⊢ ; 1 1 ∈ ℙ
49		prmrp	⊢ ( ( 7 ∈ ℙ ∧ ; 1 1 ∈ ℙ ) → ( ( 7 gcd ; 1 1 ) = 1 ↔ 7 ≠ ; 1 1 ) )
50	47 48 49	mp2an	⊢ ( ( 7 gcd ; 1 1 ) = 1 ↔ 7 ≠ ; 1 1 )
51	46 50	mpbir	⊢ ( 7 gcd ; 1 1 ) = 1
52	29 51	eqtr3i	⊢ ( 7 gcd ; 6 0 ) = 1
53	4 52	eqtr3i	⊢ ( ; 6 0 gcd 7 ) = 1