Metamath Proof Explorer


Theorem 420gcd8e4

Description: The gcd of 420 and 8 is 4. (Contributed by metakunt, 25-Apr-2024)

Ref Expression
Assertion 420gcd8e4 420 gcd 8 = 4

Proof

Step Hyp Ref Expression
1 8nn 8
2 4nn 4
3 5nn0 5 0
4 2nn 2
5 3 4 decnncl 52
6 5 nnzi 52
7 1 2 6 gcdaddmzz2nncomi 8 gcd 4 = 8 gcd 52 8 + 4
8 4nn0 4 0
9 1nn0 1 0
10 8 9 deccl 41 0
11 6nn0 6 0
12 0nn0 0 0
13 eqid 416 = 416
14 8 dec0h 4 = 04
15 1p1e2 1 + 1 = 2
16 10 nn0cni 41
17 16 addid1i 41 + 0 = 41
18 8 9 15 17 decsuc 41 + 0 + 1 = 42
19 6p4e10 6 + 4 = 10
20 10 11 12 8 13 14 18 19 decaddc2 416 + 4 = 420
21 8nn0 8 0
22 2nn0 2 0
23 eqid 52 = 52
24 0p1e1 0 + 1 = 1
25 8t5e40 8 5 = 40
26 8 12 24 25 decsuc 8 5 + 1 = 41
27 8t2e16 8 2 = 16
28 21 3 22 23 11 9 26 27 decmul2c 8 52 = 416
29 1 5 mulcomnni 8 52 = 52 8
30 28 29 eqtr3i 416 = 52 8
31 30 oveq1i 416 + 4 = 52 8 + 4
32 20 31 eqtr3i 420 = 52 8 + 4
33 32 oveq2i 8 gcd 420 = 8 gcd 52 8 + 4
34 7 33 eqtr4i 8 gcd 4 = 8 gcd 420
35 1 2 gcdcomnni 8 gcd 4 = 4 gcd 8
36 4t2e8 4 2 = 8
37 36 oveq2i 4 gcd 4 2 = 4 gcd 8
38 2 4 gcdmultiplei 4 gcd 4 2 = 4
39 37 38 eqtr3i 4 gcd 8 = 4
40 35 39 eqtri 8 gcd 4 = 4
41 8 4 decnncl 42
42 41 decnncl2 420
43 1 42 gcdcomnni 8 gcd 420 = 420 gcd 8
44 34 40 43 3eqtr3ri 420 gcd 8 = 4