Theorem m7prm

Description: The seventh Mersenne number M_7 = 127 is a prime number. (Contributed by AV, 18-Aug-2021)

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

Proof

Step	Hyp	Ref	Expression
1		1nn0	⊢ 1 ∈ ℕ0
2		2nn0	⊢ 2 ∈ ℕ0
3	1 2	deccl	⊢ ; 1 2 ∈ ℕ0
4		8nn0	⊢ 8 ∈ ℕ0
5		2exp7	⊢ ( 2 ↑ 7 ) = ; ; 1 2 8
6		2p1e3	⊢ ( 2 + 1 ) = 3
7		eqid	⊢ ; 1 2 = ; 1 2
8	1 2 6 7	decsuc	⊢ ( ; 1 2 + 1 ) = ; 1 3
9		7p1e8	⊢ ( 7 + 1 ) = 8
10		8cn	⊢ 8 ∈ ℂ
11		ax-1cn	⊢ 1 ∈ ℂ
12		7cn	⊢ 7 ∈ ℂ
13	10 11 12	subadd2i	⊢ ( ( 8 − 1 ) = 7 ↔ ( 7 + 1 ) = 8 )
14	9 13	mpbir	⊢ ( 8 − 1 ) = 7
15	3 4 1 5 8 14	decsubi	⊢ ( ( 2 ↑ 7 ) − 1 ) = ; ; 1 2 7
16		127prm	⊢ ; ; 1 2 7 ∈ ℙ
17	15 16	eqeltri	⊢ ( ( 2 ↑ 7 ) − 1 ) ∈ ℙ