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 ) ∈ ℙ

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 ∈ ℂ
5		ax-1cn	⊢ 1 ∈ ℂ
6		7cn	⊢ 7 ∈ ℂ
7	4 5 6	subadd2i	⊢ ( ( 8 − 1 ) = 7 ↔ ( 7 + 1 ) = 8 )
8	3 7	mpbir	⊢ ( 8 − 1 ) = 7
9	2 8	eqtri	⊢ ( ( 2 ↑ 3 ) − 1 ) = 7
10		7prm	⊢ 7 ∈ ℙ
11	9 10	eqeltri	⊢ ( ( 2 ↑ 3 ) − 1 ) ∈ ℙ