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 e. NN
2 6nn
 |-  6 e. NN
3 2 decnncl2
 |-  ; 6 0 e. NN
4 1 3 gcdcomnni
 |-  ( 7 gcd ; 6 0 ) = ( ; 6 0 gcd 7 )
5 1nn0
 |-  1 e. NN0
6 1nn
 |-  1 e. NN
7 5 6 decnncl
 |-  ; 1 1 e. NN
8 1 nnzi
 |-  7 e. ZZ
9 1 7 8 gcdaddmzz2nni
 |-  ( 7 gcd ; 1 1 ) = ( 7 gcd ( ; 1 1 + ( 7 x. 7 ) ) )
10 7t7e49
 |-  ( 7 x. 7 ) = ; 4 9
11 10 oveq2i
 |-  ( ; 1 1 + ( 7 x. 7 ) ) = ( ; 1 1 + ; 4 9 )
12 4nn0
 |-  4 e. NN0
13 9nn0
 |-  9 e. NN0
14 eqid
 |-  ; 1 1 = ; 1 1
15 eqid
 |-  ; 4 9 = ; 4 9
16 4cn
 |-  4 e. CC
17 ax-1cn
 |-  1 e. CC
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 e. CC
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 x. 7 ) ) = ; 6 0
28 27 oveq2i
 |-  ( 7 gcd ( ; 1 1 + ( 7 x. 7 ) ) ) = ( 7 gcd ; 6 0 )
29 9 28 eqtri
 |-  ( 7 gcd ; 1 1 ) = ( 7 gcd ; 6 0 )
30 7re
 |-  7 e. RR
31 1 nnnn0i
 |-  7 e. NN0
32 31 dec0h
 |-  7 = ; 0 7
33 0nn0
 |-  0 e. NN0
34 7lt9
 |-  7 < 9
35 9re
 |-  9 e. RR
36 30 35 pm3.2i
 |-  ( 7 e. RR /\ 9 e. RR )
37 ltle
 |-  ( ( 7 e. RR /\ 9 e. RR ) -> ( 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 e. RR /\ 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 e. Prime
48 11prm
 |-  ; 1 1 e. Prime
49 prmrp
 |-  ( ( 7 e. Prime /\ ; 1 1 e. Prime ) -> ( ( 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