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 · ; ; 7 1 1 ) = ; ; ; ; ; 1 6 7 0 8 5

Proof

Step	Hyp	Ref	Expression
1		2nn0	⊢ 2 ∈ ℕ0
2		3nn0	⊢ 3 ∈ ℕ0
3	1 2	deccl	⊢ ; 2 3 ∈ ℕ0
4		5nn0	⊢ 5 ∈ ℕ0
5	3 4	deccl	⊢ ; ; 2 3 5 ∈ ℕ0
6		7nn0	⊢ 7 ∈ ℕ0
7		1nn0	⊢ 1 ∈ ℕ0
8	6 7	deccl	⊢ ; 7 1 ∈ ℕ0
9		eqid	⊢ ; ; 7 1 1 = ; ; 7 1 1
10		eqid	⊢ ; 7 1 = ; 7 1
11		eqid	⊢ ; 2 3 = ; 2 3
12		8nn0	⊢ 8 ∈ ℕ0
13		eqid	⊢ ; ; 2 3 5 = ; ; 2 3 5
14	3	nn0cni	⊢ ; 2 3 ∈ ℂ
15		2cn	⊢ 2 ∈ ℂ
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 ∈ ℕ0
20		4nn0	⊢ 4 ∈ ℕ0
21		6nn0	⊢ 6 ∈ ℕ0
22	7 21	deccl	⊢ ; 1 6 ∈ ℕ0
23	1 20	nn0addcli	⊢ ( 2 + 4 ) ∈ ℕ0
24		7cn	⊢ 7 ∈ ℂ
25		7t2e14	⊢ ( 7 · 2 ) = ; 1 4
26	24 15 25	mulcomli	⊢ ( 2 · 7 ) = ; 1 4
27		4p2e6	⊢ ( 4 + 2 ) = 6
28	7 20 1 26 27	decaddi	⊢ ( ( 2 · 7 ) + 2 ) = ; 1 6
29		3cn	⊢ 3 ∈ ℂ
30		7t3e21	⊢ ( 7 · 3 ) = ; 2 1
31	24 29 30	mulcomli	⊢ ( 3 · 7 ) = ; 2 1
32	6 1 2 11 7 1 28 31	decmul1c	⊢ ( ; 2 3 · 7 ) = ; ; 1 6 1
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	⊢ ( ( ; 2 3 · 7 ) + ( 2 + 4 ) ) = ; ; 1 6 7
42		5cn	⊢ 5 ∈ ℂ
43		7t5e35	⊢ ( 7 · 5 ) = ; 3 5
44	24 42 43	mulcomli	⊢ ( 5 · 7 ) = ; 3 5
45		3p1e4	⊢ ( 3 + 1 ) = 4
46		5p5e10	⊢ ( 5 + 5 ) = ; 1 0
47	2 4 4 44 45 46	decaddci2	⊢ ( ( 5 · 7 ) + 5 ) = ; 4 0
48	3 4 1 4 13 18 6 19 20 41 47	decmac	⊢ ( ( ; ; 2 3 5 · 7 ) + ( 2 + ; 2 3 ) ) = ; ; ; 1 6 7 0
49	5	nn0cni	⊢ ; ; 2 3 5 ∈ ℂ
50	49	mulid1i	⊢ ( ; ; 2 3 5 · 1 ) = ; ; 2 3 5
51		5p3e8	⊢ ( 5 + 3 ) = 8
52	3 4 2 50 51	decaddi	⊢ ( ( ; ; 2 3 5 · 1 ) + 3 ) = ; ; 2 3 8
53	6 7 1 2 10 11 5 12 3 48 52	decma2c	⊢ ( ( ; ; 2 3 5 · ; 7 1 ) + ; 2 3 ) = ; ; ; ; 1 6 7 0 8
54	5 8 7 9 4 3 53 50	decmul2c	⊢ ( ; ; 2 3 5 · ; ; 7 1 1 ) = ; ; ; ; ; 1 6 7 0 8 5