Theorem 7t4e28

Description: 7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015)

	Ref	Expression
Assertion	7t4e28	⊢ ( 7 · 4 ) = ; 2 8

Proof

Step	Hyp	Ref	Expression
1		7nn0	⊢ 7 ∈ ℕ0
2		3nn0	⊢ 3 ∈ ℕ0
3		df-4	⊢ 4 = ( 3 + 1 )
4		7t3e21	⊢ ( 7 · 3 ) = ; 2 1
5		2nn0	⊢ 2 ∈ ℕ0
6		1nn0	⊢ 1 ∈ ℕ0
7		eqid	⊢ ; 2 1 = ; 2 1
8		7cn	⊢ 7 ∈ ℂ
9		ax-1cn	⊢ 1 ∈ ℂ
10		7p1e8	⊢ ( 7 + 1 ) = 8
11	8 9 10	addcomli	⊢ ( 1 + 7 ) = 8
12	5 6 1 7 11	decaddi	⊢ ( ; 2 1 + 7 ) = ; 2 8
13	1 2 3 4 12	4t3lem	⊢ ( 7 · 4 ) = ; 2 8