Metamath Proof Explorer


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