Metamath Proof Explorer

Theorem fmtno5faclem1

Description: Lemma 1 for fmtno5fac . (Contributed by AV, 22-Jul-2021)

Ref Expression
Assertion fmtno5faclem1 
|- ( ; ; ; ; ; ; 6 7 0 0 4 1 7 x. 4 ) = ; ; ; ; ; ; ; 2 6 8 0 1 6 6 8

Proof

Step Hyp Ref Expression
1 4nn0 
 |-  4 e. NN0
2 6nn0 
 |-  6 e. NN0
3 7nn0 
 |-  7 e. NN0
4 2 3 deccl 
 |-  ; 6 7 e. NN0
5 0nn0 
 |-  0 e. NN0
6 4 5 deccl 
 |-  ; ; 6 7 0 e. NN0
7 6 5 deccl 
 |-  ; ; ; 6 7 0 0 e. NN0
8 7 1 deccl 
 |-  ; ; ; ; 6 7 0 0 4 e. NN0
9 1nn0 
 |-  1 e. NN0
10 8 9 deccl 
 |-  ; ; ; ; ; 6 7 0 0 4 1 e. NN0
11 eqid 
 |-  ; ; ; ; ; ; 6 7 0 0 4 1 7 = ; ; ; ; ; ; 6 7 0 0 4 1 7
12 8nn0 
 |-  8 e. NN0
13 2nn0 
 |-  2 e. NN0
14 13 2 deccl 
 |-  ; 2 6 e. NN0
15 14 12 deccl 
 |-  ; ; 2 6 8 e. NN0
16 15 5 deccl 
 |-  ; ; ; 2 6 8 0 e. NN0
17 16 9 deccl 
 |-  ; ; ; ; 2 6 8 0 1 e. NN0
18 17 2 deccl 
 |-  ; ; ; ; ; 2 6 8 0 1 6 e. NN0
19 eqid 
 |-  ; ; ; ; ; 6 7 0 0 4 1 = ; ; ; ; ; 6 7 0 0 4 1
20 eqid 
 |-  ; ; ; ; 6 7 0 0 4 = ; ; ; ; 6 7 0 0 4
21 eqid 
 |-  ; ; ; 6 7 0 0 = ; ; ; 6 7 0 0
22 eqid 
 |-  ; ; 6 7 0 = ; ; 6 7 0
23 eqid 
 |-  ; 6 7 = ; 6 7
24 6t4e24 
 |-  ( 6 x. 4 ) = ; 2 4
25 4p2e6 
 |-  ( 4 + 2 ) = 6
26 13 1 13 24 25 decaddi 
 |-  ( ( 6 x. 4 ) + 2 ) = ; 2 6
27 7t4e28 
 |-  ( 7 x. 4 ) = ; 2 8
28 1 2 3 23 12 13 26 27 decmul1c 
 |-  ( ; 6 7 x. 4 ) = ; ; 2 6 8
29 4cn 
 |-  4 e. CC
30 29 mul02i 
 |-  ( 0 x. 4 ) = 0
31 1 4 5 22 28 30 decmul1 
 |-  ( ; ; 6 7 0 x. 4 ) = ; ; ; 2 6 8 0
32 1 6 5 21 31 30 decmul1 
 |-  ( ; ; ; 6 7 0 0 x. 4 ) = ; ; ; ; 2 6 8 0 0
33 0p1e1 
 |-  ( 0 + 1 ) = 1
34 16 5 9 32 33 decaddi 
 |-  ( ( ; ; ; 6 7 0 0 x. 4 ) + 1 ) = ; ; ; ; 2 6 8 0 1
35 4t4e16 
 |-  ( 4 x. 4 ) = ; 1 6
36 1 7 1 20 2 9 34 35 decmul1c 
 |-  ( ; ; ; ; 6 7 0 0 4 x. 4 ) = ; ; ; ; ; 2 6 8 0 1 6
37 29 mullidi 
 |-  ( 1 x. 4 ) = 4
38 1 8 9 19 36 37 decmul1 
 |-  ( ; ; ; ; ; 6 7 0 0 4 1 x. 4 ) = ; ; ; ; ; ; 2 6 8 0 1 6 4
39 18 1 13 38 25 decaddi 
 |-  ( ( ; ; ; ; ; 6 7 0 0 4 1 x. 4 ) + 2 ) = ; ; ; ; ; ; 2 6 8 0 1 6 6
40 1 10 3 11 12 13 39 27 decmul1c 
 |-  ( ; ; ; ; ; ; 6 7 0 0 4 1 7 x. 4 ) = ; ; ; ; ; ; ; 2 6 8 0 1 6 6 8