Metamath Proof Explorer

Theorem 7t7e49

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

Ref Expression
Assertion 7t7e49 ( 7 · 7 ) = 4 9

Proof

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