Metamath Proof Explorer

Theorem 9t4e36

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

Ref Expression
Assertion 9t4e36 ( 9 · 4 ) = 3 6

Proof

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