Proof of Theorem wilthlem1
Step | Hyp | Ref
| Expression |
1 | | elfzelz 12659 |
. . . . . . . . . 10
⊢ (𝑁 ∈ (1...(𝑃 − 1)) → 𝑁 ∈ ℤ) |
2 | 1 | adantl 475 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ ℤ) |
3 | | peano2zm 11772 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
4 | 2, 3 | syl 17 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 − 1) ∈ ℤ) |
5 | 4 | zcnd 11835 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 − 1) ∈ ℂ) |
6 | 2 | peano2zd 11837 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 + 1) ∈ ℤ) |
7 | 6 | zcnd 11835 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 + 1) ∈ ℂ) |
8 | 5, 7 | mulcomd 10398 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 − 1) · (𝑁 + 1)) = ((𝑁 + 1) · (𝑁 − 1))) |
9 | 2 | zcnd 11835 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ ℂ) |
10 | | ax-1cn 10330 |
. . . . . . 7
⊢ 1 ∈
ℂ |
11 | | subsq 13291 |
. . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁↑2)
− (1↑2)) = ((𝑁 +
1) · (𝑁 −
1))) |
12 | 9, 10, 11 | sylancl 580 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁↑2) − (1↑2)) = ((𝑁 + 1) · (𝑁 − 1))) |
13 | 9 | sqvald 13324 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁↑2) = (𝑁 · 𝑁)) |
14 | | sq1 13277 |
. . . . . . . 8
⊢
(1↑2) = 1 |
15 | 14 | a1i 11 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (1↑2) =
1) |
16 | 13, 15 | oveq12d 6940 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁↑2) − (1↑2)) = ((𝑁 · 𝑁) − 1)) |
17 | 8, 12, 16 | 3eqtr2d 2820 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 − 1) · (𝑁 + 1)) = ((𝑁 · 𝑁) − 1)) |
18 | 17 | breq2d 4898 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ ((𝑁 − 1) · (𝑁 + 1)) ↔ 𝑃 ∥ ((𝑁 · 𝑁) − 1))) |
19 | | fz1ssfz0 12754 |
. . . . . 6
⊢
(1...(𝑃 − 1))
⊆ (0...(𝑃 −
1)) |
20 | | simpr 479 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ (1...(𝑃 − 1))) |
21 | 19, 20 | sseldi 3819 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ (0...(𝑃 − 1))) |
22 | 21 | biantrurd 528 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ ((𝑁 · 𝑁) − 1) ↔ (𝑁 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑁 · 𝑁) − 1)))) |
23 | 18, 22 | bitrd 271 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ ((𝑁 − 1) · (𝑁 + 1)) ↔ (𝑁 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑁 · 𝑁) − 1)))) |
24 | | simpl 476 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈ ℙ) |
25 | | euclemma 15829 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 − 1) ∈ ℤ ∧
(𝑁 + 1) ∈ ℤ)
→ (𝑃 ∥ ((𝑁 − 1) · (𝑁 + 1)) ↔ (𝑃 ∥ (𝑁 − 1) ∨ 𝑃 ∥ (𝑁 + 1)))) |
26 | 24, 4, 6, 25 | syl3anc 1439 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ ((𝑁 − 1) · (𝑁 + 1)) ↔ (𝑃 ∥ (𝑁 − 1) ∨ 𝑃 ∥ (𝑁 + 1)))) |
27 | | prmnn 15793 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
28 | | fzm1ndvds 15451 |
. . . . 5
⊢ ((𝑃 ∈ ℕ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ 𝑁) |
29 | 27, 28 | sylan 575 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ 𝑁) |
30 | | eqid 2778 |
. . . . 5
⊢ ((𝑁↑(𝑃 − 2)) mod 𝑃) = ((𝑁↑(𝑃 − 2)) mod 𝑃) |
31 | 30 | prmdiveq 15895 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → ((𝑁 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑁 · 𝑁) − 1)) ↔ 𝑁 = ((𝑁↑(𝑃 − 2)) mod 𝑃))) |
32 | 24, 2, 29, 31 | syl3anc 1439 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑁 · 𝑁) − 1)) ↔ 𝑁 = ((𝑁↑(𝑃 − 2)) mod 𝑃))) |
33 | 23, 26, 32 | 3bitr3rd 302 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 = ((𝑁↑(𝑃 − 2)) mod 𝑃) ↔ (𝑃 ∥ (𝑁 − 1) ∨ 𝑃 ∥ (𝑁 + 1)))) |
34 | 24, 27 | syl 17 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈ ℕ) |
35 | | 1zzd 11760 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 1 ∈
ℤ) |
36 | | moddvds 15398 |
. . . . 5
⊢ ((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℤ ∧ 1 ∈
ℤ) → ((𝑁 mod
𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ (𝑁 − 1))) |
37 | 34, 2, 35, 36 | syl3anc 1439 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ (𝑁 − 1))) |
38 | | elfznn 12687 |
. . . . . . . 8
⊢ (𝑁 ∈ (1...(𝑃 − 1)) → 𝑁 ∈ ℕ) |
39 | 38 | adantl 475 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ ℕ) |
40 | 39 | nnred 11391 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ ℝ) |
41 | 34 | nnrpd 12179 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈
ℝ+) |
42 | 39 | nnnn0d 11702 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈
ℕ0) |
43 | 42 | nn0ge0d 11705 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 0 ≤ 𝑁) |
44 | | elfzle2 12662 |
. . . . . . . 8
⊢ (𝑁 ∈ (1...(𝑃 − 1)) → 𝑁 ≤ (𝑃 − 1)) |
45 | 44 | adantl 475 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ≤ (𝑃 − 1)) |
46 | | prmz 15794 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
47 | | zltlem1 11782 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑁 < 𝑃 ↔ 𝑁 ≤ (𝑃 − 1))) |
48 | 1, 46, 47 | syl2anr 590 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 < 𝑃 ↔ 𝑁 ≤ (𝑃 − 1))) |
49 | 45, 48 | mpbird 249 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 < 𝑃) |
50 | | modid 13014 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 𝑃 ∈ ℝ+)
∧ (0 ≤ 𝑁 ∧ 𝑁 < 𝑃)) → (𝑁 mod 𝑃) = 𝑁) |
51 | 40, 41, 43, 49, 50 | syl22anc 829 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 mod 𝑃) = 𝑁) |
52 | 34 | nnred 11391 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈ ℝ) |
53 | | prmuz2 15813 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
54 | 24, 53 | syl 17 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈
(ℤ≥‘2)) |
55 | | eluz2b2 12068 |
. . . . . . . 8
⊢ (𝑃 ∈
(ℤ≥‘2) ↔ (𝑃 ∈ ℕ ∧ 1 < 𝑃)) |
56 | 55 | simprbi 492 |
. . . . . . 7
⊢ (𝑃 ∈
(ℤ≥‘2) → 1 < 𝑃) |
57 | 54, 56 | syl 17 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 1 < 𝑃) |
58 | | 1mod 13021 |
. . . . . 6
⊢ ((𝑃 ∈ ℝ ∧ 1 <
𝑃) → (1 mod 𝑃) = 1) |
59 | 52, 57, 58 | syl2anc 579 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (1 mod 𝑃) = 1) |
60 | 51, 59 | eqeq12d 2793 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 mod 𝑃) = (1 mod 𝑃) ↔ 𝑁 = 1)) |
61 | 37, 60 | bitr3d 273 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ (𝑁 − 1) ↔ 𝑁 = 1)) |
62 | 35 | znegcld 11836 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → -1 ∈
ℤ) |
63 | | moddvds 15398 |
. . . . 5
⊢ ((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℤ ∧ -1 ∈
ℤ) → ((𝑁 mod
𝑃) = (-1 mod 𝑃) ↔ 𝑃 ∥ (𝑁 − -1))) |
64 | 34, 2, 62, 63 | syl3anc 1439 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 mod 𝑃) = (-1 mod 𝑃) ↔ 𝑃 ∥ (𝑁 − -1))) |
65 | 34 | nncnd 11392 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈ ℂ) |
66 | 65 | mulid2d 10395 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (1 · 𝑃) = 𝑃) |
67 | 66 | oveq2d 6938 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (-1 + (1 · 𝑃)) = (-1 + 𝑃)) |
68 | | neg1cn 11496 |
. . . . . . . . 9
⊢ -1 ∈
ℂ |
69 | | addcom 10562 |
. . . . . . . . 9
⊢ ((-1
∈ ℂ ∧ 𝑃
∈ ℂ) → (-1 + 𝑃) = (𝑃 + -1)) |
70 | 68, 65, 69 | sylancr 581 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (-1 + 𝑃) = (𝑃 + -1)) |
71 | | negsub 10671 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑃 + -1) =
(𝑃 −
1)) |
72 | 65, 10, 71 | sylancl 580 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 + -1) = (𝑃 − 1)) |
73 | 67, 70, 72 | 3eqtrd 2818 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (-1 + (1 · 𝑃)) = (𝑃 − 1)) |
74 | 73 | oveq1d 6937 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((-1 + (1 ·
𝑃)) mod 𝑃) = ((𝑃 − 1) mod 𝑃)) |
75 | | neg1rr 11497 |
. . . . . . . 8
⊢ -1 ∈
ℝ |
76 | 75 | a1i 11 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → -1 ∈
ℝ) |
77 | | modcyc 13024 |
. . . . . . 7
⊢ ((-1
∈ ℝ ∧ 𝑃
∈ ℝ+ ∧ 1 ∈ ℤ) → ((-1 + (1 ·
𝑃)) mod 𝑃) = (-1 mod 𝑃)) |
78 | 76, 41, 35, 77 | syl3anc 1439 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((-1 + (1 ·
𝑃)) mod 𝑃) = (-1 mod 𝑃)) |
79 | | peano2rem 10690 |
. . . . . . . 8
⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈
ℝ) |
80 | 52, 79 | syl 17 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 − 1) ∈ ℝ) |
81 | | nnm1nn0 11685 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
82 | 34, 81 | syl 17 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 − 1) ∈
ℕ0) |
83 | 82 | nn0ge0d 11705 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 0 ≤ (𝑃 − 1)) |
84 | 52 | ltm1d 11310 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 − 1) < 𝑃) |
85 | | modid 13014 |
. . . . . . 7
⊢ ((((𝑃 − 1) ∈ ℝ ∧
𝑃 ∈
ℝ+) ∧ (0 ≤ (𝑃 − 1) ∧ (𝑃 − 1) < 𝑃)) → ((𝑃 − 1) mod 𝑃) = (𝑃 − 1)) |
86 | 80, 41, 83, 84, 85 | syl22anc 829 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑃 − 1) mod 𝑃) = (𝑃 − 1)) |
87 | 74, 78, 86 | 3eqtr3d 2822 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (-1 mod 𝑃) = (𝑃 − 1)) |
88 | 51, 87 | eqeq12d 2793 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 mod 𝑃) = (-1 mod 𝑃) ↔ 𝑁 = (𝑃 − 1))) |
89 | | subneg 10672 |
. . . . . 6
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑁 −
-1) = (𝑁 +
1)) |
90 | 9, 10, 89 | sylancl 580 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 − -1) = (𝑁 + 1)) |
91 | 90 | breq2d 4898 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ (𝑁 − -1) ↔ 𝑃 ∥ (𝑁 + 1))) |
92 | 64, 88, 91 | 3bitr3rd 302 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ (𝑁 + 1) ↔ 𝑁 = (𝑃 − 1))) |
93 | 61, 92 | orbi12d 905 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑃 ∥ (𝑁 − 1) ∨ 𝑃 ∥ (𝑁 + 1)) ↔ (𝑁 = 1 ∨ 𝑁 = (𝑃 − 1)))) |
94 | 33, 93 | bitrd 271 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 = ((𝑁↑(𝑃 − 2)) mod 𝑃) ↔ (𝑁 = 1 ∨ 𝑁 = (𝑃 − 1)))) |