Proof of Theorem lighneal
Step | Hyp | Ref
| Expression |
1 | | lighneallem1 45009 |
. . . . . . 7
⊢ ((𝑃 = 2 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((2↑𝑁) − 1) ≠ (𝑃↑𝑀)) |
2 | | eqneqall 2955 |
. . . . . . 7
⊢
(((2↑𝑁) −
1) = (𝑃↑𝑀) → (((2↑𝑁) − 1) ≠ (𝑃↑𝑀) → 𝑀 = 1)) |
3 | 1, 2 | syl5com 31 |
. . . . . 6
⊢ ((𝑃 = 2 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((2↑𝑁) − 1) = (𝑃↑𝑀) → 𝑀 = 1)) |
4 | 3 | 3exp 1117 |
. . . . 5
⊢ (𝑃 = 2 → (𝑀 ∈ ℕ → (𝑁 ∈ ℕ → (((2↑𝑁) − 1) = (𝑃↑𝑀) → 𝑀 = 1)))) |
5 | 4 | a1d 25 |
. . . 4
⊢ (𝑃 = 2 → (𝑃 ∈ ℙ → (𝑀 ∈ ℕ → (𝑁 ∈ ℕ → (((2↑𝑁) − 1) = (𝑃↑𝑀) → 𝑀 = 1))))) |
6 | | eldifsn 4725 |
. . . . . 6
⊢ (𝑃 ∈ (ℙ ∖ {2})
↔ (𝑃 ∈ ℙ
∧ 𝑃 ≠
2)) |
7 | | lighneallem2 45010 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 2 ∥ 𝑁 ∧
((2↑𝑁) − 1) =
(𝑃↑𝑀)) → 𝑀 = 1) |
8 | 7 | 3exp 1117 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (2 ∥ 𝑁 →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) → 𝑀 = 1))) |
9 | 8 | 3exp 1117 |
. . . . . . . . . 10
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑀 ∈ ℕ
→ (𝑁 ∈ ℕ
→ (2 ∥ 𝑁 →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) → 𝑀 = 1))))) |
10 | 9 | com3r 87 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑃 ∈ (ℙ ∖ {2})
→ (𝑀 ∈ ℕ
→ (2 ∥ 𝑁 →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) → 𝑀 = 1))))) |
11 | 10 | com24 95 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (2
∥ 𝑁 → (𝑀 ∈ ℕ → (𝑃 ∈ (ℙ ∖ {2})
→ (((2↑𝑁) −
1) = (𝑃↑𝑀) → 𝑀 = 1))))) |
12 | | lighneallem3 45011 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ (¬ 2 ∥ 𝑁
∧ 2 ∥ 𝑀) ∧
((2↑𝑁) − 1) =
(𝑃↑𝑀)) → 𝑀 = 1) |
13 | 12 | 3exp 1117 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ ((¬ 2 ∥ 𝑁
∧ 2 ∥ 𝑀) →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) → 𝑀 = 1))) |
14 | 13 | 3exp 1117 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑀 ∈ ℕ
→ (𝑁 ∈ ℕ
→ ((¬ 2 ∥ 𝑁
∧ 2 ∥ 𝑀) →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) → 𝑀 = 1))))) |
15 | 14 | com24 95 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((¬ 2 ∥ 𝑁
∧ 2 ∥ 𝑀) →
(𝑁 ∈ ℕ →
(𝑀 ∈ ℕ →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) → 𝑀 = 1))))) |
16 | 15 | com14 96 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → ((¬ 2
∥ 𝑁 ∧ 2 ∥
𝑀) → (𝑁 ∈ ℕ → (𝑃 ∈ (ℙ ∖ {2})
→ (((2↑𝑁) −
1) = (𝑃↑𝑀) → 𝑀 = 1))))) |
17 | 16 | expcomd 416 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (2
∥ 𝑀 → (¬ 2
∥ 𝑁 → (𝑁 ∈ ℕ → (𝑃 ∈ (ℙ ∖ {2})
→ (((2↑𝑁) −
1) = (𝑃↑𝑀) → 𝑀 = 1)))))) |
18 | | lighneallem4 45014 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ (¬ 2 ∥ 𝑁
∧ ¬ 2 ∥ 𝑀)
∧ ((2↑𝑁) −
1) = (𝑃↑𝑀)) → 𝑀 = 1) |
19 | 18 | 3exp 1117 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ ((¬ 2 ∥ 𝑁
∧ ¬ 2 ∥ 𝑀)
→ (((2↑𝑁) −
1) = (𝑃↑𝑀) → 𝑀 = 1))) |
20 | 19 | 3exp 1117 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑀 ∈ ℕ
→ (𝑁 ∈ ℕ
→ ((¬ 2 ∥ 𝑁
∧ ¬ 2 ∥ 𝑀)
→ (((2↑𝑁) −
1) = (𝑃↑𝑀) → 𝑀 = 1))))) |
21 | 20 | com24 95 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((¬ 2 ∥ 𝑁
∧ ¬ 2 ∥ 𝑀)
→ (𝑁 ∈ ℕ
→ (𝑀 ∈ ℕ
→ (((2↑𝑁) −
1) = (𝑃↑𝑀) → 𝑀 = 1))))) |
22 | 21 | com14 96 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → ((¬ 2
∥ 𝑁 ∧ ¬ 2
∥ 𝑀) → (𝑁 ∈ ℕ → (𝑃 ∈ (ℙ ∖ {2})
→ (((2↑𝑁) −
1) = (𝑃↑𝑀) → 𝑀 = 1))))) |
23 | 22 | expcomd 416 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (¬ 2
∥ 𝑀 → (¬ 2
∥ 𝑁 → (𝑁 ∈ ℕ → (𝑃 ∈ (ℙ ∖ {2})
→ (((2↑𝑁) −
1) = (𝑃↑𝑀) → 𝑀 = 1)))))) |
24 | 17, 23 | pm2.61d 179 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (¬ 2
∥ 𝑁 → (𝑁 ∈ ℕ → (𝑃 ∈ (ℙ ∖ {2})
→ (((2↑𝑁) −
1) = (𝑃↑𝑀) → 𝑀 = 1))))) |
25 | 24 | com13 88 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (¬ 2
∥ 𝑁 → (𝑀 ∈ ℕ → (𝑃 ∈ (ℙ ∖ {2})
→ (((2↑𝑁) −
1) = (𝑃↑𝑀) → 𝑀 = 1))))) |
26 | 11, 25 | pm2.61d 179 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑀 ∈ ℕ → (𝑃 ∈ (ℙ ∖ {2})
→ (((2↑𝑁) −
1) = (𝑃↑𝑀) → 𝑀 = 1)))) |
27 | 26 | com13 88 |
. . . . . 6
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑀 ∈ ℕ
→ (𝑁 ∈ ℕ
→ (((2↑𝑁) −
1) = (𝑃↑𝑀) → 𝑀 = 1)))) |
28 | 6, 27 | sylbir 234 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) → (𝑀 ∈ ℕ → (𝑁 ∈ ℕ →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) → 𝑀 = 1)))) |
29 | 28 | expcom 413 |
. . . 4
⊢ (𝑃 ≠ 2 → (𝑃 ∈ ℙ → (𝑀 ∈ ℕ → (𝑁 ∈ ℕ →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) → 𝑀 = 1))))) |
30 | 5, 29 | pm2.61ine 3029 |
. . 3
⊢ (𝑃 ∈ ℙ → (𝑀 ∈ ℕ → (𝑁 ∈ ℕ →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) → 𝑀 = 1)))) |
31 | 30 | 3imp1 1345 |
. 2
⊢ (((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧
((2↑𝑁) − 1) =
(𝑃↑𝑀)) → 𝑀 = 1) |
32 | | oveq2 7276 |
. . . . . 6
⊢ (𝑀 = 1 → (𝑃↑𝑀) = (𝑃↑1)) |
33 | 32 | eqeq2d 2750 |
. . . . 5
⊢ (𝑀 = 1 → (((2↑𝑁) − 1) = (𝑃↑𝑀) ↔ ((2↑𝑁) − 1) = (𝑃↑1))) |
34 | 33 | adantl 481 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑀 = 1) → (((2↑𝑁) − 1) = (𝑃↑𝑀) ↔ ((2↑𝑁) − 1) = (𝑃↑1))) |
35 | | prmnn 16360 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
36 | 35 | nncnd 11972 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℂ) |
37 | 36 | 3ad2ant1 1131 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑃 ∈
ℂ) |
38 | 37 | exp1d 13840 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑃↑1) = 𝑃) |
39 | 38 | eqeq2d 2750 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(((2↑𝑁) − 1) =
(𝑃↑1) ↔
((2↑𝑁) − 1) =
𝑃)) |
40 | | nnz 12325 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
41 | 40 | 3ad2ant3 1133 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℤ) |
42 | | simpl1 1189 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧
((2↑𝑁) − 1) =
𝑃) → 𝑃 ∈ ℙ) |
43 | | eleq1 2827 |
. . . . . . . . . 10
⊢
(((2↑𝑁) −
1) = 𝑃 →
(((2↑𝑁) − 1)
∈ ℙ ↔ 𝑃
∈ ℙ)) |
44 | 43 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧
((2↑𝑁) − 1) =
𝑃) → (((2↑𝑁) − 1) ∈ ℙ
↔ 𝑃 ∈
ℙ)) |
45 | 42, 44 | mpbird 256 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧
((2↑𝑁) − 1) =
𝑃) → ((2↑𝑁) − 1) ∈
ℙ) |
46 | | mersenne 26356 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧
((2↑𝑁) − 1)
∈ ℙ) → 𝑁
∈ ℙ) |
47 | 41, 45, 46 | syl2an2r 681 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧
((2↑𝑁) − 1) =
𝑃) → 𝑁 ∈ ℙ) |
48 | 47 | ex 412 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(((2↑𝑁) − 1) =
𝑃 → 𝑁 ∈ ℙ)) |
49 | 39, 48 | sylbid 239 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(((2↑𝑁) − 1) =
(𝑃↑1) → 𝑁 ∈
ℙ)) |
50 | 49 | adantr 480 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑀 = 1) → (((2↑𝑁) − 1) = (𝑃↑1) → 𝑁 ∈
ℙ)) |
51 | 34, 50 | sylbid 239 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑀 = 1) → (((2↑𝑁) − 1) = (𝑃↑𝑀) → 𝑁 ∈ ℙ)) |
52 | 51 | impancom 451 |
. 2
⊢ (((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧
((2↑𝑁) − 1) =
(𝑃↑𝑀)) → (𝑀 = 1 → 𝑁 ∈ ℙ)) |
53 | 31, 52 | jcai 516 |
1
⊢ (((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧
((2↑𝑁) − 1) =
(𝑃↑𝑀)) → (𝑀 = 1 ∧ 𝑁 ∈ ℙ)) |