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\cdot 711=167085$$

Proof

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