Description: 7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | 7t4e28 | ⊢ ( 7 · 4 ) = ; 2 8 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 7nn0 | ⊢ 7 ∈ ℕ0 | |
2 | 3nn0 | ⊢ 3 ∈ ℕ0 | |
3 | df-4 | ⊢ 4 = ( 3 + 1 ) | |
4 | 7t3e21 | ⊢ ( 7 · 3 ) = ; 2 1 | |
5 | 2nn0 | ⊢ 2 ∈ ℕ0 | |
6 | 1nn0 | ⊢ 1 ∈ ℕ0 | |
7 | eqid | ⊢ ; 2 1 = ; 2 1 | |
8 | 7cn | ⊢ 7 ∈ ℂ | |
9 | ax-1cn | ⊢ 1 ∈ ℂ | |
10 | 7p1e8 | ⊢ ( 7 + 1 ) = 8 | |
11 | 8 9 10 | addcomli | ⊢ ( 1 + 7 ) = 8 |
12 | 5 6 1 7 11 | decaddi | ⊢ ( ; 2 1 + 7 ) = ; 2 8 |
13 | 1 2 3 4 12 | 4t3lem | ⊢ ( 7 · 4 ) = ; 2 8 |