Metamath Proof Explorer

Theorem 420gcd8e4

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

Ref Expression
Assertion 420gcd8e4 
|- ( ; ; 4 2 0 gcd 8 ) = 4

Proof

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