Theorem ex-decpmul

Description: Example usage of decpmul . This proof is significantly longer than 235t711 . There is more unnecessary carrying compared to 235t711 . Although saving 5 visual steps, using mulcomli early on increases the compressed proof length. (Contributed by Steven Nguyen, 10-Dec-2022) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	ex-decpmul	$$⊢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		7nn0	$$⊢7\in {\mathbb{N}}_0$$
6		1nn0	$$⊢1\in {\mathbb{N}}_0$$
7	5 6	deccl	$$⊢71\in {\mathbb{N}}_0$$
8		eqid	$$⊢71=71$$
9		6nn0	$$⊢6\in {\mathbb{N}}_0$$
10	6 9	deccl	$$⊢16\in {\mathbb{N}}_0$$
11		eqid	$$⊢23=23$$
12		4nn0	$$⊢4\in {\mathbb{N}}_0$$
13		7cn	$$⊢7\in ℂ$$
14		2cn	$$⊢2\in ℂ$$
15		7t2e14	$$⊢7\cdot 2=14$$
16	13 14 15	mulcomli	$$⊢2\cdot 7=14$$
17		4p2e6	$$⊢4+2=6$$
18	6 12 1 16 17	decaddi	$$⊢2\cdot 7+2=16$$
19		3cn	$$⊢3\in ℂ$$
20		7t3e21	$$⊢7\cdot 3=21$$
21	13 19 20	mulcomli	$$⊢3\cdot 7=21$$
22	5 1 2 11 6 1 18 21	decmul1c	$$⊢23\cdot 7=161$$
23		1p2e3	$$⊢1+2=3$$
24	10 6 1 22 23	decaddi	$$⊢23\cdot 7+2=163$$
25	3	nn0cni	$$⊢23\in ℂ$$
26	25	mulid1i	$$⊢23\cdot 1=23$$
27	3 5 6 8 2 1 24 26	decmul2c	$$⊢23\cdot 71=1633$$
28	2 4	deccl	$$⊢35\in {\mathbb{N}}_0$$
29	7	nn0cni	$$⊢71\in ℂ$$
30		5cn	$$⊢5\in ℂ$$
31		7t5e35	$$⊢7\cdot 5=35$$
32	30	mulid2i	$$⊢1\cdot 5=5$$
33	4 5 6 8 31 32	decmul1	$$⊢71\cdot 5=355$$
34	29 30 33	mulcomli	$$⊢5\cdot 71=355$$
35	28	nn0cni	$$⊢35\in ℂ$$
36		eqid	$$⊢35=35$$
37		5p2e7	$$⊢5+2=7$$
38	2 4 1 36 37	decaddi	$$⊢35+2=37$$
39	35 14 38	addcomli	$$⊢2+35=37$$
40		5p3e8	$$⊢5+3=8$$
41	30 19 40	addcomli	$$⊢3+5=8$$
42	1 2 28 4 26 34 39 41	decadd	$$⊢23\cdot 1+5\cdot 71=378$$
43	30	mulid1i	$$⊢5\cdot 1=5$$
44	4	dec0h	$$⊢5=05$$
45	43 44	eqtri	$$⊢5\cdot 1=05$$
46	10 2	deccl	$$⊢163\in {\mathbb{N}}_0$$
47	46 2	deccl	$$⊢1633\in {\mathbb{N}}_0$$
48		0nn0	$$⊢0\in {\mathbb{N}}_0$$
49	2 5	deccl	$$⊢37\in {\mathbb{N}}_0$$
50		8nn0	$$⊢8\in {\mathbb{N}}_0$$
51		eqid	$$⊢16330=16330$$
52		eqid	$$⊢378=378$$
53		eqid	$$⊢1633=1633$$
54		eqid	$$⊢37=37$$
55		eqid	$$⊢163=163$$
56		3p3e6	$$⊢3+3=6$$
57	10 2 2 55 56	decaddi	$$⊢163+3=166$$
58		6p1e7	$$⊢6+1=7$$
59	10 9 6 57 58	decaddi	$$⊢163+3+1=167$$
60		7p3e10	$$⊢7+3=10$$
61	13 19 60	addcomli	$$⊢3+7=10$$
62	46 2 2 5 53 54 59 61	decaddc2	$$⊢1633+37=1670$$
63		8cn	$$⊢8\in ℂ$$
64	63	addid2i	$$⊢0+8=8$$
65	47 48 49 50 51 52 62 64	decadd	$$⊢16330+378=16708$$
66	3 4 7 6 27 42 45 65 48 4	decpmul	$$⊢235\cdot 711=167085$$