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