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