Proof of Theorem wilthlem1
Step | Hyp | Ref
| Expression |
1 | | elfzelz 12213 |
. . . . . . . . . 10
⊢ (𝑁 ∈ (1...(𝑃 − 1)) → 𝑁 ∈ ℤ) |
2 | 1 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ ℤ) |
3 | | peano2zm 11297 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
4 | 2, 3 | syl 17 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 − 1) ∈ ℤ) |
5 | 4 | zcnd 11359 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 − 1) ∈ ℂ) |
6 | 2 | peano2zd 11361 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 + 1) ∈ ℤ) |
7 | 6 | zcnd 11359 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 + 1) ∈ ℂ) |
8 | 5, 7 | mulcomd 9940 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 − 1) · (𝑁 + 1)) = ((𝑁 + 1) · (𝑁 − 1))) |
9 | 2 | zcnd 11359 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ ℂ) |
10 | | ax-1cn 9873 |
. . . . . . 7
⊢ 1 ∈
ℂ |
11 | | subsq 12834 |
. . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁↑2)
− (1↑2)) = ((𝑁 +
1) · (𝑁 −
1))) |
12 | 9, 10, 11 | sylancl 693 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁↑2) − (1↑2)) = ((𝑁 + 1) · (𝑁 − 1))) |
13 | 9 | sqvald 12867 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁↑2) = (𝑁 · 𝑁)) |
14 | | sq1 12820 |
. . . . . . . 8
⊢
(1↑2) = 1 |
15 | 14 | a1i 11 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (1↑2) =
1) |
16 | 13, 15 | oveq12d 6567 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁↑2) − (1↑2)) = ((𝑁 · 𝑁) − 1)) |
17 | 8, 12, 16 | 3eqtr2d 2650 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 − 1) · (𝑁 + 1)) = ((𝑁 · 𝑁) − 1)) |
18 | 17 | breq2d 4595 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ ((𝑁 − 1) · (𝑁 + 1)) ↔ 𝑃 ∥ ((𝑁 · 𝑁) − 1))) |
19 | | 1e0p1 11428 |
. . . . . . . 8
⊢ 1 = (0 +
1) |
20 | 19 | oveq1i 6559 |
. . . . . . 7
⊢
(1...(𝑃 − 1))
= ((0 + 1)...(𝑃 −
1)) |
21 | | 0z 11265 |
. . . . . . . 8
⊢ 0 ∈
ℤ |
22 | | fzp1ss 12262 |
. . . . . . . 8
⊢ (0 ∈
ℤ → ((0 + 1)...(𝑃 − 1)) ⊆ (0...(𝑃 − 1))) |
23 | 21, 22 | ax-mp 5 |
. . . . . . 7
⊢ ((0 +
1)...(𝑃 − 1)) ⊆
(0...(𝑃 −
1)) |
24 | 20, 23 | eqsstri 3598 |
. . . . . 6
⊢
(1...(𝑃 − 1))
⊆ (0...(𝑃 −
1)) |
25 | | simpr 476 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ (1...(𝑃 − 1))) |
26 | 24, 25 | sseldi 3566 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ (0...(𝑃 − 1))) |
27 | 26 | biantrurd 528 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ ((𝑁 · 𝑁) − 1) ↔ (𝑁 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑁 · 𝑁) − 1)))) |
28 | 18, 27 | bitrd 267 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ ((𝑁 − 1) · (𝑁 + 1)) ↔ (𝑁 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑁 · 𝑁) − 1)))) |
29 | | simpl 472 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈ ℙ) |
30 | | euclemma 15263 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 − 1) ∈ ℤ ∧
(𝑁 + 1) ∈ ℤ)
→ (𝑃 ∥ ((𝑁 − 1) · (𝑁 + 1)) ↔ (𝑃 ∥ (𝑁 − 1) ∨ 𝑃 ∥ (𝑁 + 1)))) |
31 | 29, 4, 6, 30 | syl3anc 1318 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ ((𝑁 − 1) · (𝑁 + 1)) ↔ (𝑃 ∥ (𝑁 − 1) ∨ 𝑃 ∥ (𝑁 + 1)))) |
32 | | prmnn 15226 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
33 | | fzm1ndvds 14882 |
. . . . 5
⊢ ((𝑃 ∈ ℕ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ 𝑁) |
34 | 32, 33 | sylan 487 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ 𝑁) |
35 | | eqid 2610 |
. . . . 5
⊢ ((𝑁↑(𝑃 − 2)) mod 𝑃) = ((𝑁↑(𝑃 − 2)) mod 𝑃) |
36 | 35 | prmdiveq 15329 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → ((𝑁 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑁 · 𝑁) − 1)) ↔ 𝑁 = ((𝑁↑(𝑃 − 2)) mod 𝑃))) |
37 | 29, 2, 34, 36 | syl3anc 1318 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑁 · 𝑁) − 1)) ↔ 𝑁 = ((𝑁↑(𝑃 − 2)) mod 𝑃))) |
38 | 28, 31, 37 | 3bitr3rd 298 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 = ((𝑁↑(𝑃 − 2)) mod 𝑃) ↔ (𝑃 ∥ (𝑁 − 1) ∨ 𝑃 ∥ (𝑁 + 1)))) |
39 | 29, 32 | syl 17 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈ ℕ) |
40 | | 1zzd 11285 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 1 ∈
ℤ) |
41 | | moddvds 14829 |
. . . . 5
⊢ ((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℤ ∧ 1 ∈
ℤ) → ((𝑁 mod
𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ (𝑁 − 1))) |
42 | 39, 2, 40, 41 | syl3anc 1318 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ (𝑁 − 1))) |
43 | | elfznn 12241 |
. . . . . . . 8
⊢ (𝑁 ∈ (1...(𝑃 − 1)) → 𝑁 ∈ ℕ) |
44 | 43 | adantl 481 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ ℕ) |
45 | 44 | nnred 10912 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ ℝ) |
46 | 39 | nnrpd 11746 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈
ℝ+) |
47 | 44 | nnnn0d 11228 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈
ℕ0) |
48 | 47 | nn0ge0d 11231 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 0 ≤ 𝑁) |
49 | | elfzle2 12216 |
. . . . . . . 8
⊢ (𝑁 ∈ (1...(𝑃 − 1)) → 𝑁 ≤ (𝑃 − 1)) |
50 | 49 | adantl 481 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ≤ (𝑃 − 1)) |
51 | | prmz 15227 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
52 | | zltlem1 11307 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑁 < 𝑃 ↔ 𝑁 ≤ (𝑃 − 1))) |
53 | 1, 51, 52 | syl2anr 494 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 < 𝑃 ↔ 𝑁 ≤ (𝑃 − 1))) |
54 | 50, 53 | mpbird 246 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 < 𝑃) |
55 | | modid 12557 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 𝑃 ∈ ℝ+)
∧ (0 ≤ 𝑁 ∧ 𝑁 < 𝑃)) → (𝑁 mod 𝑃) = 𝑁) |
56 | 45, 46, 48, 54, 55 | syl22anc 1319 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 mod 𝑃) = 𝑁) |
57 | 39 | nnred 10912 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈ ℝ) |
58 | | prmuz2 15246 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
59 | 29, 58 | syl 17 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈
(ℤ≥‘2)) |
60 | | eluz2b2 11637 |
. . . . . . . 8
⊢ (𝑃 ∈
(ℤ≥‘2) ↔ (𝑃 ∈ ℕ ∧ 1 < 𝑃)) |
61 | 60 | simprbi 479 |
. . . . . . 7
⊢ (𝑃 ∈
(ℤ≥‘2) → 1 < 𝑃) |
62 | 59, 61 | syl 17 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 1 < 𝑃) |
63 | | 1mod 12564 |
. . . . . 6
⊢ ((𝑃 ∈ ℝ ∧ 1 <
𝑃) → (1 mod 𝑃) = 1) |
64 | 57, 62, 63 | syl2anc 691 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (1 mod 𝑃) = 1) |
65 | 56, 64 | eqeq12d 2625 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 mod 𝑃) = (1 mod 𝑃) ↔ 𝑁 = 1)) |
66 | 42, 65 | bitr3d 269 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ (𝑁 − 1) ↔ 𝑁 = 1)) |
67 | 40 | znegcld 11360 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → -1 ∈
ℤ) |
68 | | moddvds 14829 |
. . . . 5
⊢ ((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℤ ∧ -1 ∈
ℤ) → ((𝑁 mod
𝑃) = (-1 mod 𝑃) ↔ 𝑃 ∥ (𝑁 − -1))) |
69 | 39, 2, 67, 68 | syl3anc 1318 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 mod 𝑃) = (-1 mod 𝑃) ↔ 𝑃 ∥ (𝑁 − -1))) |
70 | 39 | nncnd 10913 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈ ℂ) |
71 | 70 | mulid2d 9937 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (1 · 𝑃) = 𝑃) |
72 | 71 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (-1 + (1 · 𝑃)) = (-1 + 𝑃)) |
73 | | neg1cn 11001 |
. . . . . . . . 9
⊢ -1 ∈
ℂ |
74 | | addcom 10101 |
. . . . . . . . 9
⊢ ((-1
∈ ℂ ∧ 𝑃
∈ ℂ) → (-1 + 𝑃) = (𝑃 + -1)) |
75 | 73, 70, 74 | sylancr 694 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (-1 + 𝑃) = (𝑃 + -1)) |
76 | | negsub 10208 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑃 + -1) =
(𝑃 −
1)) |
77 | 70, 10, 76 | sylancl 693 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 + -1) = (𝑃 − 1)) |
78 | 72, 75, 77 | 3eqtrd 2648 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (-1 + (1 · 𝑃)) = (𝑃 − 1)) |
79 | 78 | oveq1d 6564 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((-1 + (1 ·
𝑃)) mod 𝑃) = ((𝑃 − 1) mod 𝑃)) |
80 | | neg1rr 11002 |
. . . . . . . 8
⊢ -1 ∈
ℝ |
81 | 80 | a1i 11 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → -1 ∈
ℝ) |
82 | | modcyc 12567 |
. . . . . . 7
⊢ ((-1
∈ ℝ ∧ 𝑃
∈ ℝ+ ∧ 1 ∈ ℤ) → ((-1 + (1 ·
𝑃)) mod 𝑃) = (-1 mod 𝑃)) |
83 | 81, 46, 40, 82 | syl3anc 1318 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((-1 + (1 ·
𝑃)) mod 𝑃) = (-1 mod 𝑃)) |
84 | | peano2rem 10227 |
. . . . . . . 8
⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈
ℝ) |
85 | 57, 84 | syl 17 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 − 1) ∈ ℝ) |
86 | | nnm1nn0 11211 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
87 | 39, 86 | syl 17 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 − 1) ∈
ℕ0) |
88 | 87 | nn0ge0d 11231 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 0 ≤ (𝑃 − 1)) |
89 | 57 | ltm1d 10835 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 − 1) < 𝑃) |
90 | | modid 12557 |
. . . . . . 7
⊢ ((((𝑃 − 1) ∈ ℝ ∧
𝑃 ∈
ℝ+) ∧ (0 ≤ (𝑃 − 1) ∧ (𝑃 − 1) < 𝑃)) → ((𝑃 − 1) mod 𝑃) = (𝑃 − 1)) |
91 | 85, 46, 88, 89, 90 | syl22anc 1319 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑃 − 1) mod 𝑃) = (𝑃 − 1)) |
92 | 79, 83, 91 | 3eqtr3d 2652 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (-1 mod 𝑃) = (𝑃 − 1)) |
93 | 56, 92 | eqeq12d 2625 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 mod 𝑃) = (-1 mod 𝑃) ↔ 𝑁 = (𝑃 − 1))) |
94 | | subneg 10209 |
. . . . . 6
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑁 −
-1) = (𝑁 +
1)) |
95 | 9, 10, 94 | sylancl 693 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 − -1) = (𝑁 + 1)) |
96 | 95 | breq2d 4595 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ (𝑁 − -1) ↔ 𝑃 ∥ (𝑁 + 1))) |
97 | 69, 93, 96 | 3bitr3rd 298 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ (𝑁 + 1) ↔ 𝑁 = (𝑃 − 1))) |
98 | 66, 97 | orbi12d 742 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑃 ∥ (𝑁 − 1) ∨ 𝑃 ∥ (𝑁 + 1)) ↔ (𝑁 = 1 ∨ 𝑁 = (𝑃 − 1)))) |
99 | 38, 98 | bitrd 267 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 = ((𝑁↑(𝑃 − 2)) mod 𝑃) ↔ (𝑁 = 1 ∨ 𝑁 = (𝑃 − 1)))) |