Metamath Proof Explorer

Theorem 9t6e54

Description: 9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015)

Ref Expression
Assertion 9t6e54 ( 9 · 6 ) = 5 4

Proof

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