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

Proof

Step	Hyp	Ref	Expression
1		1nn0	$$⊢1\in {\mathbb{N}}_0$$
2		2nn0	$$⊢2\in {\mathbb{N}}_0$$
3	1 2	deccl	$$⊢12\in {\mathbb{N}}_0$$
4		8nn0	$$⊢8\in {\mathbb{N}}_0$$
5		2exp7	$$⊢2^7=128$$
6		2p1e3	$$⊢2+1=3$$
7		eqid	$$⊢12=12$$
8	1 2 6 7	decsuc	$$⊢12+1=13$$
9		7p1e8	$$⊢7+1=8$$
10		8cn	$$⊢8\in ℂ$$
11		ax-1cn	$$⊢1\in ℂ$$
12		7cn	$$⊢7\in ℂ$$
13	10 11 12	subadd2i	$$⊢8-1=7\leftrightarrow 7+1=8$$
14	9 13	mpbir	$$⊢8-1=7$$
15	3 4 1 5 8 14	decsubi	$$⊢2^7-1=127$$
16		127prm	$$⊢127\in \mathbb{P}$$
17	15 16	eqeltri	$$⊢2^7-1\in \mathbb{P}$$