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 · ; 2 3 )

Proof

Step	Hyp	Ref	Expression
1		2nn0	⊢ 2 ∈ ℕ0
2		0nn0	⊢ 0 ∈ ℕ0
3	1 2	deccl	⊢ ; 2 0 ∈ ℕ0
4		4nn0	⊢ 4 ∈ ℕ0
5	3 4	deccl	⊢ ; ; 2 0 4 ∈ ℕ0
6		8nn0	⊢ 8 ∈ ℕ0
7		1nn0	⊢ 1 ∈ ℕ0
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 ∈ ℕ0
15	1 14	deccl	⊢ ; 2 3 ∈ ℕ0
16		9nn0	⊢ 9 ∈ ℕ0
17		eqid	⊢ ; 8 9 = ; 8 9
18		7nn0	⊢ 7 ∈ ℕ0
19		eqid	⊢ ; 2 3 = ; 2 3
20		eqid	⊢ ; 2 0 = ; 2 0
21		8t2e16	⊢ ( 8 · 2 ) = ; 1 6
22		2p2e4	⊢ ( 2 + 2 ) = 4
23	21 22	oveq12i	⊢ ( ( 8 · 2 ) + ( 2 + 2 ) ) = ( ; 1 6 + 4 )
24		6nn0	⊢ 6 ∈ ℕ0
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 · 2 ) + ( 2 + 2 ) ) = ; 2 0
30		8t3e24	⊢ ( 8 · 3 ) = ; 2 4
31	30	oveq1i	⊢ ( ( 8 · 3 ) + 0 ) = ( ; 2 4 + 0 )
32	1 4	deccl	⊢ ; 2 4 ∈ ℕ0
33	32	nn0cni	⊢ ; 2 4 ∈ ℂ
34	33	addridi	⊢ ( ; 2 4 + 0 ) = ; 2 4
35	31 34	eqtri	⊢ ( ( 8 · 3 ) + 0 ) = ; 2 4
36	1 14 1 2 19 20 6 4 1 29 35	decma2c	⊢ ( ( 8 · ; 2 3 ) + ; 2 0 ) = ; ; 2 0 4
37		9t2e18	⊢ ( 9 · 2 ) = ; 1 8
38		8p2e10	⊢ ( 8 + 2 ) = ; 1 0
39	7 6 1 37 26 38	decaddci2	⊢ ( ( 9 · 2 ) + 2 ) = ; 2 0
40		9t3e27	⊢ ( 9 · 3 ) = ; 2 7
41	16 1 14 19 18 1 39 40	decmul2c	⊢ ( 9 · ; 2 3 ) = ; ; 2 0 7
42	15 6 16 17 18 3 36 41	decmul1c	⊢ ( ; 8 9 · ; 2 3 ) = ; ; ; 2 0 4 7
43	13 42	eqtr4i	⊢ ( ( 2 ↑ ; 1 1 ) − 1 ) = ( ; 8 9 · ; 2 3 )