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 ) e. Prime

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 e. Prime
6 4 5 eqeltri 
 |-  ( ( 2 ^ 2 ) - 1 ) e. Prime