Proof of Theorem prmdiv
Step | Hyp | Ref
| Expression |
1 | | nprmdvds1 15256 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → ¬
𝑃 ∥
1) |
2 | 1 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ¬ 𝑃 ∥ 1) |
3 | | prmnn 15226 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
4 | 3 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∈ ℕ) |
5 | | simp2 1055 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝐴 ∈ ℤ) |
6 | | prmz 15227 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
7 | 6 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∈ ℤ) |
8 | | gcdcom 15073 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝐴 gcd 𝑃) = (𝑃 gcd 𝐴)) |
9 | 5, 7, 8 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 gcd 𝑃) = (𝑃 gcd 𝐴)) |
10 | | coprm 15261 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (¬
𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1)) |
11 | 10 | biimp3a 1424 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 gcd 𝐴) = 1) |
12 | 9, 11 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 gcd 𝑃) = 1) |
13 | | eulerth 15326 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
14 | 4, 5, 12, 13 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
15 | | phiprm 15320 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ →
(ϕ‘𝑃) = (𝑃 − 1)) |
16 | 15 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (ϕ‘𝑃) = (𝑃 − 1)) |
17 | | nnm1nn0 11211 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
18 | 4, 17 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 − 1) ∈
ℕ0) |
19 | 16, 18 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (ϕ‘𝑃) ∈
ℕ0) |
20 | | zexpcl 12737 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧
(ϕ‘𝑃) ∈
ℕ0) → (𝐴↑(ϕ‘𝑃)) ∈ ℤ) |
21 | 5, 19, 20 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) ∈ ℤ) |
22 | | 1zzd 11285 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 1 ∈ ℤ) |
23 | | moddvds 14829 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℕ ∧ (𝐴↑(ϕ‘𝑃)) ∈ ℤ ∧ 1 ∈
ℤ) → (((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1))) |
24 | 4, 21, 22, 23 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1))) |
25 | 14, 24 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1)) |
26 | | prmuz2 15246 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
27 | 26 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∈
(ℤ≥‘2)) |
28 | | uznn0sub 11595 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑃 − 2) ∈
ℕ0) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 − 2) ∈
ℕ0) |
30 | | zexpcl 12737 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ (𝑃 − 2) ∈
ℕ0) → (𝐴↑(𝑃 − 2)) ∈
ℤ) |
31 | 5, 29, 30 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(𝑃 − 2)) ∈
ℤ) |
32 | 31 | zred 11358 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(𝑃 − 2)) ∈
ℝ) |
33 | 32, 4 | nndivred 10946 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(𝑃 − 2)) / 𝑃) ∈ ℝ) |
34 | 33 | flcld 12461 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)) ∈ ℤ) |
35 | 5, 34 | zmulcld 11364 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))) ∈ ℤ) |
36 | | dvdsmul1 14841 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℤ ∧ (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))) ∈ ℤ) → 𝑃 ∥ (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) |
37 | 7, 35, 36 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∥ (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) |
38 | | 1z 11284 |
. . . . . . . . . . 11
⊢ 1 ∈
ℤ |
39 | | zsubcl 11296 |
. . . . . . . . . . 11
⊢ (((𝐴↑(ϕ‘𝑃)) ∈ ℤ ∧ 1 ∈
ℤ) → ((𝐴↑(ϕ‘𝑃)) − 1) ∈
ℤ) |
40 | 21, 38, 39 | sylancl 693 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − 1) ∈
ℤ) |
41 | 7, 35 | zmulcld 11364 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))) ∈ ℤ) |
42 | | dvds2sub 14854 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℤ ∧ ((𝐴↑(ϕ‘𝑃)) − 1) ∈ ℤ
∧ (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))) ∈ ℤ) → ((𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1) ∧ 𝑃 ∥ (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) → 𝑃 ∥ (((𝐴↑(ϕ‘𝑃)) − 1) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))))) |
43 | 7, 40, 41, 42 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1) ∧ 𝑃 ∥ (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) → 𝑃 ∥ (((𝐴↑(ϕ‘𝑃)) − 1) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))))) |
44 | 25, 37, 43 | mp2and 711 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∥ (((𝐴↑(ϕ‘𝑃)) − 1) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
45 | 5 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝐴 ∈ ℂ) |
46 | 31 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(𝑃 − 2)) ∈
ℂ) |
47 | 7, 34 | zmulcld 11364 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))) ∈ ℤ) |
48 | 47 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))) ∈ ℂ) |
49 | 45, 46, 48 | subdid 10365 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 · ((𝐴↑(𝑃 − 2)) − (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) = ((𝐴 · (𝐴↑(𝑃 − 2))) − (𝐴 · (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
50 | | prmdiv.1 |
. . . . . . . . . . . . 13
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃) |
51 | 4 | nnrpd 11746 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∈
ℝ+) |
52 | | modval 12532 |
. . . . . . . . . . . . . 14
⊢ (((𝐴↑(𝑃 − 2)) ∈ ℝ ∧ 𝑃 ∈ ℝ+)
→ ((𝐴↑(𝑃 − 2)) mod 𝑃) = ((𝐴↑(𝑃 − 2)) − (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) |
53 | 32, 51, 52 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(𝑃 − 2)) mod 𝑃) = ((𝐴↑(𝑃 − 2)) − (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) |
54 | 50, 53 | syl5eq 2656 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑅 = ((𝐴↑(𝑃 − 2)) − (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) |
55 | 54 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 · 𝑅) = (𝐴 · ((𝐴↑(𝑃 − 2)) − (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
56 | | 2m1e1 11012 |
. . . . . . . . . . . . . . . . 17
⊢ (2
− 1) = 1 |
57 | 56 | oveq2i 6560 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 − (2 − 1)) = (𝑃 − 1) |
58 | 16, 57 | syl6eqr 2662 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (ϕ‘𝑃) = (𝑃 − (2 − 1))) |
59 | 4 | nncnd 10913 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∈ ℂ) |
60 | | 2cnd 10970 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 2 ∈ ℂ) |
61 | | 1cnd 9935 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 1 ∈ ℂ) |
62 | 59, 60, 61 | subsubd 10299 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 − (2 − 1)) = ((𝑃 − 2) +
1)) |
63 | 58, 62 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (ϕ‘𝑃) = ((𝑃 − 2) + 1)) |
64 | 63 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) = (𝐴↑((𝑃 − 2) + 1))) |
65 | 45, 29 | expp1d 12871 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑((𝑃 − 2) + 1)) = ((𝐴↑(𝑃 − 2)) · 𝐴)) |
66 | 46, 45 | mulcomd 9940 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(𝑃 − 2)) · 𝐴) = (𝐴 · (𝐴↑(𝑃 − 2)))) |
67 | 64, 65, 66 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) = (𝐴 · (𝐴↑(𝑃 − 2)))) |
68 | 34 | zcnd 11359 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)) ∈ ℂ) |
69 | 59, 45, 68 | mul12d 10124 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))) = (𝐴 · (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) |
70 | 67, 69 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) = ((𝐴 · (𝐴↑(𝑃 − 2))) − (𝐴 · (𝑃 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
71 | 49, 55, 70 | 3eqtr4d 2654 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 · 𝑅) = ((𝐴↑(ϕ‘𝑃)) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
72 | 71 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴 · 𝑅) − 1) = (((𝐴↑(ϕ‘𝑃)) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) − 1)) |
73 | 21 | zcnd 11359 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) ∈ ℂ) |
74 | 41 | zcnd 11359 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))) ∈ ℂ) |
75 | 73, 74, 61 | sub32d 10303 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (((𝐴↑(ϕ‘𝑃)) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃))))) − 1) = (((𝐴↑(ϕ‘𝑃)) − 1) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
76 | 72, 75 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴 · 𝑅) − 1) = (((𝐴↑(ϕ‘𝑃)) − 1) − (𝑃 · (𝐴 · (⌊‘((𝐴↑(𝑃 − 2)) / 𝑃)))))) |
77 | 44, 76 | breqtrrd 4611 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∥ ((𝐴 · 𝑅) − 1)) |
78 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑅 = 0 → (𝐴 · 𝑅) = (𝐴 · 0)) |
79 | 78 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑅 = 0 → ((𝐴 · 𝑅) − 1) = ((𝐴 · 0) − 1)) |
80 | 79 | breq2d 4595 |
. . . . . . 7
⊢ (𝑅 = 0 → (𝑃 ∥ ((𝐴 · 𝑅) − 1) ↔ 𝑃 ∥ ((𝐴 · 0) − 1))) |
81 | 77, 80 | syl5ibcom 234 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑅 = 0 → 𝑃 ∥ ((𝐴 · 0) − 1))) |
82 | 45 | mul01d 10114 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴 · 0) = 0) |
83 | 82 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴 · 0) − 1) = (0 −
1)) |
84 | | df-neg 10148 |
. . . . . . . . 9
⊢ -1 = (0
− 1) |
85 | 83, 84 | syl6eqr 2662 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴 · 0) − 1) =
-1) |
86 | 85 | breq2d 4595 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴 · 0) − 1) ↔ 𝑃 ∥ -1)) |
87 | | dvdsnegb 14837 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧ 1 ∈
ℤ) → (𝑃 ∥
1 ↔ 𝑃 ∥
-1)) |
88 | 7, 38, 87 | sylancl 693 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 ∥ 1 ↔ 𝑃 ∥ -1)) |
89 | 86, 88 | bitr4d 270 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴 · 0) − 1) ↔ 𝑃 ∥ 1)) |
90 | 81, 89 | sylibd 228 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑅 = 0 → 𝑃 ∥ 1)) |
91 | 2, 90 | mtod 188 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ¬ 𝑅 = 0) |
92 | | zmodfz 12554 |
. . . . . . . 8
⊢ (((𝐴↑(𝑃 − 2)) ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝐴↑(𝑃 − 2)) mod 𝑃) ∈ (0...(𝑃 − 1))) |
93 | 31, 4, 92 | syl2anc 691 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(𝑃 − 2)) mod 𝑃) ∈ (0...(𝑃 − 1))) |
94 | 50, 93 | syl5eqel 2692 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑅 ∈ (0...(𝑃 − 1))) |
95 | | nn0uz 11598 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) |
96 | 18, 95 | syl6eleq 2698 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 − 1) ∈
(ℤ≥‘0)) |
97 | | elfzp12 12288 |
. . . . . . 7
⊢ ((𝑃 − 1) ∈
(ℤ≥‘0) → (𝑅 ∈ (0...(𝑃 − 1)) ↔ (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1))))) |
98 | 96, 97 | syl 17 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑅 ∈ (0...(𝑃 − 1)) ↔ (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1))))) |
99 | 94, 98 | mpbid 221 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1)))) |
100 | 99 | ord 391 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (¬ 𝑅 = 0 → 𝑅 ∈ ((0 + 1)...(𝑃 − 1)))) |
101 | 91, 100 | mpd 15 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑅 ∈ ((0 + 1)...(𝑃 − 1))) |
102 | | 1e0p1 11428 |
. . . 4
⊢ 1 = (0 +
1) |
103 | 102 | oveq1i 6559 |
. . 3
⊢
(1...(𝑃 − 1))
= ((0 + 1)...(𝑃 −
1)) |
104 | 101, 103 | syl6eleqr 2699 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑅 ∈ (1...(𝑃 − 1))) |
105 | 104, 77 | jca 553 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑅 ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑅) − 1))) |