Proof of Theorem prmdiv
| Step | Hyp | Ref
| Expression |
| 1 | | nprmdvds1 16743 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → ¬
𝑃 ∥
1) |
| 2 | 1 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ¬ 𝑃 ∥ 1) |
| 3 | | prmz 16712 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
| 4 | 3 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∈ ℤ) |
| 5 | | simp2 1138 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝐴 ∈ ℤ) |
| 6 | | phiprm 16814 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ →
(ϕ‘𝑃) = (𝑃 − 1)) |
| 7 | 6 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (ϕ‘𝑃) = (𝑃 − 1)) |
| 8 | | prmnn 16711 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 9 | 8 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∈ ℕ) |
| 10 | | nnm1nn0 12567 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
| 11 | 9, 10 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 − 1) ∈
ℕ0) |
| 12 | 7, 11 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (ϕ‘𝑃) ∈
ℕ0) |
| 13 | | zexpcl 14117 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧
(ϕ‘𝑃) ∈
ℕ0) → (𝐴↑(ϕ‘𝑃)) ∈ ℤ) |
| 14 | 5, 12, 13 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) ∈ ℤ) |
| 15 | | 1z 12647 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
| 16 | | zsubcl 12659 |
. . . . . . . . . 10
⊢ (((𝐴↑(ϕ‘𝑃)) ∈ ℤ ∧ 1 ∈
ℤ) → ((𝐴↑(ϕ‘𝑃)) − 1) ∈
ℤ) |
| 17 | 14, 15, 16 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − 1) ∈
ℤ) |
| 18 | | prmuz2 16733 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
| 19 | 18 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∈
(ℤ≥‘2)) |
| 20 | | uznn0sub 12917 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑃 − 2) ∈
ℕ0) |
| 21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 − 2) ∈
ℕ0) |
| 22 | | zexpcl 14117 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ (𝑃 − 2) ∈
ℕ0) → (𝐴↑(𝑃 − 2)) ∈
ℤ) |
| 23 | 5, 21, 22 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(𝑃 − 2)) ∈
ℤ) |
| 24 | 23 | zred 12722 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(𝑃 − 2)) ∈
ℝ) |
| 25 | 24, 9 | nndivred 12320 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(𝑃 − 2)) / 𝑃) ∈ ℝ) |
| 26 | 25 | flcld 13838 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)) ∈ ℤ) |
| 27 | 5, 26 | zmulcld 12728 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))) ∈ ℤ) |
| 28 | 4, 27 | zmulcld 12728 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))) ∈ ℤ) |
| 29 | 5, 4 | gcdcomd 16551 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 gcd 𝑃) = (𝑃 gcd 𝐴)) |
| 30 | | coprm 16748 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (¬
𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1)) |
| 31 | 30 | biimp3a 1471 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 gcd 𝐴) = 1) |
| 32 | 29, 31 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 gcd 𝑃) = 1) |
| 33 | | eulerth 16820 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
| 34 | 9, 5, 32, 33 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
| 35 | | 1zzd 12648 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 1 ∈ ℤ) |
| 36 | | moddvds 16301 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℕ ∧ (𝐴↑(ϕ‘𝑃)) ∈ ℤ ∧ 1 ∈
ℤ) → (((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1))) |
| 37 | 9, 14, 35, 36 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1))) |
| 38 | 34, 37 | mpbid 232 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1)) |
| 39 | | dvdsmul1 16315 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℤ ∧ (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))) ∈ ℤ) → 𝑃 ∥ (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) |
| 40 | 4, 27, 39 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∥ (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) |
| 41 | 4, 17, 28, 38, 40 | dvds2subd 16330 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∥ (((𝐴↑(ϕ‘𝑃)) − 1) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
| 42 | 5 | zcnd 12723 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝐴 ∈ ℂ) |
| 43 | 23 | zcnd 12723 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(𝑃 − 2)) ∈
ℂ) |
| 44 | 4, 26 | zmulcld 12728 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))) ∈ ℤ) |
| 45 | 44 | zcnd 12723 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))) ∈ ℂ) |
| 46 | 42, 43, 45 | subdid 11719 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 · ((𝐴↑(𝑃 − 2)) − (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) = ((𝐴 · (𝐴↑(𝑃 − 2))) − (𝐴 · (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
| 47 | | prmdiv.1 |
. . . . . . . . . . . . 13
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃) |
| 48 | 9 | nnrpd 13075 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∈
ℝ+) |
| 49 | | modval 13911 |
. . . . . . . . . . . . . 14
⊢ (((𝐴↑(𝑃 − 2)) ∈ ℝ ∧ 𝑃 ∈ ℝ+)
→ ((𝐴↑(𝑃 − 2)) mod 𝑃) = ((𝐴↑(𝑃 − 2)) − (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) |
| 50 | 24, 48, 49 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(𝑃 − 2)) mod 𝑃) = ((𝐴↑(𝑃 − 2)) − (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) |
| 51 | 47, 50 | eqtrid 2789 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑅 = ((𝐴↑(𝑃 − 2)) − (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) |
| 52 | 51 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 · 𝑅) = (𝐴 · ((𝐴↑(𝑃 − 2)) − (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
| 53 | | 2m1e1 12392 |
. . . . . . . . . . . . . . . . 17
⊢ (2
− 1) = 1 |
| 54 | 53 | oveq2i 7442 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 − (2 − 1)) = (𝑃 − 1) |
| 55 | 7, 54 | eqtr4di 2795 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (ϕ‘𝑃) = (𝑃 − (2 − 1))) |
| 56 | 9 | nncnd 12282 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∈ ℂ) |
| 57 | | 2cnd 12344 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 2 ∈ ℂ) |
| 58 | | 1cnd 11256 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 1 ∈ ℂ) |
| 59 | 56, 57, 58 | subsubd 11648 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 − (2 − 1)) = ((𝑃 − 2) +
1)) |
| 60 | 55, 59 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (ϕ‘𝑃) = ((𝑃 − 2) + 1)) |
| 61 | 60 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) = (𝐴↑((𝑃 − 2) + 1))) |
| 62 | 42, 21 | expp1d 14187 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑((𝑃 − 2) + 1)) = ((𝐴↑(𝑃 − 2)) · 𝐴)) |
| 63 | 43, 42 | mulcomd 11282 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(𝑃 − 2)) · 𝐴) = (𝐴 · (𝐴↑(𝑃 − 2)))) |
| 64 | 61, 62, 63 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) = (𝐴 · (𝐴↑(𝑃 − 2)))) |
| 65 | 26 | zcnd 12723 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)) ∈ ℂ) |
| 66 | 56, 42, 65 | mul12d 11470 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))) = (𝐴 · (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) |
| 67 | 64, 66 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) = ((𝐴 · (𝐴↑(𝑃 − 2))) − (𝐴 · (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
| 68 | 46, 52, 67 | 3eqtr4d 2787 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 · 𝑅) = ((𝐴↑(ϕ‘𝑃)) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
| 69 | 68 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴 · 𝑅) − 1) = (((𝐴↑(ϕ‘𝑃)) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) − 1)) |
| 70 | 14 | zcnd 12723 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) ∈ ℂ) |
| 71 | 28 | zcnd 12723 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))) ∈ ℂ) |
| 72 | 70, 71, 58 | sub32d 11652 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (((𝐴↑(ϕ‘𝑃)) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) − 1) = (((𝐴↑(ϕ‘𝑃)) − 1) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
| 73 | 69, 72 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴 · 𝑅) − 1) = (((𝐴↑(ϕ‘𝑃)) − 1) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
| 74 | 41, 73 | breqtrrd 5171 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∥ ((𝐴 · 𝑅) − 1)) |
| 75 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑅 = 0 → (𝐴 · 𝑅) = (𝐴 · 0)) |
| 76 | 75 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑅 = 0 → ((𝐴 · 𝑅) − 1) = ((𝐴 · 0) − 1)) |
| 77 | 76 | breq2d 5155 |
. . . . . . 7
⊢ (𝑅 = 0 → (𝑃 ∥ ((𝐴 · 𝑅) − 1) ↔ 𝑃 ∥ ((𝐴 · 0) − 1))) |
| 78 | 74, 77 | syl5ibcom 245 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑅 = 0 → 𝑃 ∥ ((𝐴 · 0) − 1))) |
| 79 | 42 | mul01d 11460 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 · 0) = 0) |
| 80 | 79 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴 · 0) − 1) = (0 −
1)) |
| 81 | | df-neg 11495 |
. . . . . . . . 9
⊢ -1 = (0
− 1) |
| 82 | 80, 81 | eqtr4di 2795 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴 · 0) − 1) =
-1) |
| 83 | 82 | breq2d 5155 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴 · 0) − 1) ↔ 𝑃 ∥ -1)) |
| 84 | | dvdsnegb 16311 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧ 1 ∈
ℤ) → (𝑃 ∥
1 ↔ 𝑃 ∥
-1)) |
| 85 | 4, 15, 84 | sylancl 586 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 ∥ 1 ↔ 𝑃 ∥ -1)) |
| 86 | 83, 85 | bitr4d 282 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴 · 0) − 1) ↔ 𝑃 ∥ 1)) |
| 87 | 78, 86 | sylibd 239 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑅 = 0 → 𝑃 ∥ 1)) |
| 88 | 2, 87 | mtod 198 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ¬ 𝑅 = 0) |
| 89 | | zmodfz 13933 |
. . . . . . . 8
⊢ (((𝐴↑(𝑃 − 2)) ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝐴↑(𝑃 − 2)) mod 𝑃) ∈ (0...(𝑃 − 1))) |
| 90 | 23, 9, 89 | syl2anc 584 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(𝑃 − 2)) mod 𝑃) ∈ (0...(𝑃 − 1))) |
| 91 | 47, 90 | eqeltrid 2845 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑅 ∈ (0...(𝑃 − 1))) |
| 92 | | nn0uz 12920 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) |
| 93 | 11, 92 | eleqtrdi 2851 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 − 1) ∈
(ℤ≥‘0)) |
| 94 | | elfzp12 13643 |
. . . . . . 7
⊢ ((𝑃 − 1) ∈
(ℤ≥‘0) → (𝑅 ∈ (0...(𝑃 − 1)) ↔ (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1))))) |
| 95 | 93, 94 | syl 17 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑅 ∈ (0...(𝑃 − 1)) ↔ (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1))))) |
| 96 | 91, 95 | mpbid 232 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1)))) |
| 97 | 96 | ord 865 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (¬ 𝑅 = 0 → 𝑅 ∈ ((0 + 1)...(𝑃 − 1)))) |
| 98 | 88, 97 | mpd 15 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑅 ∈ ((0 + 1)...(𝑃 − 1))) |
| 99 | | 1e0p1 12775 |
. . . 4
⊢ 1 = (0 +
1) |
| 100 | 99 | oveq1i 7441 |
. . 3
⊢
(1...(𝑃 − 1))
= ((0 + 1)...(𝑃 −
1)) |
| 101 | 98, 100 | eleqtrrdi 2852 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑅 ∈ (1...(𝑃 − 1))) |
| 102 | 101, 74 | jca 511 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑅 ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑅) − 1))) |