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 = 32
5 3p1e4 3 + 1 = 4
6 2m1e1 2 1 = 1
7 1 2 3 4 5 6 decsubi 2 5 1 = 31
8 31prm 31
9 7 8 eqeltri 2 5 1