Step | Hyp | Ref
| Expression |
1 | | oveq2 7279 |
. . . . . . . . . . . . 13
⊢ (𝑁 = 1 → (2↑𝑁) = (2↑1)) |
2 | | 2cn 12048 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
3 | | exp1 13786 |
. . . . . . . . . . . . . 14
⊢ (2 ∈
ℂ → (2↑1) = 2) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(2↑1) = 2 |
5 | 1, 4 | eqtrdi 2796 |
. . . . . . . . . . . 12
⊢ (𝑁 = 1 → (2↑𝑁) = 2) |
6 | 5 | oveq1d 7286 |
. . . . . . . . . . 11
⊢ (𝑁 = 1 → ((2↑𝑁) − 1) = (2 −
1)) |
7 | | 2m1e1 12099 |
. . . . . . . . . . 11
⊢ (2
− 1) = 1 |
8 | 6, 7 | eqtrdi 2796 |
. . . . . . . . . 10
⊢ (𝑁 = 1 → ((2↑𝑁) − 1) =
1) |
9 | 8 | adantl 482 |
. . . . . . . . 9
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
∧ 𝑁 = 1) →
((2↑𝑁) − 1) =
1) |
10 | 9 | eqeq1d 2742 |
. . . . . . . 8
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
∧ 𝑁 = 1) →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) ↔ 1 = (𝑃↑𝑀))) |
11 | | eldifi 4066 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
12 | | prmnn 16377 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
13 | | nnnn0 12240 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℕ0) |
14 | 11, 12, 13 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℕ0) |
15 | 14 | nn0zd 12423 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℤ) |
16 | | iddvdsexp 15987 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑃 ∥ (𝑃↑𝑀)) |
17 | 15, 16 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
→ 𝑃 ∥ (𝑃↑𝑀)) |
18 | | breq2 5083 |
. . . . . . . . . . . . 13
⊢ (1 =
(𝑃↑𝑀) → (𝑃 ∥ 1 ↔ 𝑃 ∥ (𝑃↑𝑀))) |
19 | 18 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
∧ 1 = (𝑃↑𝑀)) → (𝑃 ∥ 1 ↔ 𝑃 ∥ (𝑃↑𝑀))) |
20 | | dvds1 16026 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℕ0
→ (𝑃 ∥ 1 ↔
𝑃 = 1)) |
21 | 14, 20 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∥ 1 ↔
𝑃 = 1)) |
22 | | eleq1 2828 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 = 1 → (𝑃 ∈ ℙ ↔ 1 ∈
ℙ)) |
23 | | 1nprm 16382 |
. . . . . . . . . . . . . . . . 17
⊢ ¬ 1
∈ ℙ |
24 | 23 | pm2.21i 119 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
ℙ → 𝑀 =
1) |
25 | 22, 24 | syl6bi 252 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 = 1 → (𝑃 ∈ ℙ → 𝑀 = 1)) |
26 | 11, 25 | syl5com 31 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 = 1 → 𝑀 = 1)) |
27 | 21, 26 | sylbid 239 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∥ 1 →
𝑀 = 1)) |
28 | 27 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
∧ 1 = (𝑃↑𝑀)) → (𝑃 ∥ 1 → 𝑀 = 1)) |
29 | 19, 28 | sylbird 259 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
∧ 1 = (𝑃↑𝑀)) → (𝑃 ∥ (𝑃↑𝑀) → 𝑀 = 1)) |
30 | 29 | ex 413 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
→ (1 = (𝑃↑𝑀) → (𝑃 ∥ (𝑃↑𝑀) → 𝑀 = 1))) |
31 | 17, 30 | mpid 44 |
. . . . . . . . 9
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
→ (1 = (𝑃↑𝑀) → 𝑀 = 1)) |
32 | 31 | adantr 481 |
. . . . . . . 8
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
∧ 𝑁 = 1) → (1 =
(𝑃↑𝑀) → 𝑀 = 1)) |
33 | 10, 32 | sylbid 239 |
. . . . . . 7
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
∧ 𝑁 = 1) →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) → 𝑀 = 1)) |
34 | 33 | ex 413 |
. . . . . 6
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
→ (𝑁 = 1 →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) → 𝑀 = 1))) |
35 | 34 | com23 86 |
. . . . 5
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
→ (((2↑𝑁) −
1) = (𝑃↑𝑀) → (𝑁 = 1 → 𝑀 = 1))) |
36 | 35 | a1d 25 |
. . . 4
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
→ ((¬ 2 ∥ 𝑁
∧ 2 ∥ 𝑀) →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) → (𝑁 = 1 → 𝑀 = 1)))) |
37 | 36 | 3adant3 1131 |
. . 3
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ ((¬ 2 ∥ 𝑁
∧ 2 ∥ 𝑀) →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) → (𝑁 = 1 → 𝑀 = 1)))) |
38 | 37 | 3imp 1110 |
. 2
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ (¬ 2 ∥ 𝑁
∧ 2 ∥ 𝑀) ∧
((2↑𝑁) − 1) =
(𝑃↑𝑀)) → (𝑁 = 1 → 𝑀 = 1)) |
39 | | neqne 2953 |
. . . . . . . . . . . 12
⊢ (¬
𝑁 = 1 → 𝑁 ≠ 1) |
40 | 39 | anim2i 617 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → (𝑁 ∈ ℕ ∧ 𝑁 ≠ 1)) |
41 | | eluz2b3 12661 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≠ 1)) |
42 | 40, 41 | sylibr 233 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → 𝑁 ∈
(ℤ≥‘2)) |
43 | | oddge22np1 16056 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (¬ 2 ∥ 𝑁 ↔ ∃𝑗 ∈ ℕ ((2 · 𝑗) + 1) = 𝑁)) |
44 | 42, 43 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → (¬ 2
∥ 𝑁 ↔
∃𝑗 ∈ ℕ ((2
· 𝑗) + 1) = 𝑁)) |
45 | 44 | 3ad2antl3 1186 |
. . . . . . . 8
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ ¬ 𝑁 = 1) →
(¬ 2 ∥ 𝑁 ↔
∃𝑗 ∈ ℕ ((2
· 𝑗) + 1) = 𝑁)) |
46 | | oveq2 7279 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 = ((2 · 𝑗) + 1) → (2↑𝑁) = (2↑((2 · 𝑗) + 1))) |
47 | 46 | oveq1d 7286 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 = ((2 · 𝑗) + 1) → ((2↑𝑁) − 1) = ((2↑((2
· 𝑗) + 1)) −
1)) |
48 | 47 | eqcoms 2748 |
. . . . . . . . . . . . . . . 16
⊢ (((2
· 𝑗) + 1) = 𝑁 → ((2↑𝑁) − 1) = ((2↑((2
· 𝑗) + 1)) −
1)) |
49 | 2 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → 2 ∈
ℂ) |
50 | | 2nn0 12250 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℕ0 |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ ℕ → 2 ∈
ℕ0) |
52 | | nnnn0 12240 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ0) |
53 | 51, 52 | nn0mulcld 12298 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → (2
· 𝑗) ∈
ℕ0) |
54 | 49, 53 | expp1d 13863 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ →
(2↑((2 · 𝑗) +
1)) = ((2↑(2 · 𝑗)) · 2)) |
55 | 51, 53 | nn0expcld 13959 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ ℕ →
(2↑(2 · 𝑗))
∈ ℕ0) |
56 | 55 | nn0cnd 12295 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ →
(2↑(2 · 𝑗))
∈ ℂ) |
57 | 56, 49 | mulcomd 10997 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ →
((2↑(2 · 𝑗))
· 2) = (2 · (2↑(2 · 𝑗)))) |
58 | 54, 57 | eqtrd 2780 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ →
(2↑((2 · 𝑗) +
1)) = (2 · (2↑(2 · 𝑗)))) |
59 | 58 | oveq1d 7286 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℕ →
((2↑((2 · 𝑗) +
1)) − 1) = ((2 · (2↑(2 · 𝑗))) − 1)) |
60 | | npcan1 11400 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((2↑(2 · 𝑗)) ∈ ℂ → (((2↑(2
· 𝑗)) − 1) +
1) = (2↑(2 · 𝑗))) |
61 | 56, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ ℕ →
(((2↑(2 · 𝑗))
− 1) + 1) = (2↑(2 · 𝑗))) |
62 | 61 | eqcomd 2746 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ →
(2↑(2 · 𝑗)) =
(((2↑(2 · 𝑗))
− 1) + 1)) |
63 | 62 | oveq2d 7287 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → (2
· (2↑(2 · 𝑗))) = (2 · (((2↑(2 · 𝑗)) − 1) +
1))) |
64 | | peano2cnm 11287 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2↑(2 · 𝑗)) ∈ ℂ → ((2↑(2 ·
𝑗)) − 1) ∈
ℂ) |
65 | 56, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ →
((2↑(2 · 𝑗))
− 1) ∈ ℂ) |
66 | | 1cnd 10971 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → 1 ∈
ℂ) |
67 | 49, 65, 66 | adddid 11000 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → (2
· (((2↑(2 · 𝑗)) − 1) + 1)) = ((2 ·
((2↑(2 · 𝑗))
− 1)) + (2 · 1))) |
68 | 63, 67 | eqtrd 2780 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → (2
· (2↑(2 · 𝑗))) = ((2 · ((2↑(2 · 𝑗)) − 1)) + (2 ·
1))) |
69 | 68 | oveq1d 7286 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℕ → ((2
· (2↑(2 · 𝑗))) − 1) = (((2 · ((2↑(2
· 𝑗)) − 1)) +
(2 · 1)) − 1)) |
70 | 49, 65 | mulcld 10996 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → (2
· ((2↑(2 · 𝑗)) − 1)) ∈
ℂ) |
71 | | ax-1cn 10930 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℂ |
72 | 2, 71 | mulcli 10983 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
· 1) ∈ ℂ |
73 | 72 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → (2
· 1) ∈ ℂ) |
74 | 70, 73, 66 | addsubassd 11352 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → (((2
· ((2↑(2 · 𝑗)) − 1)) + (2 · 1)) − 1) =
((2 · ((2↑(2 · 𝑗)) − 1)) + ((2 · 1) −
1))) |
75 | | 2t1e2 12136 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2
· 1) = 2 |
76 | 75 | oveq1i 7281 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((2
· 1) − 1) = (2 − 1) |
77 | 76, 7 | eqtri 2768 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
· 1) − 1) = 1 |
78 | 77 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → ((2
· 1) − 1) = 1) |
79 | 78 | oveq2d 7287 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → ((2
· ((2↑(2 · 𝑗)) − 1)) + ((2 · 1) − 1))
= ((2 · ((2↑(2 · 𝑗)) − 1)) + 1)) |
80 | 74, 79 | eqtrd 2780 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℕ → (((2
· ((2↑(2 · 𝑗)) − 1)) + (2 · 1)) − 1) =
((2 · ((2↑(2 · 𝑗)) − 1)) + 1)) |
81 | 59, 69, 80 | 3eqtrd 2784 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ℕ →
((2↑((2 · 𝑗) +
1)) − 1) = ((2 · ((2↑(2 · 𝑗)) − 1)) + 1)) |
82 | 81 | ad2antlr 724 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
((2↑((2 · 𝑗) +
1)) − 1) = ((2 · ((2↑(2 · 𝑗)) − 1)) + 1)) |
83 | 48, 82 | sylan9eqr 2802 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑃 ∈
(ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 2 ∥ 𝑀) ∧ ((2 · 𝑗) + 1) = 𝑁) → ((2↑𝑁) − 1) = ((2 · ((2↑(2
· 𝑗)) − 1)) +
1)) |
84 | 83 | eqeq1d 2742 |
. . . . . . . . . . . . . 14
⊢
(((((𝑃 ∈
(ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 2 ∥ 𝑀) ∧ ((2 · 𝑗) + 1) = 𝑁) → (((2↑𝑁) − 1) = (𝑃↑𝑀) ↔ ((2 · ((2↑(2 ·
𝑗)) − 1)) + 1) =
(𝑃↑𝑀))) |
85 | 14 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ 𝑃 ∈
ℕ0) |
86 | | nnnn0 12240 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
87 | 86 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ 𝑀 ∈
ℕ0) |
88 | 85, 87 | nn0expcld 13959 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (𝑃↑𝑀) ∈
ℕ0) |
89 | 88 | nn0cnd 12295 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (𝑃↑𝑀) ∈
ℂ) |
90 | 89 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ (𝑃↑𝑀) ∈
ℂ) |
91 | | 1cnd 10971 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ 1 ∈ ℂ) |
92 | 70 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ (2 · ((2↑(2 · 𝑗)) − 1)) ∈
ℂ) |
93 | 90, 91, 92 | 3jca 1127 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ ((𝑃↑𝑀) ∈ ℂ ∧ 1 ∈
ℂ ∧ (2 · ((2↑(2 · 𝑗)) − 1)) ∈
ℂ)) |
94 | 93 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
((𝑃↑𝑀) ∈ ℂ ∧ 1 ∈ ℂ
∧ (2 · ((2↑(2 · 𝑗)) − 1)) ∈
ℂ)) |
95 | | subadd2 11225 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃↑𝑀) ∈ ℂ ∧ 1 ∈ ℂ
∧ (2 · ((2↑(2 · 𝑗)) − 1)) ∈ ℂ) →
(((𝑃↑𝑀) − 1) = (2 · ((2↑(2
· 𝑗)) − 1))
↔ ((2 · ((2↑(2 · 𝑗)) − 1)) + 1) = (𝑃↑𝑀))) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
(((𝑃↑𝑀) − 1) = (2 · ((2↑(2
· 𝑗)) − 1))
↔ ((2 · ((2↑(2 · 𝑗)) − 1)) + 1) = (𝑃↑𝑀))) |
97 | | nncn 11981 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℂ) |
98 | 11, 12, 97 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℂ) |
99 | 98 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ 𝑃 ∈
ℂ) |
100 | 99, 87 | pwm1geoser 15579 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ ((𝑃↑𝑀) − 1) = ((𝑃 − 1) ·
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘))) |
101 | 100 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ ((𝑃↑𝑀) − 1) = ((𝑃 − 1) ·
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘))) |
102 | 101 | eqeq1d 2742 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ (((𝑃↑𝑀) − 1) = (2 ·
((2↑(2 · 𝑗))
− 1)) ↔ ((𝑃
− 1) · Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) = (2 · ((2↑(2 · 𝑗)) −
1)))) |
103 | 102 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
(((𝑃↑𝑀) − 1) = (2 · ((2↑(2
· 𝑗)) − 1))
↔ ((𝑃 − 1)
· Σ𝑘 ∈
(0...(𝑀 − 1))(𝑃↑𝑘)) = (2 · ((2↑(2 · 𝑗)) −
1)))) |
104 | 99 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
𝑃 ∈
ℂ) |
105 | | 1cnd 10971 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) → 1
∈ ℂ) |
106 | 104, 105 | subcld 11332 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
(𝑃 − 1) ∈
ℂ) |
107 | | fzfid 13691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (0...(𝑀 − 1))
∈ Fin) |
108 | 85 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑘 ∈ (0...(𝑀 − 1))) → 𝑃 ∈
ℕ0) |
109 | | elfznn0 13348 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ (0...(𝑀 − 1)) → 𝑘 ∈ ℕ0) |
110 | 109 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑘 ∈ (0...(𝑀 − 1))) → 𝑘 ∈
ℕ0) |
111 | 108, 110 | nn0expcld 13959 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑘 ∈ (0...(𝑀 − 1))) → (𝑃↑𝑘) ∈
ℕ0) |
112 | 111 | nn0zd 12423 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑘 ∈ (0...(𝑀 − 1))) → (𝑃↑𝑘) ∈ ℤ) |
113 | 107, 112 | fsumzcl 15445 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ Σ𝑘 ∈
(0...(𝑀 − 1))(𝑃↑𝑘) ∈ ℤ) |
114 | 113 | zcnd 12426 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ Σ𝑘 ∈
(0...(𝑀 − 1))(𝑃↑𝑘) ∈ ℂ) |
115 | 114 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘) ∈ ℂ) |
116 | 106, 115 | mulcld 10996 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
((𝑃 − 1) ·
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) ∈ ℂ) |
117 | 56 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
(2↑(2 · 𝑗))
∈ ℂ) |
118 | 117, 105 | subcld 11332 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
((2↑(2 · 𝑗))
− 1) ∈ ℂ) |
119 | | 2rp 12734 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℝ+ |
120 | 119 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) → 2
∈ ℝ+) |
121 | 120 | rpcnne0d 12780 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
(2 ∈ ℂ ∧ 2 ≠ 0)) |
122 | | divmul2 11637 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑃 − 1) ·
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) ∈ ℂ ∧ ((2↑(2 ·
𝑗)) − 1) ∈
ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((((𝑃 − 1) · Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) / 2) = ((2↑(2 · 𝑗)) − 1) ↔ ((𝑃 − 1) ·
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) = (2 · ((2↑(2 · 𝑗)) −
1)))) |
123 | 116, 118,
121, 122 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
((((𝑃 − 1) ·
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) / 2) = ((2↑(2 · 𝑗)) − 1) ↔ ((𝑃 − 1) ·
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) = (2 · ((2↑(2 · 𝑗)) −
1)))) |
124 | | div23 11652 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 − 1) ∈ ℂ ∧
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘) ∈ ℂ ∧ (2 ∈ ℂ
∧ 2 ≠ 0)) → (((𝑃 − 1) · Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) / 2) = (((𝑃 − 1) / 2) · Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘))) |
125 | 106, 115,
121, 124 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
(((𝑃 − 1) ·
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) / 2) = (((𝑃 − 1) / 2) · Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘))) |
126 | 125 | eqeq1d 2742 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
((((𝑃 − 1) ·
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) / 2) = ((2↑(2 · 𝑗)) − 1) ↔ (((𝑃 − 1) / 2) ·
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) = ((2↑(2 · 𝑗)) − 1))) |
127 | 51 | nn0zd 12423 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ ℕ → 2 ∈
ℤ) |
128 | | 2nn 12046 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 2 ∈
ℕ |
129 | 128 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 ∈ ℕ → 2 ∈
ℕ) |
130 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ) |
131 | 129, 130 | nnmulcld 12026 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ ℕ → (2
· 𝑗) ∈
ℕ) |
132 | | iddvdsexp 15987 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((2
∈ ℤ ∧ (2 · 𝑗) ∈ ℕ) → 2 ∥ (2↑(2
· 𝑗))) |
133 | 127, 131,
132 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℕ → 2 ∥
(2↑(2 · 𝑗))) |
134 | 133 | notnotd 144 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ ℕ → ¬
¬ 2 ∥ (2↑(2 · 𝑗))) |
135 | 55 | nn0zd 12423 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℕ →
(2↑(2 · 𝑗))
∈ ℤ) |
136 | | oddm1even 16050 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((2↑(2 · 𝑗)) ∈ ℤ → (¬ 2 ∥
(2↑(2 · 𝑗))
↔ 2 ∥ ((2↑(2 · 𝑗)) − 1))) |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ ℕ → (¬ 2
∥ (2↑(2 · 𝑗)) ↔ 2 ∥ ((2↑(2 ·
𝑗)) −
1))) |
138 | 134, 137 | mtbid 324 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → ¬ 2
∥ ((2↑(2 · 𝑗)) − 1)) |
139 | 138 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
¬ 2 ∥ ((2↑(2 · 𝑗)) − 1)) |
140 | | breq2 5083 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑃 − 1) / 2) ·
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) = ((2↑(2 · 𝑗)) − 1) → (2 ∥ (((𝑃 − 1) / 2) ·
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) ↔ 2 ∥ ((2↑(2 ·
𝑗)) −
1))) |
141 | 140 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑃 − 1) / 2) ·
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) = ((2↑(2 · 𝑗)) − 1) → (¬ 2 ∥
(((𝑃 − 1) / 2)
· Σ𝑘 ∈
(0...(𝑀 − 1))(𝑃↑𝑘)) ↔ ¬ 2 ∥ ((2↑(2
· 𝑗)) −
1))) |
142 | 141 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑃 ∈
(ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 2 ∥ 𝑀) ∧ (((𝑃 − 1) / 2) · Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) = ((2↑(2 · 𝑗)) − 1)) → (¬ 2 ∥
(((𝑃 − 1) / 2)
· Σ𝑘 ∈
(0...(𝑀 − 1))(𝑃↑𝑘)) ↔ ¬ 2 ∥ ((2↑(2
· 𝑗)) −
1))) |
143 | | fzfid 13691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
(0...(𝑀 − 1)) ∈
Fin) |
144 | 112 | ad4ant14 749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑃 ∈
(ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 2 ∥ 𝑀) ∧ 𝑘 ∈ (0...(𝑀 − 1))) → (𝑃↑𝑘) ∈ ℤ) |
145 | | elnn0 12235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑘 ∈ ℕ0
↔ (𝑘 ∈ ℕ
∨ 𝑘 =
0)) |
146 | | eldifsn 4726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑃 ∈ (ℙ ∖ {2})
↔ (𝑃 ∈ ℙ
∧ 𝑃 ≠
2)) |
147 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) → 𝑃 ≠ 2) |
148 | 147 | necomd 3001 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) → 2 ≠ 𝑃) |
149 | 146, 148 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 2 ≠ 𝑃) |
150 | 149 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑘 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 2 ≠ 𝑃) |
151 | 150 | neneqd 2950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑘 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ¬ 2 = 𝑃) |
152 | | 2prm 16395 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ 2 ∈
ℙ |
153 | 11 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑘 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 𝑃 ∈
ℙ) |
154 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑘 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 𝑘 ∈
ℕ) |
155 | | prmdvdsexpb 16419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((2
∈ ℙ ∧ 𝑃
∈ ℙ ∧ 𝑘
∈ ℕ) → (2 ∥ (𝑃↑𝑘) ↔ 2 = 𝑃)) |
156 | 152, 153,
154, 155 | mp3an2i 1465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑘 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (2 ∥ (𝑃↑𝑘) ↔ 2 = 𝑃)) |
157 | 151, 156 | mtbird 325 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑘 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ¬ 2 ∥ (𝑃↑𝑘)) |
158 | 157 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑘 ∈ ℕ → (𝑃 ∈ (ℙ ∖ {2})
→ ¬ 2 ∥ (𝑃↑𝑘))) |
159 | | n2dvds1 16075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ¬ 2
∥ 1 |
160 | | oveq2 7279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑘 = 0 → (𝑃↑𝑘) = (𝑃↑0)) |
161 | 98 | exp0d 13856 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃↑0) =
1) |
162 | 160, 161 | sylan9eq 2800 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑘 = 0 ∧ 𝑃 ∈ (ℙ ∖ {2})) → (𝑃↑𝑘) = 1) |
163 | 162 | breq2d 5091 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑘 = 0 ∧ 𝑃 ∈ (ℙ ∖ {2})) → (2
∥ (𝑃↑𝑘) ↔ 2 ∥
1)) |
164 | 159, 163 | mtbiri 327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑘 = 0 ∧ 𝑃 ∈ (ℙ ∖ {2})) → ¬
2 ∥ (𝑃↑𝑘)) |
165 | 164 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑘 = 0 → (𝑃 ∈ (ℙ ∖ {2}) → ¬ 2
∥ (𝑃↑𝑘))) |
166 | 158, 165 | jaoi 854 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑘 ∈ ℕ ∨ 𝑘 = 0) → (𝑃 ∈ (ℙ ∖ {2}) → ¬ 2
∥ (𝑃↑𝑘))) |
167 | 145, 166 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑘 ∈ ℕ0
→ (𝑃 ∈ (ℙ
∖ {2}) → ¬ 2 ∥ (𝑃↑𝑘))) |
168 | 167, 109 | syl11 33 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑘 ∈
(0...(𝑀 − 1)) →
¬ 2 ∥ (𝑃↑𝑘))) |
169 | 168 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (𝑘 ∈
(0...(𝑀 − 1)) →
¬ 2 ∥ (𝑃↑𝑘))) |
170 | 169 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
(𝑘 ∈ (0...(𝑀 − 1)) → ¬ 2
∥ (𝑃↑𝑘))) |
171 | 170 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑃 ∈
(ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 2 ∥ 𝑀) ∧ 𝑘 ∈ (0...(𝑀 − 1))) → ¬ 2 ∥ (𝑃↑𝑘)) |
172 | | nnm1nn0 12274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈
ℕ0) |
173 | | hashfz0 14145 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑀 − 1) ∈
ℕ0 → (♯‘(0...(𝑀 − 1))) = ((𝑀 − 1) + 1)) |
174 | 172, 173 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑀 ∈ ℕ →
(♯‘(0...(𝑀
− 1))) = ((𝑀 −
1) + 1)) |
175 | | nncn 11981 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
176 | | 1cnd 10971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑀 ∈ ℕ → 1 ∈
ℂ) |
177 | 175, 176 | npcand 11336 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑀 ∈ ℕ → ((𝑀 − 1) + 1) = 𝑀) |
178 | 174, 177 | eqtr2d 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑀 ∈ ℕ → 𝑀 = (♯‘(0...(𝑀 − 1)))) |
179 | 178 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ 𝑀 =
(♯‘(0...(𝑀
− 1)))) |
180 | 179 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ 𝑀 =
(♯‘(0...(𝑀
− 1)))) |
181 | 180 | breq2d 5091 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ (2 ∥ 𝑀 ↔
2 ∥ (♯‘(0...(𝑀 − 1))))) |
182 | 181 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) → 2
∥ (♯‘(0...(𝑀 − 1)))) |
183 | 143, 144,
171, 182 | evensumodd 16096 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) → 2
∥ Σ𝑘 ∈
(0...(𝑀 − 1))(𝑃↑𝑘)) |
184 | 183 | olcd 871 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
(2 ∥ ((𝑃 − 1) /
2) ∨ 2 ∥ Σ𝑘
∈ (0...(𝑀 −
1))(𝑃↑𝑘))) |
185 | 152 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
→ 2 ∈ ℙ) |
186 | | oddn2prm 16511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ¬ 2 ∥ 𝑃) |
187 | | oddm1d2 16067 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑃 ∈ ℤ → (¬ 2
∥ 𝑃 ↔ ((𝑃 − 1) / 2) ∈
ℤ)) |
188 | 15, 187 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (¬ 2 ∥ 𝑃
↔ ((𝑃 − 1) / 2)
∈ ℤ)) |
189 | 186, 188 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℤ) |
190 | 189 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
→ ((𝑃 − 1) / 2)
∈ ℤ) |
191 | | fzfid 13691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
→ (0...(𝑀 − 1))
∈ Fin) |
192 | 14 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
∧ 𝑘 ∈ (0...(𝑀 − 1))) → 𝑃 ∈
ℕ0) |
193 | 109 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
∧ 𝑘 ∈ (0...(𝑀 − 1))) → 𝑘 ∈
ℕ0) |
194 | 192, 193 | nn0expcld 13959 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
∧ 𝑘 ∈ (0...(𝑀 − 1))) → (𝑃↑𝑘) ∈
ℕ0) |
195 | 194 | nn0zd 12423 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
∧ 𝑘 ∈ (0...(𝑀 − 1))) → (𝑃↑𝑘) ∈ ℤ) |
196 | 191, 195 | fsumzcl 15445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
→ Σ𝑘 ∈
(0...(𝑀 − 1))(𝑃↑𝑘) ∈ ℤ) |
197 | 185, 190,
196 | 3jca 1127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
→ (2 ∈ ℙ ∧ ((𝑃 − 1) / 2) ∈ ℤ ∧
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘) ∈ ℤ)) |
198 | 197 | 3adant3 1131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (2 ∈ ℙ ∧ ((𝑃 − 1) / 2) ∈ ℤ ∧
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘) ∈ ℤ)) |
199 | | euclemma 16416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((2
∈ ℙ ∧ ((𝑃
− 1) / 2) ∈ ℤ ∧ Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘) ∈ ℤ) → (2 ∥ (((𝑃 − 1) / 2) ·
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) ↔ (2 ∥ ((𝑃 − 1) / 2) ∨ 2 ∥ Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)))) |
200 | 198, 199 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (2 ∥ (((𝑃
− 1) / 2) · Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) ↔ (2 ∥ ((𝑃 − 1) / 2) ∨ 2 ∥ Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)))) |
201 | 200 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
(2 ∥ (((𝑃 − 1)
/ 2) · Σ𝑘
∈ (0...(𝑀 −
1))(𝑃↑𝑘)) ↔ (2 ∥ ((𝑃 − 1) / 2) ∨ 2 ∥
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)))) |
202 | 184, 201 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) → 2
∥ (((𝑃 − 1) /
2) · Σ𝑘 ∈
(0...(𝑀 − 1))(𝑃↑𝑘))) |
203 | 202 | pm2.24d 151 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
(¬ 2 ∥ (((𝑃
− 1) / 2) · Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) → 𝑀 = 1)) |
204 | 203 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑃 ∈
(ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 2 ∥ 𝑀) ∧ (((𝑃 − 1) / 2) · Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) = ((2↑(2 · 𝑗)) − 1)) → (¬ 2 ∥
(((𝑃 − 1) / 2)
· Σ𝑘 ∈
(0...(𝑀 − 1))(𝑃↑𝑘)) → 𝑀 = 1)) |
205 | 142, 204 | sylbird 259 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑃 ∈
(ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 2 ∥ 𝑀) ∧ (((𝑃 − 1) / 2) · Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) = ((2↑(2 · 𝑗)) − 1)) → (¬ 2 ∥
((2↑(2 · 𝑗))
− 1) → 𝑀 =
1)) |
206 | 205 | ex 413 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
((((𝑃 − 1) / 2)
· Σ𝑘 ∈
(0...(𝑀 − 1))(𝑃↑𝑘)) = ((2↑(2 · 𝑗)) − 1) → (¬ 2 ∥
((2↑(2 · 𝑗))
− 1) → 𝑀 =
1))) |
207 | 139, 206 | mpid 44 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
((((𝑃 − 1) / 2)
· Σ𝑘 ∈
(0...(𝑀 − 1))(𝑃↑𝑘)) = ((2↑(2 · 𝑗)) − 1) → 𝑀 = 1)) |
208 | 126, 207 | sylbid 239 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
((((𝑃 − 1) ·
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) / 2) = ((2↑(2 · 𝑗)) − 1) → 𝑀 = 1)) |
209 | 123, 208 | sylbird 259 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
(((𝑃 − 1) ·
Σ𝑘 ∈ (0...(𝑀 − 1))(𝑃↑𝑘)) = (2 · ((2↑(2 · 𝑗)) − 1)) → 𝑀 = 1)) |
210 | 103, 209 | sylbid 239 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
(((𝑃↑𝑀) − 1) = (2 · ((2↑(2
· 𝑗)) − 1))
→ 𝑀 =
1)) |
211 | 96, 210 | sylbird 259 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
∧ 2 ∥ 𝑀) →
(((2 · ((2↑(2 · 𝑗)) − 1)) + 1) = (𝑃↑𝑀) → 𝑀 = 1)) |
212 | 211 | adantr 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝑃 ∈
(ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 2 ∥ 𝑀) ∧ ((2 · 𝑗) + 1) = 𝑁) → (((2 · ((2↑(2 ·
𝑗)) − 1)) + 1) =
(𝑃↑𝑀) → 𝑀 = 1)) |
213 | 84, 212 | sylbid 239 |
. . . . . . . . . . . . 13
⊢
(((((𝑃 ∈
(ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 2 ∥ 𝑀) ∧ ((2 · 𝑗) + 1) = 𝑁) → (((2↑𝑁) − 1) = (𝑃↑𝑀) → 𝑀 = 1)) |
214 | 213 | exp31 420 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ (2 ∥ 𝑀 →
(((2 · 𝑗) + 1) =
𝑁 → (((2↑𝑁) − 1) = (𝑃↑𝑀) → 𝑀 = 1)))) |
215 | 214 | com23 86 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ (((2 · 𝑗) +
1) = 𝑁 → (2 ∥
𝑀 → (((2↑𝑁) − 1) = (𝑃↑𝑀) → 𝑀 = 1)))) |
216 | 215 | rexlimdva 3215 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (∃𝑗 ∈
ℕ ((2 · 𝑗) +
1) = 𝑁 → (2 ∥
𝑀 → (((2↑𝑁) − 1) = (𝑃↑𝑀) → 𝑀 = 1)))) |
217 | 216 | com34 91 |
. . . . . . . . 9
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (∃𝑗 ∈
ℕ ((2 · 𝑗) +
1) = 𝑁 →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) → (2 ∥ 𝑀 → 𝑀 = 1)))) |
218 | 217 | adantr 481 |
. . . . . . . 8
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ ¬ 𝑁 = 1) →
(∃𝑗 ∈ ℕ
((2 · 𝑗) + 1) =
𝑁 → (((2↑𝑁) − 1) = (𝑃↑𝑀) → (2 ∥ 𝑀 → 𝑀 = 1)))) |
219 | 45, 218 | sylbid 239 |
. . . . . . 7
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ ¬ 𝑁 = 1) →
(¬ 2 ∥ 𝑁 →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) → (2 ∥ 𝑀 → 𝑀 = 1)))) |
220 | 219 | com24 95 |
. . . . . 6
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ ¬ 𝑁 = 1) →
(2 ∥ 𝑀 →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) → (¬ 2 ∥ 𝑁 → 𝑀 = 1)))) |
221 | 220 | ex 413 |
. . . . 5
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (¬ 𝑁 = 1 →
(2 ∥ 𝑀 →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) → (¬ 2 ∥ 𝑁 → 𝑀 = 1))))) |
222 | 221 | com25 99 |
. . . 4
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (¬ 2 ∥ 𝑁
→ (2 ∥ 𝑀 →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) → (¬ 𝑁 = 1 → 𝑀 = 1))))) |
223 | 222 | impd 411 |
. . 3
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ ((¬ 2 ∥ 𝑁
∧ 2 ∥ 𝑀) →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) → (¬ 𝑁 = 1 → 𝑀 = 1)))) |
224 | 223 | 3imp 1110 |
. 2
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ (¬ 2 ∥ 𝑁
∧ 2 ∥ 𝑀) ∧
((2↑𝑁) − 1) =
(𝑃↑𝑀)) → (¬ 𝑁 = 1 → 𝑀 = 1)) |
225 | 38, 224 | pm2.61d 179 |
1
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ (¬ 2 ∥ 𝑁
∧ 2 ∥ 𝑀) ∧
((2↑𝑁) − 1) =
(𝑃↑𝑀)) → 𝑀 = 1) |