Theorem m3prm

Description: The third Mersenne number M_3 = 7 is a prime number. (Contributed by AV, 16-Aug-2021)

	Ref	Expression
Assertion	m3prm	$$⊢2^3-1\in \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		cu2	$$⊢2^3=8$$
2	1	oveq1i	$$⊢2^3-1=8-1$$
3		7p1e8	$$⊢7+1=8$$
4		8cn	$$⊢8\in ℂ$$
5		ax-1cn	$$⊢1\in ℂ$$
6		7cn	$$⊢7\in ℂ$$
7	4 5 6	subadd2i	$$⊢8-1=7\leftrightarrow 7+1=8$$
8	3 7	mpbir	$$⊢8-1=7$$
9	2 8	eqtri	$$⊢2^3-1=7$$
10		7prm	$$⊢7\in \mathbb{P}$$
11	9 10	eqeltri	$$⊢2^3-1\in \mathbb{P}$$