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