Metamath Proof Explorer

Theorem fmtno5faclem2

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

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

Proof

Step Hyp Ref Expression
1 6nn0 
 |-  6 e. NN0
2 7nn0 
 |-  7 e. NN0
3 1 2 deccl 
 |-  ; 6 7 e. NN0
4 0nn0 
 |-  0 e. NN0
5 3 4 deccl 
 |-  ; ; 6 7 0 e. NN0
6 5 4 deccl 
 |-  ; ; ; 6 7 0 0 e. NN0
7 4nn0 
 |-  4 e. NN0
8 6 7 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 2nn0 
 |-  2 e. NN0
13 7 4 deccl 
 |-  ; 4 0 e. NN0
14 13 12 deccl 
 |-  ; ; 4 0 2 e. NN0
15 14 4 deccl 
 |-  ; ; ; 4 0 2 0 e. NN0
16 15 12 deccl 
 |-  ; ; ; ; 4 0 2 0 2 e. NN0
17 16 7 deccl 
 |-  ; ; ; ; ; 4 0 2 0 2 4 e. NN0
18 eqid 
 |-  ; ; ; ; ; 6 7 0 0 4 1 = ; ; ; ; ; 6 7 0 0 4 1
19 eqid 
 |-  ; ; ; ; 6 7 0 0 4 = ; ; ; ; 6 7 0 0 4
20 eqid 
 |-  ; ; ; 6 7 0 0 = ; ; ; 6 7 0 0
21 eqid 
 |-  ; ; 6 7 0 = ; ; 6 7 0
22 eqid 
 |-  ; 6 7 = ; 6 7
23 3nn0 
 |-  3 e. NN0
24 6t6e36 
 |-  ( 6 x. 6 ) = ; 3 6
25 3p1e4 
 |-  ( 3 + 1 ) = 4
26 6p4e10 
 |-  ( 6 + 4 ) = ; 1 0
27 23 1 7 24 25 26 decaddci2 
 |-  ( ( 6 x. 6 ) + 4 ) = ; 4 0
28 7t6e42 
 |-  ( 7 x. 6 ) = ; 4 2
29 1 1 2 22 12 7 27 28 decmul1c 
 |-  ( ; 6 7 x. 6 ) = ; ; 4 0 2
30 6cn 
 |-  6 e. CC
31 30 mul02i 
 |-  ( 0 x. 6 ) = 0
32 1 3 4 21 29 31 decmul1 
 |-  ( ; ; 6 7 0 x. 6 ) = ; ; ; 4 0 2 0
33 1 5 4 20 32 31 decmul1 
 |-  ( ; ; ; 6 7 0 0 x. 6 ) = ; ; ; ; 4 0 2 0 0
34 2cn 
 |-  2 e. CC
35 34 addid2i 
 |-  ( 0 + 2 ) = 2
36 15 4 12 33 35 decaddi 
 |-  ( ( ; ; ; 6 7 0 0 x. 6 ) + 2 ) = ; ; ; ; 4 0 2 0 2
37 4cn 
 |-  4 e. CC
38 6t4e24 
 |-  ( 6 x. 4 ) = ; 2 4
39 30 37 38 mulcomli 
 |-  ( 4 x. 6 ) = ; 2 4
40 1 6 7 19 7 12 36 39 decmul1c 
 |-  ( ; ; ; ; 6 7 0 0 4 x. 6 ) = ; ; ; ; ; 4 0 2 0 2 4
41 30 mulid2i 
 |-  ( 1 x. 6 ) = 6
42 1 8 9 18 40 41 decmul1 
 |-  ( ; ; ; ; ; 6 7 0 0 4 1 x. 6 ) = ; ; ; ; ; ; 4 0 2 0 2 4 6
43 eqid 
 |-  ; ; ; ; ; 4 0 2 0 2 4 = ; ; ; ; ; 4 0 2 0 2 4
44 4p1e5 
 |-  ( 4 + 1 ) = 5
45 16 7 9 43 44 decaddi 
 |-  ( ; ; ; ; ; 4 0 2 0 2 4 + 1 ) = ; ; ; ; ; 4 0 2 0 2 5
46 17 1 7 42 45 26 decaddci2 
 |-  ( ( ; ; ; ; ; 6 7 0 0 4 1 x. 6 ) + 4 ) = ; ; ; ; ; ; 4 0 2 0 2 5 0
47 1 10 2 11 12 7 46 28 decmul1c 
 |-  ( ; ; ; ; ; ; 6 7 0 0 4 1 7 x. 6 ) = ; ; ; ; ; ; ; 4 0 2 0 2 5 0 2