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 ) = ; 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 ∈ ℙ
9	7 8	eqeltri	⊢ ( ( 2 ↑ 5 ) − 1 ) ∈ ℙ