Theorem m2prm

Description: The second Mersenne number M_2 = 3 is a prime number. (Contributed by AV, 16-Aug-2021)

	Ref	Expression
Assertion	m2prm	⊢ ( ( 2 ↑ 2 ) − 1 ) ∈ ℙ

Proof

Step	Hyp	Ref	Expression
1		sq2	⊢ ( 2 ↑ 2 ) = 4
2	1	oveq1i	⊢ ( ( 2 ↑ 2 ) − 1 ) = ( 4 − 1 )
3		4m1e3	⊢ ( 4 − 1 ) = 3
4	2 3	eqtri	⊢ ( ( 2 ↑ 2 ) − 1 ) = 3
5		3prm	⊢ 3 ∈ ℙ
6	4 5	eqeltri	⊢ ( ( 2 ↑ 2 ) − 1 ) ∈ ℙ