Theorem 11t31e341

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

	Ref	Expression
Assertion	11t31e341	⊢ ( ; 1 1 · ; 3 1 ) = ; ; 3 4 1

Proof

Step	Hyp	Ref	Expression
1		3nn0	⊢ 3 ∈ ℕ0
2		1nn0	⊢ 1 ∈ ℕ0
3	1 2	deccl	⊢ ; 3 1 ∈ ℕ0
4		eqid	⊢ ; 1 1 = ; 1 1
5	3	nn0cni	⊢ ; 3 1 ∈ ℂ
6	5	mulid2i	⊢ ( 1 · ; 3 1 ) = ; 3 1
7		3cn	⊢ 3 ∈ ℂ
8		ax-1cn	⊢ 1 ∈ ℂ
9		3p1e4	⊢ ( 3 + 1 ) = 4
10	7 8 9	addcomli	⊢ ( 1 + 3 ) = 4
11	1 2 1 6 10	decaddi	⊢ ( ( 1 · ; 3 1 ) + 3 ) = ; 3 4
12	3 2 2 4 2 1 11 6	decmul1c	⊢ ( ; 1 1 · ; 3 1 ) = ; ; 3 4 1