Proof of Theorem prmdiveq
Step | Hyp | Ref
| Expression |
1 | | simpl1 985 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑃 ∈ ℙ) |
2 | | prmz 11992 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
3 | 1, 2 | syl 14 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑃 ∈ ℤ) |
4 | | simpl2 986 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝐴 ∈ ℤ) |
5 | | elfzelz 9929 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (0...(𝑃 − 1)) → 𝑆 ∈ ℤ) |
6 | 5 | ad2antrl 482 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑆 ∈ ℤ) |
7 | 4, 6 | zmulcld 9293 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝐴 · 𝑆) ∈ ℤ) |
8 | | 1z 9194 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
9 | | zsubcl 9209 |
. . . . . . . . 9
⊢ (((𝐴 · 𝑆) ∈ ℤ ∧ 1 ∈ ℤ)
→ ((𝐴 · 𝑆) − 1) ∈
ℤ) |
10 | 7, 8, 9 | sylancl 410 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → ((𝐴 · 𝑆) − 1) ∈
ℤ) |
11 | | prmdiv.1 |
. . . . . . . . . . . . . 14
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃) |
12 | 11 | prmdiv 12114 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑅 ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑅) − 1))) |
13 | 12 | adantr 274 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝑅 ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑅) − 1))) |
14 | 13 | simpld 111 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑅 ∈ (1...(𝑃 − 1))) |
15 | | elfzelz 9929 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ (1...(𝑃 − 1)) → 𝑅 ∈ ℤ) |
16 | 14, 15 | syl 14 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑅 ∈ ℤ) |
17 | 4, 16 | zmulcld 9293 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝐴 · 𝑅) ∈ ℤ) |
18 | | zsubcl 9209 |
. . . . . . . . 9
⊢ (((𝐴 · 𝑅) ∈ ℤ ∧ 1 ∈ ℤ)
→ ((𝐴 · 𝑅) − 1) ∈
ℤ) |
19 | 17, 8, 18 | sylancl 410 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → ((𝐴 · 𝑅) − 1) ∈
ℤ) |
20 | | simprr 522 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑃 ∥ ((𝐴 · 𝑆) − 1)) |
21 | 13 | simprd 113 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑃 ∥ ((𝐴 · 𝑅) − 1)) |
22 | 3, 10, 19, 20, 21 | dvds2subd 11727 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑃 ∥ (((𝐴 · 𝑆) − 1) − ((𝐴 · 𝑅) − 1))) |
23 | 7 | zcnd 9288 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝐴 · 𝑆) ∈ ℂ) |
24 | 17 | zcnd 9288 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝐴 · 𝑅) ∈ ℂ) |
25 | | 1cnd 7895 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 1 ∈
ℂ) |
26 | 23, 24, 25 | nnncan2d 8222 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (((𝐴 · 𝑆) − 1) − ((𝐴 · 𝑅) − 1)) = ((𝐴 · 𝑆) − (𝐴 · 𝑅))) |
27 | 4 | zcnd 9288 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝐴 ∈ ℂ) |
28 | | elfznn0 10017 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (0...(𝑃 − 1)) → 𝑆 ∈
ℕ0) |
29 | 28 | ad2antrl 482 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑆 ∈
ℕ0) |
30 | 29 | nn0cnd 9146 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑆 ∈ ℂ) |
31 | 16 | zcnd 9288 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑅 ∈ ℂ) |
32 | 27, 30, 31 | subdid 8290 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝐴 · (𝑆 − 𝑅)) = ((𝐴 · 𝑆) − (𝐴 · 𝑅))) |
33 | 26, 32 | eqtr4d 2193 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (((𝐴 · 𝑆) − 1) − ((𝐴 · 𝑅) − 1)) = (𝐴 · (𝑆 − 𝑅))) |
34 | 22, 33 | breqtrd 3991 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑃 ∥ (𝐴 · (𝑆 − 𝑅))) |
35 | | simpl3 987 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → ¬ 𝑃 ∥ 𝐴) |
36 | | coprm 12023 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (¬
𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1)) |
37 | 1, 4, 36 | syl2anc 409 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (¬ 𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1)) |
38 | 35, 37 | mpbid 146 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝑃 gcd 𝐴) = 1) |
39 | 6, 16 | zsubcld 9292 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝑆 − 𝑅) ∈ ℤ) |
40 | | coprmdvds 11973 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ (𝑆 − 𝑅) ∈ ℤ) → ((𝑃 ∥ (𝐴 · (𝑆 − 𝑅)) ∧ (𝑃 gcd 𝐴) = 1) → 𝑃 ∥ (𝑆 − 𝑅))) |
41 | 3, 4, 39, 40 | syl3anc 1220 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → ((𝑃 ∥ (𝐴 · (𝑆 − 𝑅)) ∧ (𝑃 gcd 𝐴) = 1) → 𝑃 ∥ (𝑆 − 𝑅))) |
42 | 34, 38, 41 | mp2and 430 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑃 ∥ (𝑆 − 𝑅)) |
43 | | prmnn 11991 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
44 | 1, 43 | syl 14 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑃 ∈ ℕ) |
45 | | moddvds 11699 |
. . . . . 6
⊢ ((𝑃 ∈ ℕ ∧ 𝑆 ∈ ℤ ∧ 𝑅 ∈ ℤ) → ((𝑆 mod 𝑃) = (𝑅 mod 𝑃) ↔ 𝑃 ∥ (𝑆 − 𝑅))) |
46 | 44, 6, 16, 45 | syl3anc 1220 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → ((𝑆 mod 𝑃) = (𝑅 mod 𝑃) ↔ 𝑃 ∥ (𝑆 − 𝑅))) |
47 | 42, 46 | mpbird 166 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝑆 mod 𝑃) = (𝑅 mod 𝑃)) |
48 | | zq 9536 |
. . . . . 6
⊢ (𝑆 ∈ ℤ → 𝑆 ∈
ℚ) |
49 | 6, 48 | syl 14 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑆 ∈ ℚ) |
50 | | nnq 9543 |
. . . . . 6
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℚ) |
51 | 44, 50 | syl 14 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑃 ∈ ℚ) |
52 | | elfzle1 9930 |
. . . . . 6
⊢ (𝑆 ∈ (0...(𝑃 − 1)) → 0 ≤ 𝑆) |
53 | 52 | ad2antrl 482 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 0 ≤ 𝑆) |
54 | | elfzle2 9931 |
. . . . . . 7
⊢ (𝑆 ∈ (0...(𝑃 − 1)) → 𝑆 ≤ (𝑃 − 1)) |
55 | 54 | ad2antrl 482 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑆 ≤ (𝑃 − 1)) |
56 | | zltlem1 9225 |
. . . . . . 7
⊢ ((𝑆 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑆 < 𝑃 ↔ 𝑆 ≤ (𝑃 − 1))) |
57 | 6, 3, 56 | syl2anc 409 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝑆 < 𝑃 ↔ 𝑆 ≤ (𝑃 − 1))) |
58 | 55, 57 | mpbird 166 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑆 < 𝑃) |
59 | | modqid 10252 |
. . . . 5
⊢ (((𝑆 ∈ ℚ ∧ 𝑃 ∈ ℚ) ∧ (0 ≤
𝑆 ∧ 𝑆 < 𝑃)) → (𝑆 mod 𝑃) = 𝑆) |
60 | 49, 51, 53, 58, 59 | syl22anc 1221 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝑆 mod 𝑃) = 𝑆) |
61 | | prmuz2 12012 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
62 | | uznn0sub 9471 |
. . . . . . . . 9
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑃 − 2) ∈
ℕ0) |
63 | 1, 61, 62 | 3syl 17 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝑃 − 2) ∈
ℕ0) |
64 | | zexpcl 10438 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (𝑃 − 2) ∈
ℕ0) → (𝐴↑(𝑃 − 2)) ∈
ℤ) |
65 | 4, 63, 64 | syl2anc 409 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝐴↑(𝑃 − 2)) ∈
ℤ) |
66 | | zq 9536 |
. . . . . . 7
⊢ ((𝐴↑(𝑃 − 2)) ∈ ℤ → (𝐴↑(𝑃 − 2)) ∈
ℚ) |
67 | 65, 66 | syl 14 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝐴↑(𝑃 − 2)) ∈
ℚ) |
68 | 44 | nngt0d 8878 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 0 < 𝑃) |
69 | | modqabs2 10261 |
. . . . . 6
⊢ (((𝐴↑(𝑃 − 2)) ∈ ℚ ∧ 𝑃 ∈ ℚ ∧ 0 <
𝑃) → (((𝐴↑(𝑃 − 2)) mod 𝑃) mod 𝑃) = ((𝐴↑(𝑃 − 2)) mod 𝑃)) |
70 | 67, 51, 68, 69 | syl3anc 1220 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (((𝐴↑(𝑃 − 2)) mod 𝑃) mod 𝑃) = ((𝐴↑(𝑃 − 2)) mod 𝑃)) |
71 | 11 | oveq1i 5835 |
. . . . 5
⊢ (𝑅 mod 𝑃) = (((𝐴↑(𝑃 − 2)) mod 𝑃) mod 𝑃) |
72 | 70, 71, 11 | 3eqtr4g 2215 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝑅 mod 𝑃) = 𝑅) |
73 | 47, 60, 72 | 3eqtr3d 2198 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑆 = 𝑅) |
74 | 73 | ex 114 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1)) → 𝑆 = 𝑅)) |
75 | | fz1ssfz0 10020 |
. . . . . 6
⊢
(1...(𝑃 − 1))
⊆ (0...(𝑃 −
1)) |
76 | 75 | sseli 3124 |
. . . . 5
⊢ (𝑅 ∈ (1...(𝑃 − 1)) → 𝑅 ∈ (0...(𝑃 − 1))) |
77 | | eleq1 2220 |
. . . . 5
⊢ (𝑆 = 𝑅 → (𝑆 ∈ (0...(𝑃 − 1)) ↔ 𝑅 ∈ (0...(𝑃 − 1)))) |
78 | 76, 77 | syl5ibr 155 |
. . . 4
⊢ (𝑆 = 𝑅 → (𝑅 ∈ (1...(𝑃 − 1)) → 𝑆 ∈ (0...(𝑃 − 1)))) |
79 | | oveq2 5833 |
. . . . . . 7
⊢ (𝑆 = 𝑅 → (𝐴 · 𝑆) = (𝐴 · 𝑅)) |
80 | 79 | oveq1d 5840 |
. . . . . 6
⊢ (𝑆 = 𝑅 → ((𝐴 · 𝑆) − 1) = ((𝐴 · 𝑅) − 1)) |
81 | 80 | breq2d 3978 |
. . . . 5
⊢ (𝑆 = 𝑅 → (𝑃 ∥ ((𝐴 · 𝑆) − 1) ↔ 𝑃 ∥ ((𝐴 · 𝑅) − 1))) |
82 | 81 | biimprd 157 |
. . . 4
⊢ (𝑆 = 𝑅 → (𝑃 ∥ ((𝐴 · 𝑅) − 1) → 𝑃 ∥ ((𝐴 · 𝑆) − 1))) |
83 | 78, 82 | anim12d 333 |
. . 3
⊢ (𝑆 = 𝑅 → ((𝑅 ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑅) − 1)) → (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1)))) |
84 | 12, 83 | syl5com 29 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑆 = 𝑅 → (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1)))) |
85 | 74, 84 | impbid 128 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1)) ↔ 𝑆 = 𝑅)) |