Step | Hyp | Ref
| Expression |
1 | | simpl 476 |
. . 3
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 𝑃
∈ ℤ) |
2 | | 2nn0 11661 |
. . . . . . 7
⊢ 2 ∈
ℕ0 |
3 | 2 | numexp1 16185 |
. . . . . 6
⊢
(2↑1) = 2 |
4 | | df-2 11438 |
. . . . . 6
⊢ 2 = (1 +
1) |
5 | 3, 4 | eqtri 2801 |
. . . . 5
⊢
(2↑1) = (1 + 1) |
6 | | prmuz2 15813 |
. . . . . . . 8
⊢
(((2↑𝑃) −
1) ∈ ℙ → ((2↑𝑃) − 1) ∈
(ℤ≥‘2)) |
7 | 6 | adantl 475 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑𝑃) − 1) ∈
(ℤ≥‘2)) |
8 | | eluz2b2 12068 |
. . . . . . . 8
⊢
(((2↑𝑃) −
1) ∈ (ℤ≥‘2) ↔ (((2↑𝑃) − 1) ∈ ℕ ∧ 1 <
((2↑𝑃) −
1))) |
9 | 8 | simprbi 492 |
. . . . . . 7
⊢
(((2↑𝑃) −
1) ∈ (ℤ≥‘2) → 1 < ((2↑𝑃) − 1)) |
10 | 7, 9 | syl 17 |
. . . . . 6
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 1 < ((2↑𝑃) − 1)) |
11 | | 1red 10377 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 1 ∈ ℝ) |
12 | | 2re 11449 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
13 | 12 | a1i 11 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 2 ∈ ℝ) |
14 | | 2ne0 11486 |
. . . . . . . . 9
⊢ 2 ≠
0 |
15 | 14 | a1i 11 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 2 ≠ 0) |
16 | 13, 15, 1 | reexpclzd 13355 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (2↑𝑃) ∈ ℝ) |
17 | 11, 11, 16 | ltaddsubd 10975 |
. . . . . 6
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((1 + 1) < (2↑𝑃) ↔ 1 < ((2↑𝑃) − 1))) |
18 | 10, 17 | mpbird 249 |
. . . . 5
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (1 + 1) < (2↑𝑃)) |
19 | 5, 18 | syl5eqbr 4921 |
. . . 4
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (2↑1) < (2↑𝑃)) |
20 | | 1zzd 11760 |
. . . . 5
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 1 ∈ ℤ) |
21 | | 1lt2 11553 |
. . . . . 6
⊢ 1 <
2 |
22 | 21 | a1i 11 |
. . . . 5
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 1 < 2) |
23 | 13, 20, 1, 22 | ltexp2d 13359 |
. . . 4
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (1 < 𝑃 ↔ (2↑1) < (2↑𝑃))) |
24 | 19, 23 | mpbird 249 |
. . 3
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 1 < 𝑃) |
25 | | eluz2b1 12066 |
. . 3
⊢ (𝑃 ∈
(ℤ≥‘2) ↔ (𝑃 ∈ ℤ ∧ 1 < 𝑃)) |
26 | 1, 24, 25 | sylanbrc 578 |
. 2
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 𝑃
∈ (ℤ≥‘2)) |
27 | | simpllr 766 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑃) − 1) ∈
ℙ) |
28 | | prmnn 15793 |
. . . . . . . 8
⊢
(((2↑𝑃) −
1) ∈ ℙ → ((2↑𝑃) − 1) ∈
ℕ) |
29 | 27, 28 | syl 17 |
. . . . . . 7
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑃) − 1) ∈
ℕ) |
30 | 29 | nncnd 11392 |
. . . . . 6
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑃) − 1) ∈
ℂ) |
31 | | 2nn 11448 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ |
32 | | elfzuz 12655 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (2...(𝑃 − 1)) → 𝑘 ∈
(ℤ≥‘2)) |
33 | 32 | ad2antlr 717 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑘 ∈
(ℤ≥‘2)) |
34 | | eluz2nn 12032 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(ℤ≥‘2) → 𝑘 ∈ ℕ) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑘 ∈ ℕ) |
36 | 35 | nnnn0d 11702 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑘 ∈ ℕ0) |
37 | | nnexpcl 13191 |
. . . . . . . . . . 11
⊢ ((2
∈ ℕ ∧ 𝑘
∈ ℕ0) → (2↑𝑘) ∈ ℕ) |
38 | 31, 36, 37 | sylancr 581 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑𝑘) ∈
ℕ) |
39 | 38 | nnzd 11833 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑𝑘) ∈
ℤ) |
40 | | peano2zm 11772 |
. . . . . . . . 9
⊢
((2↑𝑘) ∈
ℤ → ((2↑𝑘)
− 1) ∈ ℤ) |
41 | 39, 40 | syl 17 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) ∈
ℤ) |
42 | 41 | zred 11834 |
. . . . . . 7
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) ∈
ℝ) |
43 | 42 | recnd 10405 |
. . . . . 6
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) ∈
ℂ) |
44 | | 0red 10380 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 0 ∈
ℝ) |
45 | | 1red 10377 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 1 ∈
ℝ) |
46 | | 0lt1 10897 |
. . . . . . . . . 10
⊢ 0 <
1 |
47 | 46 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 0 <
1) |
48 | | eluz2b2 12068 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈
(ℤ≥‘2) ↔ (𝑘 ∈ ℕ ∧ 1 < 𝑘)) |
49 | 48 | simprbi 492 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(ℤ≥‘2) → 1 < 𝑘) |
50 | 33, 49 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 1 < 𝑘) |
51 | 12 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 2 ∈
ℝ) |
52 | | 1zzd 11760 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 1 ∈
ℤ) |
53 | | elfzelz 12659 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (2...(𝑃 − 1)) → 𝑘 ∈ ℤ) |
54 | 53 | ad2antlr 717 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑘 ∈ ℤ) |
55 | 21 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 1 <
2) |
56 | 51, 52, 54, 55 | ltexp2d 13359 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (1 < 𝑘 ↔ (2↑1) <
(2↑𝑘))) |
57 | 50, 56 | mpbid 224 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑1) <
(2↑𝑘)) |
58 | 5, 57 | syl5eqbrr 4922 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (1 + 1) <
(2↑𝑘)) |
59 | 38 | nnred 11391 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑𝑘) ∈
ℝ) |
60 | 45, 45, 59 | ltaddsubd 10975 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((1 + 1) <
(2↑𝑘) ↔ 1 <
((2↑𝑘) −
1))) |
61 | 58, 60 | mpbid 224 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 1 < ((2↑𝑘) − 1)) |
62 | 44, 45, 42, 47, 61 | lttrd 10537 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 0 < ((2↑𝑘) − 1)) |
63 | | elnnz 11738 |
. . . . . . . 8
⊢
(((2↑𝑘) −
1) ∈ ℕ ↔ (((2↑𝑘) − 1) ∈ ℤ ∧ 0 <
((2↑𝑘) −
1))) |
64 | 41, 62, 63 | sylanbrc 578 |
. . . . . . 7
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) ∈
ℕ) |
65 | 64 | nnne0d 11425 |
. . . . . 6
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) ≠
0) |
66 | 30, 43, 65 | divcan2d 11153 |
. . . . 5
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (((2↑𝑘) − 1) ·
(((2↑𝑃) − 1) /
((2↑𝑘) − 1))) =
((2↑𝑃) −
1)) |
67 | 66, 27 | eqeltrd 2858 |
. . . 4
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (((2↑𝑘) − 1) ·
(((2↑𝑃) − 1) /
((2↑𝑘) − 1)))
∈ ℙ) |
68 | | eluz2b2 12068 |
. . . . . 6
⊢
(((2↑𝑘) −
1) ∈ (ℤ≥‘2) ↔ (((2↑𝑘) − 1) ∈ ℕ ∧ 1 <
((2↑𝑘) −
1))) |
69 | 64, 61, 68 | sylanbrc 578 |
. . . . 5
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) ∈
(ℤ≥‘2)) |
70 | 38 | nncnd 11392 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑𝑘) ∈
ℂ) |
71 | | ax-1cn 10330 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
72 | | subeq0 10649 |
. . . . . . . . . . . 12
⊢
(((2↑𝑘) ∈
ℂ ∧ 1 ∈ ℂ) → (((2↑𝑘) − 1) = 0 ↔ (2↑𝑘) = 1)) |
73 | 70, 71, 72 | sylancl 580 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (((2↑𝑘) − 1) = 0 ↔
(2↑𝑘) =
1)) |
74 | 73 | necon3bid 3012 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (((2↑𝑘) − 1) ≠ 0 ↔
(2↑𝑘) ≠
1)) |
75 | 65, 74 | mpbid 224 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑𝑘) ≠ 1) |
76 | | simpr 479 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑘 ∥ 𝑃) |
77 | | eluz2nn 12032 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈
(ℤ≥‘2) → 𝑃 ∈ ℕ) |
78 | 26, 77 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 𝑃
∈ ℕ) |
79 | 78 | ad2antrr 716 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑃 ∈ ℕ) |
80 | | nndivdvds 15396 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑘 ∥ 𝑃 ↔ (𝑃 / 𝑘) ∈ ℕ)) |
81 | 79, 35, 80 | syl2anc 579 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (𝑘 ∥ 𝑃 ↔ (𝑃 / 𝑘) ∈ ℕ)) |
82 | 76, 81 | mpbid 224 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (𝑃 / 𝑘) ∈ ℕ) |
83 | 82 | nnnn0d 11702 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (𝑃 / 𝑘) ∈
ℕ0) |
84 | 70, 75, 83 | geoser 15003 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → Σ𝑛 ∈ (0...((𝑃 / 𝑘) − 1))((2↑𝑘)↑𝑛) = ((1 − ((2↑𝑘)↑(𝑃 / 𝑘))) / (1 − (2↑𝑘)))) |
85 | 16 | ad2antrr 716 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑𝑃) ∈
ℝ) |
86 | 85 | recnd 10405 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑𝑃) ∈
ℂ) |
87 | | negsubdi2 10682 |
. . . . . . . . . . 11
⊢
(((2↑𝑃) ∈
ℂ ∧ 1 ∈ ℂ) → -((2↑𝑃) − 1) = (1 − (2↑𝑃))) |
88 | 86, 71, 87 | sylancl 580 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → -((2↑𝑃) − 1) = (1 −
(2↑𝑃))) |
89 | 79 | nncnd 11392 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑃 ∈ ℂ) |
90 | 35 | nncnd 11392 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑘 ∈ ℂ) |
91 | 35 | nnne0d 11425 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑘 ≠ 0) |
92 | 89, 90, 91 | divcan2d 11153 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (𝑘 · (𝑃 / 𝑘)) = 𝑃) |
93 | 92 | oveq2d 6938 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑(𝑘 · (𝑃 / 𝑘))) = (2↑𝑃)) |
94 | 51 | recnd 10405 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 2 ∈
ℂ) |
95 | 94, 83, 36 | expmuld 13330 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑(𝑘 · (𝑃 / 𝑘))) = ((2↑𝑘)↑(𝑃 / 𝑘))) |
96 | 93, 95 | eqtr3d 2815 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑𝑃) = ((2↑𝑘)↑(𝑃 / 𝑘))) |
97 | 96 | oveq2d 6938 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (1 −
(2↑𝑃)) = (1 −
((2↑𝑘)↑(𝑃 / 𝑘)))) |
98 | 88, 97 | eqtrd 2813 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → -((2↑𝑃) − 1) = (1 −
((2↑𝑘)↑(𝑃 / 𝑘)))) |
99 | | negsubdi2 10682 |
. . . . . . . . . 10
⊢
(((2↑𝑘) ∈
ℂ ∧ 1 ∈ ℂ) → -((2↑𝑘) − 1) = (1 − (2↑𝑘))) |
100 | 70, 71, 99 | sylancl 580 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → -((2↑𝑘) − 1) = (1 −
(2↑𝑘))) |
101 | 98, 100 | oveq12d 6940 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (-((2↑𝑃) − 1) / -((2↑𝑘) − 1)) = ((1 −
((2↑𝑘)↑(𝑃 / 𝑘))) / (1 − (2↑𝑘)))) |
102 | 30, 43, 65 | div2negd 11166 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (-((2↑𝑃) − 1) / -((2↑𝑘) − 1)) = (((2↑𝑃) − 1) / ((2↑𝑘) − 1))) |
103 | 84, 101, 102 | 3eqtr2d 2819 |
. . . . . . 7
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → Σ𝑛 ∈ (0...((𝑃 / 𝑘) − 1))((2↑𝑘)↑𝑛) = (((2↑𝑃) − 1) / ((2↑𝑘) − 1))) |
104 | | fzfid 13091 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (0...((𝑃 / 𝑘) − 1)) ∈ Fin) |
105 | | elfznn0 12751 |
. . . . . . . . 9
⊢ (𝑛 ∈ (0...((𝑃 / 𝑘) − 1)) → 𝑛 ∈ ℕ0) |
106 | | zexpcl 13193 |
. . . . . . . . 9
⊢
(((2↑𝑘) ∈
ℤ ∧ 𝑛 ∈
ℕ0) → ((2↑𝑘)↑𝑛) ∈ ℤ) |
107 | 39, 105, 106 | syl2an 589 |
. . . . . . . 8
⊢
(((((𝑃 ∈
ℤ ∧ ((2↑𝑃)
− 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) ∧ 𝑛 ∈ (0...((𝑃 / 𝑘) − 1))) → ((2↑𝑘)↑𝑛) ∈ ℤ) |
108 | 104, 107 | fsumzcl 14873 |
. . . . . . 7
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → Σ𝑛 ∈ (0...((𝑃 / 𝑘) − 1))((2↑𝑘)↑𝑛) ∈ ℤ) |
109 | 103, 108 | eqeltrrd 2859 |
. . . . . 6
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (((2↑𝑃) − 1) / ((2↑𝑘) − 1)) ∈
ℤ) |
110 | 43 | mulid2d 10395 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (1 ·
((2↑𝑘) − 1)) =
((2↑𝑘) −
1)) |
111 | | 2z 11761 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
112 | | elfzm11 12729 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℤ ∧ 𝑃
∈ ℤ) → (𝑘
∈ (2...(𝑃 − 1))
↔ (𝑘 ∈ ℤ
∧ 2 ≤ 𝑘 ∧ 𝑘 < 𝑃))) |
113 | 111, 1, 112 | sylancr 581 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (𝑘
∈ (2...(𝑃 − 1))
↔ (𝑘 ∈ ℤ
∧ 2 ≤ 𝑘 ∧ 𝑘 < 𝑃))) |
114 | 113 | biimpa 470 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
→ (𝑘 ∈ ℤ
∧ 2 ≤ 𝑘 ∧ 𝑘 < 𝑃)) |
115 | 114 | simp3d 1135 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
→ 𝑘 < 𝑃) |
116 | 115 | adantr 474 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑘 < 𝑃) |
117 | 1 | ad2antrr 716 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑃 ∈ ℤ) |
118 | 51, 54, 117, 55 | ltexp2d 13359 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (𝑘 < 𝑃 ↔ (2↑𝑘) < (2↑𝑃))) |
119 | 116, 118 | mpbid 224 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑𝑘) < (2↑𝑃)) |
120 | 59, 85, 45, 119 | ltsub1dd 10987 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) < ((2↑𝑃) − 1)) |
121 | 110, 120 | eqbrtrd 4908 |
. . . . . . 7
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (1 ·
((2↑𝑘) − 1))
< ((2↑𝑃) −
1)) |
122 | 29 | nnred 11391 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑃) − 1) ∈
ℝ) |
123 | | ltmuldiv 11250 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ ((2↑𝑃) − 1) ∈ ℝ ∧
(((2↑𝑘) − 1)
∈ ℝ ∧ 0 < ((2↑𝑘) − 1))) → ((1 ·
((2↑𝑘) − 1))
< ((2↑𝑃) − 1)
↔ 1 < (((2↑𝑃)
− 1) / ((2↑𝑘)
− 1)))) |
124 | 45, 122, 42, 62, 123 | syl112anc 1442 |
. . . . . . 7
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((1 ·
((2↑𝑘) − 1))
< ((2↑𝑃) − 1)
↔ 1 < (((2↑𝑃)
− 1) / ((2↑𝑘)
− 1)))) |
125 | 121, 124 | mpbid 224 |
. . . . . 6
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 1 < (((2↑𝑃) − 1) / ((2↑𝑘) − 1))) |
126 | | eluz2b1 12066 |
. . . . . 6
⊢
((((2↑𝑃)
− 1) / ((2↑𝑘)
− 1)) ∈ (ℤ≥‘2) ↔ ((((2↑𝑃) − 1) / ((2↑𝑘) − 1)) ∈ ℤ
∧ 1 < (((2↑𝑃)
− 1) / ((2↑𝑘)
− 1)))) |
127 | 109, 125,
126 | sylanbrc 578 |
. . . . 5
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (((2↑𝑃) − 1) / ((2↑𝑘) − 1)) ∈
(ℤ≥‘2)) |
128 | | nprm 15806 |
. . . . 5
⊢
((((2↑𝑘)
− 1) ∈ (ℤ≥‘2) ∧ (((2↑𝑃) − 1) / ((2↑𝑘) − 1)) ∈
(ℤ≥‘2)) → ¬ (((2↑𝑘) − 1) · (((2↑𝑃) − 1) / ((2↑𝑘) − 1))) ∈
ℙ) |
129 | 69, 127, 128 | syl2anc 579 |
. . . 4
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ¬ (((2↑𝑘) − 1) ·
(((2↑𝑃) − 1) /
((2↑𝑘) − 1)))
∈ ℙ) |
130 | 67, 129 | pm2.65da 807 |
. . 3
⊢ (((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
→ ¬ 𝑘 ∥
𝑃) |
131 | 130 | ralrimiva 3147 |
. 2
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ∀𝑘 ∈ (2...(𝑃 − 1)) ¬ 𝑘 ∥ 𝑃) |
132 | | isprm3 15801 |
. 2
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑘 ∈ (2...(𝑃 − 1)) ¬ 𝑘 ∥ 𝑃)) |
133 | 26, 131, 132 | sylanbrc 578 |
1
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 𝑃
∈ ℙ) |