Metamath Proof Explorer


Theorem m5prm

Description: The fifth Mersenne number M_5 = 31 is a prime number. (Contributed by AV, 17-Aug-2021)

Ref Expression
Assertion m5prm ( ( 2 ↑ 5 ) − 1 ) ∈ ℙ

Proof

Step Hyp Ref Expression
1 3nn0 3 ∈ ℕ0
2 2nn0 2 ∈ ℕ0
3 1nn0 1 ∈ ℕ0
4 2exp5 ( 2 ↑ 5 ) = 3 2
5 3p1e4 ( 3 + 1 ) = 4
6 2m1e1 ( 2 − 1 ) = 1
7 1 2 3 4 5 6 decsubi ( ( 2 ↑ 5 ) − 1 ) = 3 1
8 31prm 3 1 ∈ ℙ
9 7 8 eqeltri ( ( 2 ↑ 5 ) − 1 ) ∈ ℙ