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 235 711 = 167085

Proof

Step Hyp Ref Expression
1 2nn0 2 0
2 3nn0 3 0
3 1 2 deccl 23 0
4 5nn0 5 0
5 3 4 deccl 235 0
6 7nn0 7 0
7 1nn0 1 0
8 6 7 deccl 71 0
9 eqid 711 = 711
10 eqid 71 = 71
11 eqid 23 = 23
12 8nn0 8 0
13 eqid 235 = 235
14 3 nn0cni 23
15 2cn 2
16 3p2e5 3 + 2 = 5
17 1 2 1 11 16 decaddi 23 + 2 = 25
18 14 15 17 addcomli 2 + 23 = 25
19 0nn0 0 0
20 4nn0 4 0
21 6nn0 6 0
22 7 21 deccl 16 0
23 1 20 nn0addcli 2 + 4 0
24 7cn 7
25 7t2e14 7 2 = 14
26 24 15 25 mulcomli 2 7 = 14
27 4p2e6 4 + 2 = 6
28 7 20 1 26 27 decaddi 2 7 + 2 = 16
29 3cn 3
30 7t3e21 7 3 = 21
31 24 29 30 mulcomli 3 7 = 21
32 6 1 2 11 7 1 28 31 decmul1c 23 7 = 161
33 4cn 4
34 15 33 addcli 2 + 4
35 ax-1cn 1
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 23 7 + 2 + 4 = 167
42 5cn 5
43 7t5e35 7 5 = 35
44 24 42 43 mulcomli 5 7 = 35
45 3p1e4 3 + 1 = 4
46 5p5e10 5 + 5 = 10
47 2 4 4 44 45 46 decaddci2 5 7 + 5 = 40
48 3 4 1 4 13 18 6 19 20 41 47 decmac 235 7 + 2 + 23 = 1670
49 5 nn0cni 235
50 49 mulid1i 235 1 = 235
51 5p3e8 5 + 3 = 8
52 3 4 2 50 51 decaddi 235 1 + 3 = 238
53 6 7 1 2 10 11 5 12 3 48 52 decma2c 235 71 + 23 = 16708
54 5 8 7 9 4 3 53 50 decmul2c 235 711 = 167085