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 |