Proof of Theorem prmdiv
Step | Hyp | Ref
| Expression |
1 | | nprmdvds1 16049 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → ¬
𝑃 ∥
1) |
2 | 1 | 3ad2ant1 1129 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ¬ 𝑃 ∥ 1) |
3 | | prmz 16018 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
4 | 3 | 3ad2ant1 1129 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∈ ℤ) |
5 | | prmnn 16017 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
6 | 5 | 3ad2ant1 1129 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∈ ℕ) |
7 | | simp2 1133 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝐴 ∈ ℤ) |
8 | | gcdcom 15861 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝐴 gcd 𝑃) = (𝑃 gcd 𝐴)) |
9 | 7, 4, 8 | syl2anc 586 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 gcd 𝑃) = (𝑃 gcd 𝐴)) |
10 | | coprm 16054 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (¬
𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1)) |
11 | 10 | biimp3a 1465 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 gcd 𝐴) = 1) |
12 | 9, 11 | eqtrd 2856 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 gcd 𝑃) = 1) |
13 | | eulerth 16119 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
14 | 6, 7, 12, 13 | syl3anc 1367 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
15 | | phiprm 16113 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ →
(ϕ‘𝑃) = (𝑃 − 1)) |
16 | 15 | 3ad2ant1 1129 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (ϕ‘𝑃) = (𝑃 − 1)) |
17 | | nnm1nn0 11937 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
18 | 6, 17 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 − 1) ∈
ℕ0) |
19 | 16, 18 | eqeltrd 2913 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (ϕ‘𝑃) ∈
ℕ0) |
20 | | zexpcl 13443 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧
(ϕ‘𝑃) ∈
ℕ0) → (𝐴↑(ϕ‘𝑃)) ∈ ℤ) |
21 | 7, 19, 20 | syl2anc 586 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) ∈ ℤ) |
22 | | 1zzd 12012 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 1 ∈ ℤ) |
23 | | moddvds 15617 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℕ ∧ (𝐴↑(ϕ‘𝑃)) ∈ ℤ ∧ 1 ∈
ℤ) → (((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1))) |
24 | 6, 21, 22, 23 | syl3anc 1367 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1))) |
25 | 14, 24 | mpbid 234 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1)) |
26 | | prmuz2 16039 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
27 | 26 | 3ad2ant1 1129 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∈
(ℤ≥‘2)) |
28 | | uznn0sub 12276 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑃 − 2) ∈
ℕ0) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 − 2) ∈
ℕ0) |
30 | | zexpcl 13443 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ (𝑃 − 2) ∈
ℕ0) → (𝐴↑(𝑃 − 2)) ∈
ℤ) |
31 | 7, 29, 30 | syl2anc 586 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(𝑃 − 2)) ∈
ℤ) |
32 | 31 | zred 12086 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(𝑃 − 2)) ∈
ℝ) |
33 | 32, 6 | nndivred 11690 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(𝑃 − 2)) / 𝑃) ∈ ℝ) |
34 | 33 | flcld 13167 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)) ∈ ℤ) |
35 | 7, 34 | zmulcld 12092 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))) ∈ ℤ) |
36 | | dvdsmul1 15630 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℤ ∧ (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))) ∈ ℤ) → 𝑃 ∥ (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) |
37 | 4, 35, 36 | syl2anc 586 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∥ (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) |
38 | | 1z 12011 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
39 | | zsubcl 12023 |
. . . . . . . . . 10
⊢ (((𝐴↑(ϕ‘𝑃)) ∈ ℤ ∧ 1 ∈
ℤ) → ((𝐴↑(ϕ‘𝑃)) − 1) ∈
ℤ) |
40 | 21, 38, 39 | sylancl 588 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − 1) ∈
ℤ) |
41 | 4, 35 | zmulcld 12092 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))) ∈ ℤ) |
42 | 4, 25, 37, 40, 41 | dvds2subd 15644 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∥ (((𝐴↑(ϕ‘𝑃)) − 1) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
43 | 7 | zcnd 12087 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝐴 ∈ ℂ) |
44 | 31 | zcnd 12087 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(𝑃 − 2)) ∈
ℂ) |
45 | 4, 34 | zmulcld 12092 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))) ∈ ℤ) |
46 | 45 | zcnd 12087 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))) ∈ ℂ) |
47 | 43, 44, 46 | subdid 11095 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 · ((𝐴↑(𝑃 − 2)) − (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) = ((𝐴 · (𝐴↑(𝑃 − 2))) − (𝐴 · (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
48 | | prmdiv.1 |
. . . . . . . . . . . . 13
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃) |
49 | 6 | nnrpd 12428 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∈
ℝ+) |
50 | | modval 13238 |
. . . . . . . . . . . . . 14
⊢ (((𝐴↑(𝑃 − 2)) ∈ ℝ ∧ 𝑃 ∈ ℝ+)
→ ((𝐴↑(𝑃 − 2)) mod 𝑃) = ((𝐴↑(𝑃 − 2)) − (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) |
51 | 32, 49, 50 | syl2anc 586 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(𝑃 − 2)) mod 𝑃) = ((𝐴↑(𝑃 − 2)) − (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) |
52 | 48, 51 | syl5eq 2868 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑅 = ((𝐴↑(𝑃 − 2)) − (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) |
53 | 52 | oveq2d 7171 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 · 𝑅) = (𝐴 · ((𝐴↑(𝑃 − 2)) − (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
54 | | 2m1e1 11762 |
. . . . . . . . . . . . . . . . 17
⊢ (2
− 1) = 1 |
55 | 54 | oveq2i 7166 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 − (2 − 1)) = (𝑃 − 1) |
56 | 16, 55 | syl6eqr 2874 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (ϕ‘𝑃) = (𝑃 − (2 − 1))) |
57 | 6 | nncnd 11653 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∈ ℂ) |
58 | | 2cnd 11714 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 2 ∈ ℂ) |
59 | | 1cnd 10635 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 1 ∈ ℂ) |
60 | 57, 58, 59 | subsubd 11024 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 − (2 − 1)) = ((𝑃 − 2) +
1)) |
61 | 56, 60 | eqtrd 2856 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (ϕ‘𝑃) = ((𝑃 − 2) + 1)) |
62 | 61 | oveq2d 7171 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) = (𝐴↑((𝑃 − 2) + 1))) |
63 | 43, 29 | expp1d 13510 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑((𝑃 − 2) + 1)) = ((𝐴↑(𝑃 − 2)) · 𝐴)) |
64 | 44, 43 | mulcomd 10661 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(𝑃 − 2)) · 𝐴) = (𝐴 · (𝐴↑(𝑃 − 2)))) |
65 | 62, 63, 64 | 3eqtrd 2860 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) = (𝐴 · (𝐴↑(𝑃 − 2)))) |
66 | 34 | zcnd 12087 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)) ∈ ℂ) |
67 | 57, 43, 66 | mul12d 10848 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))) = (𝐴 · (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) |
68 | 65, 67 | oveq12d 7173 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) = ((𝐴 · (𝐴↑(𝑃 − 2))) − (𝐴 · (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
69 | 47, 53, 68 | 3eqtr4d 2866 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 · 𝑅) = ((𝐴↑(ϕ‘𝑃)) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
70 | 69 | oveq1d 7170 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴 · 𝑅) − 1) = (((𝐴↑(ϕ‘𝑃)) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) − 1)) |
71 | 21 | zcnd 12087 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) ∈ ℂ) |
72 | 41 | zcnd 12087 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))) ∈ ℂ) |
73 | 71, 72, 59 | sub32d 11028 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (((𝐴↑(ϕ‘𝑃)) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) − 1) = (((𝐴↑(ϕ‘𝑃)) − 1) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
74 | 70, 73 | eqtrd 2856 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴 · 𝑅) − 1) = (((𝐴↑(ϕ‘𝑃)) − 1) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
75 | 42, 74 | breqtrrd 5093 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∥ ((𝐴 · 𝑅) − 1)) |
76 | | oveq2 7163 |
. . . . . . . . 9
⊢ (𝑅 = 0 → (𝐴 · 𝑅) = (𝐴 · 0)) |
77 | 76 | oveq1d 7170 |
. . . . . . . 8
⊢ (𝑅 = 0 → ((𝐴 · 𝑅) − 1) = ((𝐴 · 0) − 1)) |
78 | 77 | breq2d 5077 |
. . . . . . 7
⊢ (𝑅 = 0 → (𝑃 ∥ ((𝐴 · 𝑅) − 1) ↔ 𝑃 ∥ ((𝐴 · 0) − 1))) |
79 | 75, 78 | syl5ibcom 247 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑅 = 0 → 𝑃 ∥ ((𝐴 · 0) − 1))) |
80 | 43 | mul01d 10838 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 · 0) = 0) |
81 | 80 | oveq1d 7170 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴 · 0) − 1) = (0 −
1)) |
82 | | df-neg 10872 |
. . . . . . . . 9
⊢ -1 = (0
− 1) |
83 | 81, 82 | syl6eqr 2874 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴 · 0) − 1) =
-1) |
84 | 83 | breq2d 5077 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴 · 0) − 1) ↔ 𝑃 ∥ -1)) |
85 | | dvdsnegb 15626 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧ 1 ∈
ℤ) → (𝑃 ∥
1 ↔ 𝑃 ∥
-1)) |
86 | 4, 38, 85 | sylancl 588 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 ∥ 1 ↔ 𝑃 ∥ -1)) |
87 | 84, 86 | bitr4d 284 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴 · 0) − 1) ↔ 𝑃 ∥ 1)) |
88 | 79, 87 | sylibd 241 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑅 = 0 → 𝑃 ∥ 1)) |
89 | 2, 88 | mtod 200 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ¬ 𝑅 = 0) |
90 | | zmodfz 13260 |
. . . . . . . 8
⊢ (((𝐴↑(𝑃 − 2)) ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝐴↑(𝑃 − 2)) mod 𝑃) ∈ (0...(𝑃 − 1))) |
91 | 31, 6, 90 | syl2anc 586 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(𝑃 − 2)) mod 𝑃) ∈ (0...(𝑃 − 1))) |
92 | 48, 91 | eqeltrid 2917 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑅 ∈ (0...(𝑃 − 1))) |
93 | | nn0uz 12279 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) |
94 | 18, 93 | eleqtrdi 2923 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 − 1) ∈
(ℤ≥‘0)) |
95 | | elfzp12 12985 |
. . . . . . 7
⊢ ((𝑃 − 1) ∈
(ℤ≥‘0) → (𝑅 ∈ (0...(𝑃 − 1)) ↔ (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1))))) |
96 | 94, 95 | syl 17 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑅 ∈ (0...(𝑃 − 1)) ↔ (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1))))) |
97 | 92, 96 | mpbid 234 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1)))) |
98 | 97 | ord 860 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (¬ 𝑅 = 0 → 𝑅 ∈ ((0 + 1)...(𝑃 − 1)))) |
99 | 89, 98 | mpd 15 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑅 ∈ ((0 + 1)...(𝑃 − 1))) |
100 | | 1e0p1 12139 |
. . . 4
⊢ 1 = (0 +
1) |
101 | 100 | oveq1i 7165 |
. . 3
⊢
(1...(𝑃 − 1))
= ((0 + 1)...(𝑃 −
1)) |
102 | 99, 101 | eleqtrrdi 2924 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑅 ∈ (1...(𝑃 − 1))) |
103 | 102, 75 | jca 514 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑅 ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑅) − 1))) |