Description: The gcd of 420 and 8 is 4. (Contributed by metakunt, 25-Apr-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | 420gcd8e4 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 8nn | ||
2 | 4nn | ||
3 | 5nn0 | ||
4 | 2nn | ||
5 | 3 4 | decnncl | |
6 | 5 | nnzi | |
7 | 1 2 6 | gcdaddmzz2nncomi | |
8 | 4nn0 | ||
9 | 1nn0 | ||
10 | 8 9 | deccl | |
11 | 6nn0 | ||
12 | 0nn0 | ||
13 | eqid | ||
14 | 8 | dec0h | |
15 | 1p1e2 | ||
16 | 10 | nn0cni | |
17 | 16 | addid1i | |
18 | 8 9 15 17 | decsuc | |
19 | 6p4e10 | ||
20 | 10 11 12 8 13 14 18 19 | decaddc2 | |
21 | 8nn0 | ||
22 | 2nn0 | ||
23 | eqid | ||
24 | 0p1e1 | ||
25 | 8t5e40 | ||
26 | 8 12 24 25 | decsuc | |
27 | 8t2e16 | ||
28 | 21 3 22 23 11 9 26 27 | decmul2c | |
29 | 1 5 | mulcomnni | |
30 | 28 29 | eqtr3i | |
31 | 30 | oveq1i | |
32 | 20 31 | eqtr3i | |
33 | 32 | oveq2i | |
34 | 7 33 | eqtr4i | |
35 | 1 2 | gcdcomnni | |
36 | 4t2e8 | ||
37 | 36 | oveq2i | |
38 | 2 4 | gcdmultiplei | |
39 | 37 38 | eqtr3i | |
40 | 35 39 | eqtri | |
41 | 8 4 | decnncl | |
42 | 41 | decnncl2 | |
43 | 1 42 | gcdcomnni | |
44 | 34 40 43 | 3eqtr3ri |