Metamath Proof Explorer


Theorem 2exp4

Description: Two to the fourth power is 16. (Contributed by Mario Carneiro, 20-Apr-2015)

Ref Expression
Assertion 2exp4 ⊢ 2 4 = 16

Proof

Step Hyp Ref Expression
1 2nn0 ⊢ 2 ∈ ℕ 0
2 2t2e4 ⊢ 2 ⋅ 2 = 4
3 sq2 ⊢ 2 2 = 4
4 4t4e16 ⊢ 4 ⋅ 4 = 16
5 1 1 2 3 4 numexp2x ⊢ 2 4 = 16