Metamath Proof Explorer


Theorem 8t4e32

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

Ref Expression
Assertion 8t4e32 ( 8 · 4 ) = 3 2

Proof

Step Hyp Ref Expression
1 8nn0 8 ∈ ℕ0
2 3nn0 3 ∈ ℕ0
3 df-4 4 = ( 3 + 1 )
4 8t3e24 ( 8 · 3 ) = 2 4
5 2nn0 2 ∈ ℕ0
6 4nn0 4 ∈ ℕ0
7 eqid 2 4 = 2 4
8 2p1e3 ( 2 + 1 ) = 3
9 1 nn0cni 8 ∈ ℂ
10 6 nn0cni 4 ∈ ℂ
11 8p4e12 ( 8 + 4 ) = 1 2
12 9 10 11 addcomli ( 4 + 8 ) = 1 2
13 5 6 1 7 8 5 12 decaddci ( 2 4 + 8 ) = 3 2
14 1 2 3 4 13 4t3lem ( 8 · 4 ) = 3 2