Metamath Proof Explorer


Theorem 6t5e30

Description: 6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015) (Revised by AV, 6-Sep-2021)

Ref Expression
Assertion 6t5e30 ( 6 · 5 ) = 3 0

Proof

Step Hyp Ref Expression
1 6nn0 6 ∈ ℕ0
2 4nn0 4 ∈ ℕ0
3 df-5 5 = ( 4 + 1 )
4 6t4e24 ( 6 · 4 ) = 2 4
5 2nn0 2 ∈ ℕ0
6 eqid 2 4 = 2 4
7 2p1e3 ( 2 + 1 ) = 3
8 6cn 6 ∈ ℂ
9 4cn 4 ∈ ℂ
10 6p4e10 ( 6 + 4 ) = 1 0
11 8 9 10 addcomli ( 4 + 6 ) = 1 0
12 5 2 1 6 7 11 decaddci2 ( 2 4 + 6 ) = 3 0
13 1 2 3 4 12 4t3lem ( 6 · 5 ) = 3 0