Metamath Proof Explorer

Theorem 235t711

Description: Calculate a product by long multiplication as a base comparison with other multiplication algorithms.

Conveniently, 7 1 1 has two ones which greatly simplifies calculations like 2 3 5 x. 1 . There isn't a higher level mulcomli saving the lower level uses of mulcomli within 2 3 5 x. 7 since mulcom2 doesn't exist, but if commuted versions of theorems like 7t2e14 are added then this proof would benefit more than ex-decpmul .

For practicality, this proof doesn't have "e167085" at the end of its name like 2p2e4 or 8t7e56 . (Contributed by Steven Nguyen, 10-Dec-2022) (New usage is discouraged.)

Ref Expression
Assertion 235t711 
|- ( ; ; 2 3 5 x. ; ; 7 1 1 ) = ; ; ; ; ; 1 6 7 0 8 5

Proof

Step Hyp Ref Expression
1 2nn0 
 |-  2 e. NN0
2 3nn0 
 |-  3 e. NN0
3 1 2 deccl 
 |-  ; 2 3 e. NN0
4 5nn0 
 |-  5 e. NN0
5 3 4 deccl 
 |-  ; ; 2 3 5 e. NN0
6 7nn0 
 |-  7 e. NN0
7 1nn0 
 |-  1 e. NN0
8 6 7 deccl 
 |-  ; 7 1 e. NN0
9 eqid 
 |-  ; ; 7 1 1 = ; ; 7 1 1
10 eqid 
 |-  ; 7 1 = ; 7 1
11 eqid 
 |-  ; 2 3 = ; 2 3
12 8nn0 
 |-  8 e. NN0
13 eqid 
 |-  ; ; 2 3 5 = ; ; 2 3 5
14 3 nn0cni 
 |-  ; 2 3 e. CC
15 2cn 
 |-  2 e. CC
16 3p2e5 
 |-  ( 3 + 2 ) = 5
17 1 2 1 11 16 decaddi 
 |-  ( ; 2 3 + 2 ) = ; 2 5
18 14 15 17 addcomli 
 |-  ( 2 + ; 2 3 ) = ; 2 5
19 0nn0 
 |-  0 e. NN0
20 4nn0 
 |-  4 e. NN0
21 6nn0 
 |-  6 e. NN0
22 7 21 deccl 
 |-  ; 1 6 e. NN0
23 1 20 nn0addcli 
 |-  ( 2 + 4 ) e. NN0
24 7cn 
 |-  7 e. CC
25 7t2e14 
 |-  ( 7 x. 2 ) = ; 1 4
26 24 15 25 mulcomli 
 |-  ( 2 x. 7 ) = ; 1 4
27 4p2e6 
 |-  ( 4 + 2 ) = 6
28 7 20 1 26 27 decaddi 
 |-  ( ( 2 x. 7 ) + 2 ) = ; 1 6
29 3cn 
 |-  3 e. CC
30 7t3e21 
 |-  ( 7 x. 3 ) = ; 2 1
31 24 29 30 mulcomli 
 |-  ( 3 x. 7 ) = ; 2 1
32 6 1 2 11 7 1 28 31 decmul1c 
 |-  ( ; 2 3 x. 7 ) = ; ; 1 6 1
33 4cn 
 |-  4 e. CC
34 15 33 addcli 
 |-  ( 2 + 4 ) e. CC
35 ax-1cn 
 |-  1 e. CC
36 33 15 27 addcomli 
 |-  ( 2 + 4 ) = 6
37 36 oveq1i 
 |-  ( ( 2 + 4 ) + 1 ) = ( 6 + 1 )
38 6p1e7 
 |-  ( 6 + 1 ) = 7
39 37 38 eqtri 
 |-  ( ( 2 + 4 ) + 1 ) = 7
40 34 35 39 addcomli 
 |-  ( 1 + ( 2 + 4 ) ) = 7
41 22 7 23 32 40 decaddi 
 |-  ( ( ; 2 3 x. 7 ) + ( 2 + 4 ) ) = ; ; 1 6 7
42 5cn 
 |-  5 e. CC
43 7t5e35 
 |-  ( 7 x. 5 ) = ; 3 5
44 24 42 43 mulcomli 
 |-  ( 5 x. 7 ) = ; 3 5
45 3p1e4 
 |-  ( 3 + 1 ) = 4
46 5p5e10 
 |-  ( 5 + 5 ) = ; 1 0
47 2 4 4 44 45 46 decaddci2 
 |-  ( ( 5 x. 7 ) + 5 ) = ; 4 0
48 3 4 1 4 13 18 6 19 20 41 47 decmac 
 |-  ( ( ; ; 2 3 5 x. 7 ) + ( 2 + ; 2 3 ) ) = ; ; ; 1 6 7 0
49 5 nn0cni 
 |-  ; ; 2 3 5 e. CC
50 49 mulid1i 
 |-  ( ; ; 2 3 5 x. 1 ) = ; ; 2 3 5
51 5p3e8 
 |-  ( 5 + 3 ) = 8
52 3 4 2 50 51 decaddi 
 |-  ( ( ; ; 2 3 5 x. 1 ) + 3 ) = ; ; 2 3 8
53 6 7 1 2 10 11 5 12 3 48 52 decma2c 
 |-  ( ( ; ; 2 3 5 x. ; 7 1 ) + ; 2 3 ) = ; ; ; ; 1 6 7 0 8
54 5 8 7 9 4 3 53 50 decmul2c 
 |-  ( ; ; 2 3 5 x. ; ; 7 1 1 ) = ; ; ; ; ; 1 6 7 0 8 5