Metamath Proof Explorer


Theorem 8t2e16

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

Ref Expression
Assertion 8t2e16 ( 8 · 2 ) = 1 6

Proof

Step Hyp Ref Expression
1 8cn 8 ∈ ℂ
2 1 times2i ( 8 · 2 ) = ( 8 + 8 )
3 8p8e16 ( 8 + 8 ) = 1 6
4 2 3 eqtri ( 8 · 2 ) = 1 6