Proof of Theorem fmtnoprmfac2
Step | Hyp | Ref
| Expression |
1 | | breq1 5030 |
. . . . . . 7
⊢ (𝑃 = 2 → (𝑃 ∥ (FermatNo‘𝑁) ↔ 2 ∥ (FermatNo‘𝑁))) |
2 | 1 | adantr 484 |
. . . . . 6
⊢ ((𝑃 = 2 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑃 ∥
(FermatNo‘𝑁) ↔ 2
∥ (FermatNo‘𝑁))) |
3 | | eluzge2nn0 12362 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈
ℕ0) |
4 | | fmtnoodd 44503 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ¬ 2 ∥ (FermatNo‘𝑁)) |
5 | 3, 4 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → ¬ 2 ∥ (FermatNo‘𝑁)) |
6 | 5 | adantl 485 |
. . . . . . 7
⊢ ((𝑃 = 2 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ¬ 2 ∥ (FermatNo‘𝑁)) |
7 | 6 | pm2.21d 121 |
. . . . . 6
⊢ ((𝑃 = 2 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (2 ∥ (FermatNo‘𝑁) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
8 | 2, 7 | sylbid 243 |
. . . . 5
⊢ ((𝑃 = 2 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑃 ∥
(FermatNo‘𝑁) →
∃𝑘 ∈ ℕ
𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
9 | 8 | a1d 25 |
. . . 4
⊢ ((𝑃 = 2 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑃 ∈ ℙ
→ (𝑃 ∥
(FermatNo‘𝑁) →
∃𝑘 ∈ ℕ
𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
10 | 9 | ex 416 |
. . 3
⊢ (𝑃 = 2 → (𝑁 ∈ (ℤ≥‘2)
→ (𝑃 ∈ ℙ
→ (𝑃 ∥
(FermatNo‘𝑁) →
∃𝑘 ∈ ℕ
𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))))) |
11 | 10 | 3impd 1349 |
. 2
⊢ (𝑃 = 2 → ((𝑁 ∈ (ℤ≥‘2)
∧ 𝑃 ∈ ℙ
∧ 𝑃 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈ ℕ
𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
12 | | simpr1 1195 |
. . . . 5
⊢ ((¬
𝑃 = 2 ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → 𝑁 ∈
(ℤ≥‘2)) |
13 | | neqne 2942 |
. . . . . . . . . 10
⊢ (¬
𝑃 = 2 → 𝑃 ≠ 2) |
14 | 13 | anim2i 620 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ ¬
𝑃 = 2) → (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2)) |
15 | | eldifsn 4672 |
. . . . . . . . 9
⊢ (𝑃 ∈ (ℙ ∖ {2})
↔ (𝑃 ∈ ℙ
∧ 𝑃 ≠
2)) |
16 | 14, 15 | sylibr 237 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ ¬
𝑃 = 2) → 𝑃 ∈ (ℙ ∖
{2})) |
17 | 16 | ex 416 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → (¬
𝑃 = 2 → 𝑃 ∈ (ℙ ∖
{2}))) |
18 | 17 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → (¬ 𝑃 = 2 → 𝑃 ∈ (ℙ ∖
{2}))) |
19 | 18 | impcom 411 |
. . . . 5
⊢ ((¬
𝑃 = 2 ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → 𝑃 ∈ (ℙ ∖
{2})) |
20 | | simpr3 1197 |
. . . . 5
⊢ ((¬
𝑃 = 2 ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → 𝑃 ∥ (FermatNo‘𝑁)) |
21 | | fmtnoprmfac2lem1 44536 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1) |
22 | 12, 19, 20, 21 | syl3anc 1372 |
. . . 4
⊢ ((¬
𝑃 = 2 ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1) |
23 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ ¬
𝑃 = 2) → 𝑃 ∈
ℙ) |
24 | | 2nn 11782 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ |
25 | 24 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ ¬
𝑃 = 2) → 2 ∈
ℕ) |
26 | | oddprm 16240 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
27 | 16, 26 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ ¬
𝑃 = 2) → ((𝑃 − 1) / 2) ∈
ℕ) |
28 | 27 | nnnn0d 12029 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ ¬
𝑃 = 2) → ((𝑃 − 1) / 2) ∈
ℕ0) |
29 | 25, 28 | nnexpcld 13691 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ ¬
𝑃 = 2) →
(2↑((𝑃 − 1) /
2)) ∈ ℕ) |
30 | 29 | nnzd 12160 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ ¬
𝑃 = 2) →
(2↑((𝑃 − 1) /
2)) ∈ ℤ) |
31 | 23, 30 | jca 515 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ ¬
𝑃 = 2) → (𝑃 ∈ ℙ ∧
(2↑((𝑃 − 1) /
2)) ∈ ℤ)) |
32 | 31 | ex 416 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → (¬
𝑃 = 2 → (𝑃 ∈ ℙ ∧
(2↑((𝑃 − 1) /
2)) ∈ ℤ))) |
33 | 32 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → (¬ 𝑃 = 2 → (𝑃 ∈ ℙ ∧ (2↑((𝑃 − 1) / 2)) ∈
ℤ))) |
34 | 33 | impcom 411 |
. . . . . 6
⊢ ((¬
𝑃 = 2 ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → (𝑃 ∈ ℙ ∧ (2↑((𝑃 − 1) / 2)) ∈
ℤ)) |
35 | | modprm1div 16227 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧
(2↑((𝑃 − 1) /
2)) ∈ ℤ) → (((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1 ↔ 𝑃 ∥ ((2↑((𝑃 − 1) / 2)) −
1))) |
36 | 34, 35 | syl 17 |
. . . . 5
⊢ ((¬
𝑃 = 2 ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → (((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1 ↔ 𝑃 ∥ ((2↑((𝑃 − 1) / 2)) −
1))) |
37 | | prmnn 16108 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
38 | 37 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ ¬
𝑃 = 2) → 𝑃 ∈
ℕ) |
39 | | 2z 12088 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℤ |
40 | 39 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ ¬
𝑃 = 2) → 2 ∈
ℤ) |
41 | 13 | necomd 2989 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑃 = 2 → 2 ≠ 𝑃) |
42 | 41 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ ¬
𝑃 = 2) → 2 ≠ 𝑃) |
43 | | 2prm 16126 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℙ |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑃 = 2 → 2 ∈
ℙ) |
45 | 44 | anim2i 620 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ ¬
𝑃 = 2) → (𝑃 ∈ ℙ ∧ 2 ∈
ℙ)) |
46 | 45 | ancomd 465 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ ¬
𝑃 = 2) → (2 ∈
ℙ ∧ 𝑃 ∈
ℙ)) |
47 | | prmrp 16146 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℙ ∧ 𝑃
∈ ℙ) → ((2 gcd 𝑃) = 1 ↔ 2 ≠ 𝑃)) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ ¬
𝑃 = 2) → ((2 gcd 𝑃) = 1 ↔ 2 ≠ 𝑃)) |
49 | 42, 48 | mpbird 260 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ ¬
𝑃 = 2) → (2 gcd 𝑃) = 1) |
50 | 38, 40, 49 | 3jca 1129 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ ¬
𝑃 = 2) → (𝑃 ∈ ℕ ∧ 2 ∈
ℤ ∧ (2 gcd 𝑃) =
1)) |
51 | 50, 28 | jca 515 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ ¬
𝑃 = 2) → ((𝑃 ∈ ℕ ∧ 2 ∈
ℤ ∧ (2 gcd 𝑃) =
1) ∧ ((𝑃 − 1) /
2) ∈ ℕ0)) |
52 | 51 | ex 416 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → (¬
𝑃 = 2 → ((𝑃 ∈ ℕ ∧ 2 ∈
ℤ ∧ (2 gcd 𝑃) =
1) ∧ ((𝑃 − 1) /
2) ∈ ℕ0))) |
53 | 52 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → (¬ 𝑃 = 2 → ((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧
(2 gcd 𝑃) = 1) ∧
((𝑃 − 1) / 2) ∈
ℕ0))) |
54 | 53 | impcom 411 |
. . . . . . 7
⊢ ((¬
𝑃 = 2 ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → ((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧
(2 gcd 𝑃) = 1) ∧
((𝑃 − 1) / 2) ∈
ℕ0)) |
55 | | odzdvds 16225 |
. . . . . . 7
⊢ (((𝑃 ∈ ℕ ∧ 2 ∈
ℤ ∧ (2 gcd 𝑃) =
1) ∧ ((𝑃 − 1) /
2) ∈ ℕ0) → (𝑃 ∥ ((2↑((𝑃 − 1) / 2)) − 1) ↔
((odℤ‘𝑃)‘2) ∥ ((𝑃 − 1) / 2))) |
56 | 54, 55 | syl 17 |
. . . . . 6
⊢ ((¬
𝑃 = 2 ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → (𝑃 ∥ ((2↑((𝑃 − 1) / 2)) − 1) ↔
((odℤ‘𝑃)‘2) ∥ ((𝑃 − 1) / 2))) |
57 | | eluz2nn 12359 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℕ) |
58 | 57 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → 𝑁 ∈ ℕ) |
59 | 58 | adantl 485 |
. . . . . . . 8
⊢ ((¬
𝑃 = 2 ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → 𝑁 ∈ ℕ) |
60 | | fmtnoprmfac1lem 44534 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∥
(FermatNo‘𝑁)) →
((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))) |
61 | 59, 19, 20, 60 | syl3anc 1372 |
. . . . . . 7
⊢ ((¬
𝑃 = 2 ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) →
((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))) |
62 | | breq1 5030 |
. . . . . . . . . 10
⊢
(((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1)) →
(((odℤ‘𝑃)‘2) ∥ ((𝑃 − 1) / 2) ↔ (2↑(𝑁 + 1)) ∥ ((𝑃 − 1) /
2))) |
63 | 62 | adantl 485 |
. . . . . . . . 9
⊢ (((¬
𝑃 = 2 ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) ∧ ((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))) →
(((odℤ‘𝑃)‘2) ∥ ((𝑃 − 1) / 2) ↔ (2↑(𝑁 + 1)) ∥ ((𝑃 − 1) /
2))) |
64 | 24 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈ ℕ) |
65 | | peano2nn 11721 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) |
66 | 57, 65 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 + 1) ∈ ℕ) |
67 | 66 | nnnn0d 12029 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 + 1) ∈
ℕ0) |
68 | 64, 67 | nnexpcld 13691 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(𝑁 + 1)) ∈ ℕ) |
69 | | nndivides 15702 |
. . . . . . . . . . . . . . 15
⊢
(((2↑(𝑁 + 1))
∈ ℕ ∧ ((𝑃
− 1) / 2) ∈ ℕ) → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) ↔ ∃𝑘 ∈ ℕ (𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2))) |
70 | 68, 27, 69 | syl2an 599 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2)) → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) ↔
∃𝑘 ∈ ℕ
(𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2))) |
71 | | eqcom 2745 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2) ↔ ((𝑃 − 1) / 2) = (𝑘 · (2↑(𝑁 + 1)))) |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2) ↔ ((𝑃 − 1) / 2) = (𝑘 · (2↑(𝑁 + 1))))) |
73 | 37 | nncnd 11725 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℂ) |
74 | | peano2cnm 11023 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℂ → (𝑃 − 1) ∈
ℂ) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℙ → (𝑃 − 1) ∈
ℂ) |
76 | 75 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (𝑃 − 1) ∈ ℂ) |
77 | 76 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑃 − 1) ∈ ℂ) |
78 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
79 | 68 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (2↑(𝑁 + 1)) ∈
ℕ) |
80 | 78, 79 | nnmulcld 11762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑘 · (2↑(𝑁 + 1))) ∈ ℕ) |
81 | 80 | nncnd 11725 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑘 · (2↑(𝑁 + 1))) ∈ ℂ) |
82 | | 2cnne0 11919 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
83 | 82 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (2 ∈ ℂ
∧ 2 ≠ 0)) |
84 | | divmul3 11374 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 − 1) ∈ ℂ ∧
(𝑘 · (2↑(𝑁 + 1))) ∈ ℂ ∧ (2
∈ ℂ ∧ 2 ≠ 0)) → (((𝑃 − 1) / 2) = (𝑘 · (2↑(𝑁 + 1))) ↔ (𝑃 − 1) = ((𝑘 · (2↑(𝑁 + 1))) · 2))) |
85 | 77, 81, 83, 84 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (((𝑃 − 1) / 2) = (𝑘 · (2↑(𝑁 + 1))) ↔ (𝑃 − 1) = ((𝑘 · (2↑(𝑁 + 1))) · 2))) |
86 | | nncn 11717 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
87 | 86 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ) |
88 | 68 | nncnd 11725 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(𝑁 + 1)) ∈ ℂ) |
89 | 88 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (2↑(𝑁 + 1)) ∈
ℂ) |
90 | | 2cnd 11787 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 2 ∈
ℂ) |
91 | 87, 89, 90 | mulassd 10735 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑘 · (2↑(𝑁 + 1))) · 2) = (𝑘 · ((2↑(𝑁 + 1)) · 2))) |
92 | | 2cnd 11787 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 2 ∈
ℂ) |
93 | 65 | nnnn0d 12029 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ0) |
94 | 92, 93 | expp1d 13596 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ →
(2↑((𝑁 + 1) + 1)) =
((2↑(𝑁 + 1)) ·
2)) |
95 | | nncn 11717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
96 | | add1p1 11960 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) + 1) = (𝑁 + 2)) |
97 | 95, 96 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) + 1) = (𝑁 + 2)) |
98 | 97 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ →
(2↑((𝑁 + 1) + 1)) =
(2↑(𝑁 +
2))) |
99 | 94, 98 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ →
((2↑(𝑁 + 1)) ·
2) = (2↑(𝑁 +
2))) |
100 | 57, 99 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2↑(𝑁 + 1)) · 2) = (2↑(𝑁 + 2))) |
101 | 100 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((2↑(𝑁 + 1)) · 2) =
(2↑(𝑁 +
2))) |
102 | 101 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑘 · ((2↑(𝑁 + 1)) · 2)) = (𝑘 · (2↑(𝑁 + 2)))) |
103 | 91, 102 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑘 · (2↑(𝑁 + 1))) · 2) = (𝑘 · (2↑(𝑁 + 2)))) |
104 | 103 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑃 − 1) = ((𝑘 · (2↑(𝑁 + 1))) · 2) ↔ (𝑃 − 1) = (𝑘 · (2↑(𝑁 + 2))))) |
105 | 73 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → 𝑃 ∈ ℂ) |
106 | 105 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑃 ∈ ℂ) |
107 | | 1cnd 10707 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 1 ∈
ℂ) |
108 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ) |
109 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → 2 ∈
ℕ) |
110 | 108, 109 | nnaddcld 11761 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → (𝑁 + 2) ∈
ℕ) |
111 | 110 | nnnn0d 12029 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → (𝑁 + 2) ∈
ℕ0) |
112 | 57, 111 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 + 2) ∈
ℕ0) |
113 | 64, 112 | nnexpcld 13691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(𝑁 + 2)) ∈ ℕ) |
114 | 113 | nncnd 11725 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(𝑁 + 2)) ∈ ℂ) |
115 | 114 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (2↑(𝑁 + 2)) ∈
ℂ) |
116 | 87, 115 | mulcld 10732 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑘 · (2↑(𝑁 + 2))) ∈ ℂ) |
117 | 106, 107,
116 | subadd2d 11087 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑃 − 1) = (𝑘 · (2↑(𝑁 + 2))) ↔ ((𝑘 · (2↑(𝑁 + 2))) + 1) = 𝑃)) |
118 | | eqcom 2745 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑘 · (2↑(𝑁 + 2))) + 1) = 𝑃 ↔ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)) |
119 | 118 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (((𝑘 · (2↑(𝑁 + 2))) + 1) = 𝑃 ↔ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
120 | 104, 117,
119 | 3bitrd 308 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑃 − 1) = ((𝑘 · (2↑(𝑁 + 1))) · 2) ↔ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
121 | 72, 85, 120 | 3bitrd 308 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2) ↔ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
122 | 121 | rexbidva 3205 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (∃𝑘 ∈ ℕ (𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2) ↔ ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
123 | 122 | biimpd 232 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (∃𝑘 ∈ ℕ (𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
124 | 123 | adantrr 717 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2)) → (∃𝑘 ∈ ℕ (𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
125 | 70, 124 | sylbid 243 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2)) → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) →
∃𝑘 ∈ ℕ
𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
126 | 125 | expr 460 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (¬ 𝑃 = 2 → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) →
∃𝑘 ∈ ℕ
𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
127 | 126 | 3adant3 1133 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → (¬ 𝑃 = 2 → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
128 | 127 | impcom 411 |
. . . . . . . . . 10
⊢ ((¬
𝑃 = 2 ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
129 | 128 | adantr 484 |
. . . . . . . . 9
⊢ (((¬
𝑃 = 2 ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) ∧ ((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))) → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) →
∃𝑘 ∈ ℕ
𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
130 | 63, 129 | sylbid 243 |
. . . . . . . 8
⊢ (((¬
𝑃 = 2 ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) ∧ ((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))) →
(((odℤ‘𝑃)‘2) ∥ ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
131 | 130 | ex 416 |
. . . . . . 7
⊢ ((¬
𝑃 = 2 ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) →
(((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1)) →
(((odℤ‘𝑃)‘2) ∥ ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
132 | 61, 131 | mpd 15 |
. . . . . 6
⊢ ((¬
𝑃 = 2 ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) →
(((odℤ‘𝑃)‘2) ∥ ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
133 | 56, 132 | sylbid 243 |
. . . . 5
⊢ ((¬
𝑃 = 2 ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → (𝑃 ∥ ((2↑((𝑃 − 1) / 2)) − 1) →
∃𝑘 ∈ ℕ
𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
134 | 36, 133 | sylbid 243 |
. . . 4
⊢ ((¬
𝑃 = 2 ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → (((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1 → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
135 | 22, 134 | mpd 15 |
. . 3
⊢ ((¬
𝑃 = 2 ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)) |
136 | 135 | ex 416 |
. 2
⊢ (¬
𝑃 = 2 → ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
137 | 11, 136 | pm2.61i 185 |
1
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)) |