Theorem 11t31e341

Description: 341 is the product of 11 and 31. (Contributed by AV, 3-Jun-2023)

	Ref	Expression
Assertion	11t31e341	$$⊢11\cdot 31=341$$

Proof

Step	Hyp	Ref	Expression
1		3nn0	$$⊢3\in {\mathbb{N}}_0$$
2		1nn0	$$⊢1\in {\mathbb{N}}_0$$
3	1 2	deccl	$$⊢31\in {\mathbb{N}}_0$$
4		eqid	$$⊢11=11$$
5	3	nn0cni	$$⊢31\in ℂ$$
6	5	mullidi	$$⊢1\cdot 31=31$$
7		3cn	$$⊢3\in ℂ$$
8		ax-1cn	$$⊢1\in ℂ$$
9		3p1e4	$$⊢3+1=4$$
10	7 8 9	addcomli	$$⊢1+3=4$$
11	1 2 1 6 10	decaddi	$$⊢1\cdot 31+3=34$$
12	3 2 2 4 2 1 11 6	decmul1c	$$⊢11\cdot 31=341$$