Theorem m11nprm

Description: The eleventh Mersenne number M_11 = 2047 is not a prime number. (Contributed by AV, 18-Aug-2021)

	Ref	Expression
Assertion	m11nprm	$$⊢2^{11}-1=89\cdot 23$$

Proof

Step	Hyp	Ref	Expression
1		2nn0	$$⊢2\in {\mathbb{N}}_0$$
2		0nn0	$$⊢0\in {\mathbb{N}}_0$$
3	1 2	deccl	$$⊢20\in {\mathbb{N}}_0$$
4		4nn0	$$⊢4\in {\mathbb{N}}_0$$
5	3 4	deccl	$$⊢204\in {\mathbb{N}}_0$$
6		8nn0	$$⊢8\in {\mathbb{N}}_0$$
7		1nn0	$$⊢1\in {\mathbb{N}}_0$$
8		2exp11	$$⊢2^{11}=2048$$
9		4p1e5	$$⊢4+1=5$$
10		eqid	$$⊢204=204$$
11	3 4 9 10	decsuc	$$⊢204+1=205$$
12		8m1e7	$$⊢8-1=7$$
13	5 6 7 8 11 12	decsubi	$$⊢2^{11}-1=2047$$
14		3nn0	$$⊢3\in {\mathbb{N}}_0$$
15	1 14	deccl	$$⊢23\in {\mathbb{N}}_0$$
16		9nn0	$$⊢9\in {\mathbb{N}}_0$$
17		eqid	$$⊢89=89$$
18		7nn0	$$⊢7\in {\mathbb{N}}_0$$
19		eqid	$$⊢23=23$$
20		eqid	$$⊢20=20$$
21		8t2e16	$$⊢8\cdot 2=16$$
22		2p2e4	$$⊢2+2=4$$
23	21 22	oveq12i	$$⊢8\cdot 2+2+2=16+4$$
24		6nn0	$$⊢6\in {\mathbb{N}}_0$$
25		eqid	$$⊢16=16$$
26		1p1e2	$$⊢1+1=2$$
27		6p4e10	$$⊢6+4=10$$
28	7 24 4 25 26 27	decaddci2	$$⊢16+4=20$$
29	23 28	eqtri	$$⊢8\cdot 2+2+2=20$$
30		8t3e24	$$⊢8\cdot 3=24$$
31	30	oveq1i	$$⊢8\cdot 3+0=24+0$$
32	1 4	deccl	$$⊢24\in {\mathbb{N}}_0$$
33	32	nn0cni	$$⊢24\in ℂ$$
34	33	addid1i	$$⊢24+0=24$$
35	31 34	eqtri	$$⊢8\cdot 3+0=24$$
36	1 14 1 2 19 20 6 4 1 29 35	decma2c	$$⊢8\cdot 23+20=204$$
37		9t2e18	$$⊢9\cdot 2=18$$
38		8p2e10	$$⊢8+2=10$$
39	7 6 1 37 26 38	decaddci2	$$⊢9\cdot 2+2=20$$
40		9t3e27	$$⊢9\cdot 3=27$$
41	16 1 14 19 18 1 39 40	decmul2c	$$⊢9\cdot 23=207$$
42	15 6 16 17 18 3 36 41	decmul1c	$$⊢89\cdot 23=2047$$
43	13 42	eqtr4i	$$⊢2^{11}-1=89\cdot 23$$