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 ) e. Prime

Proof

Step	Hyp	Ref	Expression
1		1nn0	|- 1 e. NN0
2		2nn0	|- 2 e. NN0
3	1 2	deccl	|- ; 1 2 e. NN0
4		8nn0	|- 8 e. NN0
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 e. CC
11		ax-1cn	|- 1 e. CC
12		7cn	|- 7 e. CC
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 e. Prime
17	15 16	eqeltri	|- ( ( 2 ^ 7 ) - 1 ) e. Prime