Metamath Proof Explorer

Theorem m3prm

Description: The third Mersenne number M_3 = 7 is a prime number. (Contributed by AV, 16-Aug-2021)

Ref Expression
Assertion m3prm 
|- ( ( 2 ^ 3 ) - 1 ) e. Prime

Proof

Step Hyp Ref Expression
1 cu2 
 |-  ( 2 ^ 3 ) = 8
2 1 oveq1i 
 |-  ( ( 2 ^ 3 ) - 1 ) = ( 8 - 1 )
3 7p1e8 
 |-  ( 7 + 1 ) = 8
4 8cn 
 |-  8 e. CC
5 ax-1cn 
 |-  1 e. CC
6 7cn 
 |-  7 e. CC
7 4 5 6 subadd2i 
 |-  ( ( 8 - 1 ) = 7 <-> ( 7 + 1 ) = 8 )
8 3 7 mpbir 
 |-  ( 8 - 1 ) = 7
9 2 8 eqtri 
 |-  ( ( 2 ^ 3 ) - 1 ) = 7
10 7prm 
 |-  7 e. Prime
11 9 10 eqeltri 
 |-  ( ( 2 ^ 3 ) - 1 ) e. Prime