Proof of Theorem prmdiveq
Step | Hyp | Ref
| Expression |
1 | | simprr 792 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑃 ∥ ((𝐴 · 𝑆) − 1)) |
2 | | prmdiv.1 |
. . . . . . . . . . 11
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃) |
3 | 2 | prmdiv 15328 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑅 ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑅) − 1))) |
4 | 3 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝑅 ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑅) − 1))) |
5 | 4 | simprd 478 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑃 ∥ ((𝐴 · 𝑅) − 1)) |
6 | | simpl1 1057 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑃 ∈ ℙ) |
7 | | prmz 15227 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
8 | 6, 7 | syl 17 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑃 ∈ ℤ) |
9 | | simpl2 1058 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝐴 ∈ ℤ) |
10 | | elfzelz 12213 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ (0...(𝑃 − 1)) → 𝑆 ∈ ℤ) |
11 | 10 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑆 ∈ ℤ) |
12 | 9, 11 | zmulcld 11364 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝐴 · 𝑆) ∈ ℤ) |
13 | | 1z 11284 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
14 | | zsubcl 11296 |
. . . . . . . . . 10
⊢ (((𝐴 · 𝑆) ∈ ℤ ∧ 1 ∈ ℤ)
→ ((𝐴 · 𝑆) − 1) ∈
ℤ) |
15 | 12, 13, 14 | sylancl 693 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → ((𝐴 · 𝑆) − 1) ∈
ℤ) |
16 | 4 | simpld 474 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑅 ∈ (1...(𝑃 − 1))) |
17 | | elfzelz 12213 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ (1...(𝑃 − 1)) → 𝑅 ∈ ℤ) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑅 ∈ ℤ) |
19 | 9, 18 | zmulcld 11364 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝐴 · 𝑅) ∈ ℤ) |
20 | | zsubcl 11296 |
. . . . . . . . . 10
⊢ (((𝐴 · 𝑅) ∈ ℤ ∧ 1 ∈ ℤ)
→ ((𝐴 · 𝑅) − 1) ∈
ℤ) |
21 | 19, 13, 20 | sylancl 693 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → ((𝐴 · 𝑅) − 1) ∈
ℤ) |
22 | | dvds2sub 14854 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℤ ∧ ((𝐴 · 𝑆) − 1) ∈ ℤ ∧ ((𝐴 · 𝑅) − 1) ∈ ℤ) → ((𝑃 ∥ ((𝐴 · 𝑆) − 1) ∧ 𝑃 ∥ ((𝐴 · 𝑅) − 1)) → 𝑃 ∥ (((𝐴 · 𝑆) − 1) − ((𝐴 · 𝑅) − 1)))) |
23 | 8, 15, 21, 22 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → ((𝑃 ∥ ((𝐴 · 𝑆) − 1) ∧ 𝑃 ∥ ((𝐴 · 𝑅) − 1)) → 𝑃 ∥ (((𝐴 · 𝑆) − 1) − ((𝐴 · 𝑅) − 1)))) |
24 | 1, 5, 23 | mp2and 711 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑃 ∥ (((𝐴 · 𝑆) − 1) − ((𝐴 · 𝑅) − 1))) |
25 | 12 | zcnd 11359 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝐴 · 𝑆) ∈ ℂ) |
26 | 19 | zcnd 11359 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝐴 · 𝑅) ∈ ℂ) |
27 | | 1cnd 9935 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 1 ∈
ℂ) |
28 | 25, 26, 27 | nnncan2d 10306 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (((𝐴 · 𝑆) − 1) − ((𝐴 · 𝑅) − 1)) = ((𝐴 · 𝑆) − (𝐴 · 𝑅))) |
29 | 9 | zcnd 11359 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝐴 ∈ ℂ) |
30 | | elfznn0 12302 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ (0...(𝑃 − 1)) → 𝑆 ∈
ℕ0) |
31 | 30 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑆 ∈
ℕ0) |
32 | 31 | nn0red 11229 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑆 ∈ ℝ) |
33 | 32 | recnd 9947 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑆 ∈ ℂ) |
34 | 18 | zcnd 11359 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑅 ∈ ℂ) |
35 | 29, 33, 34 | subdid 10365 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝐴 · (𝑆 − 𝑅)) = ((𝐴 · 𝑆) − (𝐴 · 𝑅))) |
36 | 28, 35 | eqtr4d 2647 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (((𝐴 · 𝑆) − 1) − ((𝐴 · 𝑅) − 1)) = (𝐴 · (𝑆 − 𝑅))) |
37 | 24, 36 | breqtrd 4609 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑃 ∥ (𝐴 · (𝑆 − 𝑅))) |
38 | | simpl3 1059 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → ¬ 𝑃 ∥ 𝐴) |
39 | | coprm 15261 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (¬
𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1)) |
40 | 6, 9, 39 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (¬ 𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1)) |
41 | 38, 40 | mpbid 221 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝑃 gcd 𝐴) = 1) |
42 | 11, 18 | zsubcld 11363 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝑆 − 𝑅) ∈ ℤ) |
43 | | coprmdvds 15204 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ (𝑆 − 𝑅) ∈ ℤ) → ((𝑃 ∥ (𝐴 · (𝑆 − 𝑅)) ∧ (𝑃 gcd 𝐴) = 1) → 𝑃 ∥ (𝑆 − 𝑅))) |
44 | 8, 9, 42, 43 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → ((𝑃 ∥ (𝐴 · (𝑆 − 𝑅)) ∧ (𝑃 gcd 𝐴) = 1) → 𝑃 ∥ (𝑆 − 𝑅))) |
45 | 37, 41, 44 | mp2and 711 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑃 ∥ (𝑆 − 𝑅)) |
46 | | prmnn 15226 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
47 | 6, 46 | syl 17 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑃 ∈ ℕ) |
48 | | moddvds 14829 |
. . . . . 6
⊢ ((𝑃 ∈ ℕ ∧ 𝑆 ∈ ℤ ∧ 𝑅 ∈ ℤ) → ((𝑆 mod 𝑃) = (𝑅 mod 𝑃) ↔ 𝑃 ∥ (𝑆 − 𝑅))) |
49 | 47, 11, 18, 48 | syl3anc 1318 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → ((𝑆 mod 𝑃) = (𝑅 mod 𝑃) ↔ 𝑃 ∥ (𝑆 − 𝑅))) |
50 | 45, 49 | mpbird 246 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝑆 mod 𝑃) = (𝑅 mod 𝑃)) |
51 | 47 | nnrpd 11746 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑃 ∈
ℝ+) |
52 | | elfzle1 12215 |
. . . . . 6
⊢ (𝑆 ∈ (0...(𝑃 − 1)) → 0 ≤ 𝑆) |
53 | 52 | ad2antrl 760 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 0 ≤ 𝑆) |
54 | | elfzle2 12216 |
. . . . . . 7
⊢ (𝑆 ∈ (0...(𝑃 − 1)) → 𝑆 ≤ (𝑃 − 1)) |
55 | 54 | ad2antrl 760 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑆 ≤ (𝑃 − 1)) |
56 | | zltlem1 11307 |
. . . . . . 7
⊢ ((𝑆 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑆 < 𝑃 ↔ 𝑆 ≤ (𝑃 − 1))) |
57 | 11, 8, 56 | syl2anc 691 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝑆 < 𝑃 ↔ 𝑆 ≤ (𝑃 − 1))) |
58 | 55, 57 | mpbird 246 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑆 < 𝑃) |
59 | | modid 12557 |
. . . . 5
⊢ (((𝑆 ∈ ℝ ∧ 𝑃 ∈ ℝ+)
∧ (0 ≤ 𝑆 ∧ 𝑆 < 𝑃)) → (𝑆 mod 𝑃) = 𝑆) |
60 | 32, 51, 53, 58, 59 | syl22anc 1319 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝑆 mod 𝑃) = 𝑆) |
61 | | prmuz2 15246 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
62 | | uznn0sub 11595 |
. . . . . . . . 9
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑃 − 2) ∈
ℕ0) |
63 | 6, 61, 62 | 3syl 18 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝑃 − 2) ∈
ℕ0) |
64 | | zexpcl 12737 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (𝑃 − 2) ∈
ℕ0) → (𝐴↑(𝑃 − 2)) ∈
ℤ) |
65 | 9, 63, 64 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝐴↑(𝑃 − 2)) ∈
ℤ) |
66 | 65 | zred 11358 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝐴↑(𝑃 − 2)) ∈
ℝ) |
67 | | modabs2 12566 |
. . . . . 6
⊢ (((𝐴↑(𝑃 − 2)) ∈ ℝ ∧ 𝑃 ∈ ℝ+)
→ (((𝐴↑(𝑃 − 2)) mod 𝑃) mod 𝑃) = ((𝐴↑(𝑃 − 2)) mod 𝑃)) |
68 | 66, 51, 67 | syl2anc 691 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (((𝐴↑(𝑃 − 2)) mod 𝑃) mod 𝑃) = ((𝐴↑(𝑃 − 2)) mod 𝑃)) |
69 | 2 | oveq1i 6559 |
. . . . 5
⊢ (𝑅 mod 𝑃) = (((𝐴↑(𝑃 − 2)) mod 𝑃) mod 𝑃) |
70 | 68, 69, 2 | 3eqtr4g 2669 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → (𝑅 mod 𝑃) = 𝑅) |
71 | 50, 60, 70 | 3eqtr3d 2652 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) ∧ (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1))) → 𝑆 = 𝑅) |
72 | 71 | ex 449 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1)) → 𝑆 = 𝑅)) |
73 | | 1e0p1 11428 |
. . . . . . . 8
⊢ 1 = (0 +
1) |
74 | 73 | oveq1i 6559 |
. . . . . . 7
⊢
(1...(𝑃 − 1))
= ((0 + 1)...(𝑃 −
1)) |
75 | | 0z 11265 |
. . . . . . . 8
⊢ 0 ∈
ℤ |
76 | | fzp1ss 12262 |
. . . . . . . 8
⊢ (0 ∈
ℤ → ((0 + 1)...(𝑃 − 1)) ⊆ (0...(𝑃 − 1))) |
77 | 75, 76 | ax-mp 5 |
. . . . . . 7
⊢ ((0 +
1)...(𝑃 − 1)) ⊆
(0...(𝑃 −
1)) |
78 | 74, 77 | eqsstri 3598 |
. . . . . 6
⊢
(1...(𝑃 − 1))
⊆ (0...(𝑃 −
1)) |
79 | 78 | sseli 3564 |
. . . . 5
⊢ (𝑅 ∈ (1...(𝑃 − 1)) → 𝑅 ∈ (0...(𝑃 − 1))) |
80 | | eleq1 2676 |
. . . . 5
⊢ (𝑆 = 𝑅 → (𝑆 ∈ (0...(𝑃 − 1)) ↔ 𝑅 ∈ (0...(𝑃 − 1)))) |
81 | 79, 80 | syl5ibr 235 |
. . . 4
⊢ (𝑆 = 𝑅 → (𝑅 ∈ (1...(𝑃 − 1)) → 𝑆 ∈ (0...(𝑃 − 1)))) |
82 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑆 = 𝑅 → (𝐴 · 𝑆) = (𝐴 · 𝑅)) |
83 | 82 | oveq1d 6564 |
. . . . . 6
⊢ (𝑆 = 𝑅 → ((𝐴 · 𝑆) − 1) = ((𝐴 · 𝑅) − 1)) |
84 | 83 | breq2d 4595 |
. . . . 5
⊢ (𝑆 = 𝑅 → (𝑃 ∥ ((𝐴 · 𝑆) − 1) ↔ 𝑃 ∥ ((𝐴 · 𝑅) − 1))) |
85 | 84 | biimprd 237 |
. . . 4
⊢ (𝑆 = 𝑅 → (𝑃 ∥ ((𝐴 · 𝑅) − 1) → 𝑃 ∥ ((𝐴 · 𝑆) − 1))) |
86 | 81, 85 | anim12d 584 |
. . 3
⊢ (𝑆 = 𝑅 → ((𝑅 ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑅) − 1)) → (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1)))) |
87 | 3, 86 | syl5com 31 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑆 = 𝑅 → (𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1)))) |
88 | 72, 87 | impbid 201 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1)) ↔ 𝑆 = 𝑅)) |