Description: The gcd of 60 and 7 is 1. (Contributed by metakunt, 25-Apr-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | 60gcd7e1 | |- ( ; 6 0 gcd 7 ) = 1 |
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 |