Description: The gcd of 12 and 5 is 1. (Contributed by metakunt, 25-Apr-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | 12gcd5e1 | |- ( ; 1 2 gcd 5 ) = 1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2lt5 | |- 2 < 5 |
|
2 | 1 | olci | |- ( 5 < 2 \/ 2 < 5 ) |
3 | 5re | |- 5 e. RR |
|
4 | 2re | |- 2 e. RR |
|
5 | lttri2 | |- ( ( 5 e. RR /\ 2 e. RR ) -> ( 5 =/= 2 <-> ( 5 < 2 \/ 2 < 5 ) ) ) |
|
6 | 3 4 5 | mp2an | |- ( 5 =/= 2 <-> ( 5 < 2 \/ 2 < 5 ) ) |
7 | 2 6 | mpbir | |- 5 =/= 2 |
8 | 5prm | |- 5 e. Prime |
|
9 | 2prm | |- 2 e. Prime |
|
10 | prmrp | |- ( ( 5 e. Prime /\ 2 e. Prime ) -> ( ( 5 gcd 2 ) = 1 <-> 5 =/= 2 ) ) |
|
11 | 8 9 10 | mp2an | |- ( ( 5 gcd 2 ) = 1 <-> 5 =/= 2 ) |
12 | 7 11 | mpbir | |- ( 5 gcd 2 ) = 1 |
13 | 5nn | |- 5 e. NN |
|
14 | 2nn | |- 2 e. NN |
|
15 | 14 | nnzi | |- 2 e. ZZ |
16 | 13 14 15 | gcdaddmzz2nncomi | |- ( 5 gcd 2 ) = ( 5 gcd ( ( 2 x. 5 ) + 2 ) ) |
17 | 13 14 | mulcomnni | |- ( 5 x. 2 ) = ( 2 x. 5 ) |
18 | 5t2e10 | |- ( 5 x. 2 ) = ; 1 0 |
|
19 | 17 18 | eqtr3i | |- ( 2 x. 5 ) = ; 1 0 |
20 | 19 | oveq1i | |- ( ( 2 x. 5 ) + 2 ) = ( ; 1 0 + 2 ) |
21 | 1nn0 | |- 1 e. NN0 |
|
22 | 0nn0 | |- 0 e. NN0 |
|
23 | 14 | nnnn0i | |- 2 e. NN0 |
24 | eqid | |- ; 1 0 = ; 1 0 |
|
25 | 23 | dec0h | |- 2 = ; 0 2 |
26 | 1p0e1 | |- ( 1 + 0 ) = 1 |
|
27 | 2cn | |- 2 e. CC |
|
28 | 27 | addid2i | |- ( 0 + 2 ) = 2 |
29 | 21 22 22 23 24 25 26 28 | decadd | |- ( ; 1 0 + 2 ) = ; 1 2 |
30 | 20 29 | eqtri | |- ( ( 2 x. 5 ) + 2 ) = ; 1 2 |
31 | 30 | oveq2i | |- ( 5 gcd ( ( 2 x. 5 ) + 2 ) ) = ( 5 gcd ; 1 2 ) |
32 | 16 31 | eqtri | |- ( 5 gcd 2 ) = ( 5 gcd ; 1 2 ) |
33 | 12 32 | eqtr3i | |- 1 = ( 5 gcd ; 1 2 ) |
34 | 21 14 | decnncl | |- ; 1 2 e. NN |
35 | 13 34 | gcdcomnni | |- ( 5 gcd ; 1 2 ) = ( ; 1 2 gcd 5 ) |
36 | 33 35 | eqtr2i | |- ( ; 1 2 gcd 5 ) = 1 |