Metamath Proof Explorer


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 addid1i ( 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 )