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

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\in \mathbb{P}$$
6	4 5	eqeltri	$$⊢2^2-1\in \mathbb{P}$$