Metamath Proof Explorer

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