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 ^ ; 1 1 ) - 1 ) = ( ; 8 9 x. ; 2 3 )

Proof

Step	Hyp	Ref	Expression
1		2nn0	|- 2 e. NN0
2		0nn0	|- 0 e. NN0
3	1 2	deccl	|- ; 2 0 e. NN0
4		4nn0	|- 4 e. NN0
5	3 4	deccl	|- ; ; 2 0 4 e. NN0
6		8nn0	|- 8 e. NN0
7		1nn0	|- 1 e. NN0
8		2exp11	|- ( 2 ^ ; 1 1 ) = ; ; ; 2 0 4 8
9		4p1e5	|- ( 4 + 1 ) = 5
10		eqid	|- ; ; 2 0 4 = ; ; 2 0 4
11	3 4 9 10	decsuc	|- ( ; ; 2 0 4 + 1 ) = ; ; 2 0 5
12		8m1e7	|- ( 8 - 1 ) = 7
13	5 6 7 8 11 12	decsubi	|- ( ( 2 ^ ; 1 1 ) - 1 ) = ; ; ; 2 0 4 7
14		3nn0	|- 3 e. NN0
15	1 14	deccl	|- ; 2 3 e. NN0
16		9nn0	|- 9 e. NN0
17		eqid	|- ; 8 9 = ; 8 9
18		7nn0	|- 7 e. NN0
19		eqid	|- ; 2 3 = ; 2 3
20		eqid	|- ; 2 0 = ; 2 0
21		8t2e16	|- ( 8 x. 2 ) = ; 1 6
22		2p2e4	|- ( 2 + 2 ) = 4
23	21 22	oveq12i	|- ( ( 8 x. 2 ) + ( 2 + 2 ) ) = ( ; 1 6 + 4 )
24		6nn0	|- 6 e. NN0
25		eqid	|- ; 1 6 = ; 1 6
26		1p1e2	|- ( 1 + 1 ) = 2
27		6p4e10	|- ( 6 + 4 ) = ; 1 0
28	7 24 4 25 26 27	decaddci2	|- ( ; 1 6 + 4 ) = ; 2 0
29	23 28	eqtri	|- ( ( 8 x. 2 ) + ( 2 + 2 ) ) = ; 2 0
30		8t3e24	|- ( 8 x. 3 ) = ; 2 4
31	30	oveq1i	|- ( ( 8 x. 3 ) + 0 ) = ( ; 2 4 + 0 )
32	1 4	deccl	|- ; 2 4 e. NN0
33	32	nn0cni	|- ; 2 4 e. CC
34	33	addid1i	|- ( ; 2 4 + 0 ) = ; 2 4
35	31 34	eqtri	|- ( ( 8 x. 3 ) + 0 ) = ; 2 4
36	1 14 1 2 19 20 6 4 1 29 35	decma2c	|- ( ( 8 x. ; 2 3 ) + ; 2 0 ) = ; ; 2 0 4
37		9t2e18	|- ( 9 x. 2 ) = ; 1 8
38		8p2e10	|- ( 8 + 2 ) = ; 1 0
39	7 6 1 37 26 38	decaddci2	|- ( ( 9 x. 2 ) + 2 ) = ; 2 0
40		9t3e27	|- ( 9 x. 3 ) = ; 2 7
41	16 1 14 19 18 1 39 40	decmul2c	|- ( 9 x. ; 2 3 ) = ; ; 2 0 7
42	15 6 16 17 18 3 36 41	decmul1c	|- ( ; 8 9 x. ; 2 3 ) = ; ; ; 2 0 4 7
43	13 42	eqtr4i	|- ( ( 2 ^ ; 1 1 ) - 1 ) = ( ; 8 9 x. ; 2 3 )