Proof of Theorem wilthlem1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elfzelz 13564 | . . . . . . . . . 10
⊢ (𝑁 ∈ (1...(𝑃 − 1)) → 𝑁 ∈ ℤ) | 
| 2 | 1 | adantl 481 | . . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ ℤ) | 
| 3 |  | peano2zm 12660 | . . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) | 
| 4 | 2, 3 | syl 17 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 − 1) ∈ ℤ) | 
| 5 | 4 | zcnd 12723 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 − 1) ∈ ℂ) | 
| 6 | 2 | peano2zd 12725 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 + 1) ∈ ℤ) | 
| 7 | 6 | zcnd 12723 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 + 1) ∈ ℂ) | 
| 8 | 5, 7 | mulcomd 11282 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 − 1) · (𝑁 + 1)) = ((𝑁 + 1) · (𝑁 − 1))) | 
| 9 | 2 | zcnd 12723 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ ℂ) | 
| 10 |  | ax-1cn 11213 | . . . . . . 7
⊢ 1 ∈
ℂ | 
| 11 |  | subsq 14249 | . . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁↑2)
− (1↑2)) = ((𝑁 +
1) · (𝑁 −
1))) | 
| 12 | 9, 10, 11 | sylancl 586 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁↑2) − (1↑2)) = ((𝑁 + 1) · (𝑁 − 1))) | 
| 13 | 9 | sqvald 14183 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁↑2) = (𝑁 · 𝑁)) | 
| 14 |  | sq1 14234 | . . . . . . . 8
⊢
(1↑2) = 1 | 
| 15 | 14 | a1i 11 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (1↑2) =
1) | 
| 16 | 13, 15 | oveq12d 7449 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁↑2) − (1↑2)) = ((𝑁 · 𝑁) − 1)) | 
| 17 | 8, 12, 16 | 3eqtr2d 2783 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 − 1) · (𝑁 + 1)) = ((𝑁 · 𝑁) − 1)) | 
| 18 | 17 | breq2d 5155 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ ((𝑁 − 1) · (𝑁 + 1)) ↔ 𝑃 ∥ ((𝑁 · 𝑁) − 1))) | 
| 19 |  | fz1ssfz0 13663 | . . . . . 6
⊢
(1...(𝑃 − 1))
⊆ (0...(𝑃 −
1)) | 
| 20 |  | simpr 484 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ (1...(𝑃 − 1))) | 
| 21 | 19, 20 | sselid 3981 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ (0...(𝑃 − 1))) | 
| 22 | 21 | biantrurd 532 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ ((𝑁 · 𝑁) − 1) ↔ (𝑁 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑁 · 𝑁) − 1)))) | 
| 23 | 18, 22 | bitrd 279 | . . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ ((𝑁 − 1) · (𝑁 + 1)) ↔ (𝑁 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑁 · 𝑁) − 1)))) | 
| 24 |  | simpl 482 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈ ℙ) | 
| 25 |  | euclemma 16750 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 − 1) ∈ ℤ ∧
(𝑁 + 1) ∈ ℤ)
→ (𝑃 ∥ ((𝑁 − 1) · (𝑁 + 1)) ↔ (𝑃 ∥ (𝑁 − 1) ∨ 𝑃 ∥ (𝑁 + 1)))) | 
| 26 | 24, 4, 6, 25 | syl3anc 1373 | . . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ ((𝑁 − 1) · (𝑁 + 1)) ↔ (𝑃 ∥ (𝑁 − 1) ∨ 𝑃 ∥ (𝑁 + 1)))) | 
| 27 |  | prmnn 16711 | . . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 28 |  | fzm1ndvds 16359 | . . . . 5
⊢ ((𝑃 ∈ ℕ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ 𝑁) | 
| 29 | 27, 28 | sylan 580 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ 𝑁) | 
| 30 |  | eqid 2737 | . . . . 5
⊢ ((𝑁↑(𝑃 − 2)) mod 𝑃) = ((𝑁↑(𝑃 − 2)) mod 𝑃) | 
| 31 | 30 | prmdiveq 16823 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → ((𝑁 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑁 · 𝑁) − 1)) ↔ 𝑁 = ((𝑁↑(𝑃 − 2)) mod 𝑃))) | 
| 32 | 24, 2, 29, 31 | syl3anc 1373 | . . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑁 · 𝑁) − 1)) ↔ 𝑁 = ((𝑁↑(𝑃 − 2)) mod 𝑃))) | 
| 33 | 23, 26, 32 | 3bitr3rd 310 | . 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 = ((𝑁↑(𝑃 − 2)) mod 𝑃) ↔ (𝑃 ∥ (𝑁 − 1) ∨ 𝑃 ∥ (𝑁 + 1)))) | 
| 34 | 24, 27 | syl 17 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈ ℕ) | 
| 35 |  | 1zzd 12648 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 1 ∈
ℤ) | 
| 36 |  | moddvds 16301 | . . . . 5
⊢ ((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℤ ∧ 1 ∈
ℤ) → ((𝑁 mod
𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ (𝑁 − 1))) | 
| 37 | 34, 2, 35, 36 | syl3anc 1373 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ (𝑁 − 1))) | 
| 38 |  | elfznn 13593 | . . . . . . . 8
⊢ (𝑁 ∈ (1...(𝑃 − 1)) → 𝑁 ∈ ℕ) | 
| 39 | 38 | adantl 481 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ ℕ) | 
| 40 | 39 | nnred 12281 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ ℝ) | 
| 41 | 34 | nnrpd 13075 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈
ℝ+) | 
| 42 | 39 | nnnn0d 12587 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈
ℕ0) | 
| 43 | 42 | nn0ge0d 12590 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 0 ≤ 𝑁) | 
| 44 |  | elfzle2 13568 | . . . . . . . 8
⊢ (𝑁 ∈ (1...(𝑃 − 1)) → 𝑁 ≤ (𝑃 − 1)) | 
| 45 | 44 | adantl 481 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ≤ (𝑃 − 1)) | 
| 46 |  | prmz 16712 | . . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) | 
| 47 |  | zltlem1 12670 | . . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑁 < 𝑃 ↔ 𝑁 ≤ (𝑃 − 1))) | 
| 48 | 1, 46, 47 | syl2anr 597 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 < 𝑃 ↔ 𝑁 ≤ (𝑃 − 1))) | 
| 49 | 45, 48 | mpbird 257 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 < 𝑃) | 
| 50 |  | modid 13936 | . . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 𝑃 ∈ ℝ+)
∧ (0 ≤ 𝑁 ∧ 𝑁 < 𝑃)) → (𝑁 mod 𝑃) = 𝑁) | 
| 51 | 40, 41, 43, 49, 50 | syl22anc 839 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 mod 𝑃) = 𝑁) | 
| 52 | 34 | nnred 12281 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈ ℝ) | 
| 53 |  | prmuz2 16733 | . . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) | 
| 54 | 24, 53 | syl 17 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈
(ℤ≥‘2)) | 
| 55 |  | eluz2gt1 12962 | . . . . . . 7
⊢ (𝑃 ∈
(ℤ≥‘2) → 1 < 𝑃) | 
| 56 | 54, 55 | syl 17 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 1 < 𝑃) | 
| 57 |  | 1mod 13943 | . . . . . 6
⊢ ((𝑃 ∈ ℝ ∧ 1 <
𝑃) → (1 mod 𝑃) = 1) | 
| 58 | 52, 56, 57 | syl2anc 584 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (1 mod 𝑃) = 1) | 
| 59 | 51, 58 | eqeq12d 2753 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 mod 𝑃) = (1 mod 𝑃) ↔ 𝑁 = 1)) | 
| 60 | 37, 59 | bitr3d 281 | . . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ (𝑁 − 1) ↔ 𝑁 = 1)) | 
| 61 | 35 | znegcld 12724 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → -1 ∈
ℤ) | 
| 62 |  | moddvds 16301 | . . . . 5
⊢ ((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℤ ∧ -1 ∈
ℤ) → ((𝑁 mod
𝑃) = (-1 mod 𝑃) ↔ 𝑃 ∥ (𝑁 − -1))) | 
| 63 | 34, 2, 61, 62 | syl3anc 1373 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 mod 𝑃) = (-1 mod 𝑃) ↔ 𝑃 ∥ (𝑁 − -1))) | 
| 64 | 34 | nncnd 12282 | . . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈ ℂ) | 
| 65 | 64 | mullidd 11279 | . . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (1 · 𝑃) = 𝑃) | 
| 66 | 65 | oveq2d 7447 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (-1 + (1 · 𝑃)) = (-1 + 𝑃)) | 
| 67 |  | neg1cn 12380 | . . . . . . . . 9
⊢ -1 ∈
ℂ | 
| 68 |  | addcom 11447 | . . . . . . . . 9
⊢ ((-1
∈ ℂ ∧ 𝑃
∈ ℂ) → (-1 + 𝑃) = (𝑃 + -1)) | 
| 69 | 67, 64, 68 | sylancr 587 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (-1 + 𝑃) = (𝑃 + -1)) | 
| 70 |  | negsub 11557 | . . . . . . . . 9
⊢ ((𝑃 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑃 + -1) =
(𝑃 −
1)) | 
| 71 | 64, 10, 70 | sylancl 586 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 + -1) = (𝑃 − 1)) | 
| 72 | 66, 69, 71 | 3eqtrd 2781 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (-1 + (1 · 𝑃)) = (𝑃 − 1)) | 
| 73 | 72 | oveq1d 7446 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((-1 + (1 ·
𝑃)) mod 𝑃) = ((𝑃 − 1) mod 𝑃)) | 
| 74 |  | neg1rr 12381 | . . . . . . . 8
⊢ -1 ∈
ℝ | 
| 75 | 74 | a1i 11 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → -1 ∈
ℝ) | 
| 76 |  | modcyc 13946 | . . . . . . 7
⊢ ((-1
∈ ℝ ∧ 𝑃
∈ ℝ+ ∧ 1 ∈ ℤ) → ((-1 + (1 ·
𝑃)) mod 𝑃) = (-1 mod 𝑃)) | 
| 77 | 75, 41, 35, 76 | syl3anc 1373 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((-1 + (1 ·
𝑃)) mod 𝑃) = (-1 mod 𝑃)) | 
| 78 |  | peano2rem 11576 | . . . . . . . 8
⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈
ℝ) | 
| 79 | 52, 78 | syl 17 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 − 1) ∈ ℝ) | 
| 80 |  | nnm1nn0 12567 | . . . . . . . . 9
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) | 
| 81 | 34, 80 | syl 17 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 − 1) ∈
ℕ0) | 
| 82 | 81 | nn0ge0d 12590 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 0 ≤ (𝑃 − 1)) | 
| 83 | 52 | ltm1d 12200 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 − 1) < 𝑃) | 
| 84 |  | modid 13936 | . . . . . . 7
⊢ ((((𝑃 − 1) ∈ ℝ ∧
𝑃 ∈
ℝ+) ∧ (0 ≤ (𝑃 − 1) ∧ (𝑃 − 1) < 𝑃)) → ((𝑃 − 1) mod 𝑃) = (𝑃 − 1)) | 
| 85 | 79, 41, 82, 83, 84 | syl22anc 839 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑃 − 1) mod 𝑃) = (𝑃 − 1)) | 
| 86 | 73, 77, 85 | 3eqtr3d 2785 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (-1 mod 𝑃) = (𝑃 − 1)) | 
| 87 | 51, 86 | eqeq12d 2753 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑁 mod 𝑃) = (-1 mod 𝑃) ↔ 𝑁 = (𝑃 − 1))) | 
| 88 |  | subneg 11558 | . . . . . 6
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑁 −
-1) = (𝑁 +
1)) | 
| 89 | 9, 10, 88 | sylancl 586 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 − -1) = (𝑁 + 1)) | 
| 90 | 89 | breq2d 5155 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ (𝑁 − -1) ↔ 𝑃 ∥ (𝑁 + 1))) | 
| 91 | 63, 87, 90 | 3bitr3rd 310 | . . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 ∥ (𝑁 + 1) ↔ 𝑁 = (𝑃 − 1))) | 
| 92 | 60, 91 | orbi12d 919 | . 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((𝑃 ∥ (𝑁 − 1) ∨ 𝑃 ∥ (𝑁 + 1)) ↔ (𝑁 = 1 ∨ 𝑁 = (𝑃 − 1)))) | 
| 93 | 33, 92 | bitrd 279 | 1
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 = ((𝑁↑(𝑃 − 2)) mod 𝑃) ↔ (𝑁 = 1 ∨ 𝑁 = (𝑃 − 1)))) |