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

Proof

Step Hyp Ref Expression
1 3nn0 
 |-  3 e. NN0
2 2nn0 
 |-  2 e. NN0
3 1nn0 
 |-  1 e. NN0
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 e. Prime
9 7 8 eqeltri 
 |-  ( ( 2 ^ 5 ) - 1 ) e. Prime