Metamath Proof Explorer

Theorem 7t6e42

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

Ref Expression
Assertion 7t6e42 ( 7 · 6 ) = 4 2

Proof

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