Metamath Proof Explorer


Theorem m2prm

Description: The second Mersenne number M_2 = 3 is a prime number. (Contributed by AV, 16-Aug-2021)

Ref Expression
Assertion m2prm ( ( 2 ↑ 2 ) − 1 ) ∈ ℙ

Proof

Step Hyp Ref Expression
1 sq2 ( 2 ↑ 2 ) = 4
2 1 oveq1i ( ( 2 ↑ 2 ) − 1 ) = ( 4 − 1 )
3 4m1e3 ( 4 − 1 ) = 3
4 2 3 eqtri ( ( 2 ↑ 2 ) − 1 ) = 3
5 3prm 3 ∈ ℙ
6 4 5 eqeltri ( ( 2 ↑ 2 ) − 1 ) ∈ ℙ