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