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\in \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		3nn0	$$⊢3\in {\mathbb{N}}_0$$
2		2nn0	$$⊢2\in {\mathbb{N}}_0$$
3		1nn0	$$⊢1\in {\mathbb{N}}_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\in \mathbb{P}$$
9	7 8	eqeltri	$$⊢2^5-1\in \mathbb{P}$$