Step | Hyp | Ref
| Expression |
1 | | reumodprminv 12207 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃!𝑟 ∈ (1...(𝑃 − 1))((𝑁 · 𝑟) mod 𝑃) = 1) |
2 | | reurex 2683 |
. . . 4
⊢
(∃!𝑟 ∈
(1...(𝑃 − 1))((𝑁 · 𝑟) mod 𝑃) = 1 → ∃𝑟 ∈ (1...(𝑃 − 1))((𝑁 · 𝑟) mod 𝑃) = 1) |
3 | | prmz 12065 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
4 | 3 | 3ad2ant1 1013 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑃 ∈ ℤ) |
5 | 4 | adantl 275 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑃 ∈ ℤ) |
6 | | elfzelz 9981 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ (1...(𝑃 − 1)) → 𝑟 ∈ ℤ) |
7 | 6 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) → 𝑟 ∈ ℤ) |
8 | | elfzoelz 10103 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ (1..^𝑃) → 𝐼 ∈ ℤ) |
9 | 8 | 3ad2ant3 1015 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝐼 ∈ ℤ) |
10 | | zmulcl 9265 |
. . . . . . . . . 10
⊢ ((𝑟 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝑟 · 𝐼) ∈ ℤ) |
11 | 7, 9, 10 | syl2an 287 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑟 · 𝐼) ∈ ℤ) |
12 | 5, 11 | zsubcld 9339 |
. . . . . . . 8
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑃 − (𝑟 · 𝐼)) ∈ ℤ) |
13 | | prmnn 12064 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
14 | 13 | 3ad2ant1 1013 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑃 ∈ ℕ) |
15 | 14 | adantl 275 |
. . . . . . . 8
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑃 ∈ ℕ) |
16 | | zmodfzo 10303 |
. . . . . . . 8
⊢ (((𝑃 − (𝑟 · 𝐼)) ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑃 − (𝑟 · 𝐼)) mod 𝑃) ∈ (0..^𝑃)) |
17 | 12, 15, 16 | syl2anc 409 |
. . . . . . 7
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑃 − (𝑟 · 𝐼)) mod 𝑃) ∈ (0..^𝑃)) |
18 | 9 | adantl 275 |
. . . . . . . . . 10
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝐼 ∈ ℤ) |
19 | | zq 9585 |
. . . . . . . . . 10
⊢ (𝐼 ∈ ℤ → 𝐼 ∈
ℚ) |
20 | 18, 19 | syl 14 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝐼 ∈ ℚ) |
21 | | zq 9585 |
. . . . . . . . . 10
⊢ ((𝑃 − (𝑟 · 𝐼)) ∈ ℤ → (𝑃 − (𝑟 · 𝐼)) ∈ ℚ) |
22 | 12, 21 | syl 14 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑃 − (𝑟 · 𝐼)) ∈ ℚ) |
23 | | elfzoelz 10103 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ (1..^𝑃) → 𝑁 ∈ ℤ) |
24 | 23 | 3ad2ant2 1014 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑁 ∈ ℤ) |
25 | 24 | adantl 275 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑁 ∈ ℤ) |
26 | | zq 9585 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℤ → 𝑃 ∈
ℚ) |
27 | 5, 26 | syl 14 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑃 ∈ ℚ) |
28 | 15 | nngt0d 8922 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 0 < 𝑃) |
29 | | modqaddmulmod 10347 |
. . . . . . . . 9
⊢ (((𝐼 ∈ ℚ ∧ (𝑃 − (𝑟 · 𝐼)) ∈ ℚ ∧ 𝑁 ∈ ℤ) ∧ (𝑃 ∈ ℚ ∧ 0 < 𝑃)) → ((𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)) mod 𝑃) = ((𝐼 + ((𝑃 − (𝑟 · 𝐼)) · 𝑁)) mod 𝑃)) |
30 | 20, 22, 25, 27, 28, 29 | syl32anc 1241 |
. . . . . . . 8
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)) mod 𝑃) = ((𝐼 + ((𝑃 − (𝑟 · 𝐼)) · 𝑁)) mod 𝑃)) |
31 | 13 | nncnd 8892 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℂ) |
32 | 31 | 3ad2ant1 1013 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑃 ∈ ℂ) |
33 | 32 | adantl 275 |
. . . . . . . . . . 11
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑃 ∈ ℂ) |
34 | 6 | zcnd 9335 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ (1...(𝑃 − 1)) → 𝑟 ∈ ℂ) |
35 | 34 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) → 𝑟 ∈ ℂ) |
36 | 8 | zcnd 9335 |
. . . . . . . . . . . . 13
⊢ (𝐼 ∈ (1..^𝑃) → 𝐼 ∈ ℂ) |
37 | 36 | 3ad2ant3 1015 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝐼 ∈ ℂ) |
38 | | mulcl 7901 |
. . . . . . . . . . . 12
⊢ ((𝑟 ∈ ℂ ∧ 𝐼 ∈ ℂ) → (𝑟 · 𝐼) ∈ ℂ) |
39 | 35, 37, 38 | syl2an 287 |
. . . . . . . . . . 11
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑟 · 𝐼) ∈ ℂ) |
40 | 23 | zcnd 9335 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ (1..^𝑃) → 𝑁 ∈ ℂ) |
41 | 40 | 3ad2ant2 1014 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑁 ∈ ℂ) |
42 | 41 | adantl 275 |
. . . . . . . . . . 11
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑁 ∈ ℂ) |
43 | 33, 39, 42 | subdird 8334 |
. . . . . . . . . 10
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑃 − (𝑟 · 𝐼)) · 𝑁) = ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁))) |
44 | 43 | oveq2d 5869 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝐼 + ((𝑃 − (𝑟 · 𝐼)) · 𝑁)) = (𝐼 + ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)))) |
45 | 44 | oveq1d 5868 |
. . . . . . . 8
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + ((𝑃 − (𝑟 · 𝐼)) · 𝑁)) mod 𝑃) = ((𝐼 + ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁))) mod 𝑃)) |
46 | | mulcom 7903 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑃 · 𝑁) = (𝑁 · 𝑃)) |
47 | 31, 40, 46 | syl2an 287 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (𝑃 · 𝑁) = (𝑁 · 𝑃)) |
48 | 47 | oveq1d 5868 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ((𝑃 · 𝑁) mod 𝑃) = ((𝑁 · 𝑃) mod 𝑃)) |
49 | 23 | adantl 275 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 𝑁 ∈ ℤ) |
50 | 3 | adantr 274 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 𝑃 ∈ ℤ) |
51 | 50, 26 | syl 14 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 𝑃 ∈ ℚ) |
52 | 13 | nngt0d 8922 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℙ → 0 <
𝑃) |
53 | 52 | adantr 274 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 0 < 𝑃) |
54 | | mulqmod0 10286 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℤ ∧ 𝑃 ∈ ℚ ∧ 0 <
𝑃) → ((𝑁 · 𝑃) mod 𝑃) = 0) |
55 | 49, 51, 53, 54 | syl3anc 1233 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ((𝑁 · 𝑃) mod 𝑃) = 0) |
56 | 48, 55 | eqtrd 2203 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ((𝑃 · 𝑁) mod 𝑃) = 0) |
57 | 56 | 3adant3 1012 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ((𝑃 · 𝑁) mod 𝑃) = 0) |
58 | 57 | adantl 275 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑃 · 𝑁) mod 𝑃) = 0) |
59 | 35 | adantr 274 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑟 ∈ ℂ) |
60 | 37 | adantl 275 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝐼 ∈ ℂ) |
61 | 59, 60, 42 | mul32d 8072 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑟 · 𝐼) · 𝑁) = ((𝑟 · 𝑁) · 𝐼)) |
62 | 61 | oveq1d 5868 |
. . . . . . . . . . . . . . 15
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑟 · 𝐼) · 𝑁) mod 𝑃) = (((𝑟 · 𝑁) · 𝐼) mod 𝑃)) |
63 | | elfznn 10010 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 ∈ (1...(𝑃 − 1)) → 𝑟 ∈ ℕ) |
64 | 63 | adantr 274 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) → 𝑟 ∈ ℕ) |
65 | 64 | adantr 274 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑟 ∈ ℕ) |
66 | | elfzo1 10146 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ (1..^𝑃) ↔ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℕ ∧ 𝑁 < 𝑃)) |
67 | 66 | simp1bi 1007 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ (1..^𝑃) → 𝑁 ∈ ℕ) |
68 | 67 | 3ad2ant2 1014 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑁 ∈ ℕ) |
69 | 68 | adantl 275 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑁 ∈ ℕ) |
70 | 65, 69 | nnmulcld 8927 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑟 · 𝑁) ∈ ℕ) |
71 | | nnq 9592 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑟 · 𝑁) ∈ ℕ → (𝑟 · 𝑁) ∈ ℚ) |
72 | 70, 71 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑟 · 𝑁) ∈ ℚ) |
73 | | modqmulmod 10345 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑟 · 𝑁) ∈ ℚ ∧ 𝐼 ∈ ℤ) ∧ (𝑃 ∈ ℚ ∧ 0 < 𝑃)) → ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃) = (((𝑟 · 𝑁) · 𝐼) mod 𝑃)) |
74 | 72, 18, 27, 28, 73 | syl22anc 1234 |
. . . . . . . . . . . . . . 15
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃) = (((𝑟 · 𝑁) · 𝐼) mod 𝑃)) |
75 | 62, 74 | eqtr4d 2206 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑟 · 𝐼) · 𝑁) mod 𝑃) = ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃)) |
76 | 58, 75 | oveq12d 5871 |
. . . . . . . . . . . . 13
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑃 · 𝑁) mod 𝑃) − (((𝑟 · 𝐼) · 𝑁) mod 𝑃)) = (0 − ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃))) |
77 | 76 | oveq1d 5868 |
. . . . . . . . . . . 12
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((((𝑃 · 𝑁) mod 𝑃) − (((𝑟 · 𝐼) · 𝑁) mod 𝑃)) mod 𝑃) = ((0 − ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃)) mod 𝑃)) |
78 | 15, 69 | nnmulcld 8927 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑃 · 𝑁) ∈ ℕ) |
79 | | nnq 9592 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 · 𝑁) ∈ ℕ → (𝑃 · 𝑁) ∈ ℚ) |
80 | 78, 79 | syl 14 |
. . . . . . . . . . . . 13
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑃 · 𝑁) ∈ ℚ) |
81 | | elfzo1 10146 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐼 ∈ (1..^𝑃) ↔ (𝐼 ∈ ℕ ∧ 𝑃 ∈ ℕ ∧ 𝐼 < 𝑃)) |
82 | 81 | simp1bi 1007 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∈ (1..^𝑃) → 𝐼 ∈ ℕ) |
83 | 82 | 3ad2ant3 1015 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝐼 ∈ ℕ) |
84 | 83 | adantl 275 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝐼 ∈ ℕ) |
85 | 65, 84 | nnmulcld 8927 |
. . . . . . . . . . . . . . 15
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑟 · 𝐼) ∈ ℕ) |
86 | 85, 69 | nnmulcld 8927 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑟 · 𝐼) · 𝑁) ∈ ℕ) |
87 | | nnq 9592 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 · 𝐼) · 𝑁) ∈ ℕ → ((𝑟 · 𝐼) · 𝑁) ∈ ℚ) |
88 | 86, 87 | syl 14 |
. . . . . . . . . . . . 13
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑟 · 𝐼) · 𝑁) ∈ ℚ) |
89 | | modqsubmodmod 10339 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 · 𝑁) ∈ ℚ ∧ ((𝑟 · 𝐼) · 𝑁) ∈ ℚ) ∧ (𝑃 ∈ ℚ ∧ 0 < 𝑃)) → ((((𝑃 · 𝑁) mod 𝑃) − (((𝑟 · 𝐼) · 𝑁) mod 𝑃)) mod 𝑃) = (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃)) |
90 | 80, 88, 27, 28, 89 | syl22anc 1234 |
. . . . . . . . . . . 12
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((((𝑃 · 𝑁) mod 𝑃) − (((𝑟 · 𝐼) · 𝑁) mod 𝑃)) mod 𝑃) = (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃)) |
91 | | mulcom 7903 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℂ ∧ 𝑟 ∈ ℂ) → (𝑁 · 𝑟) = (𝑟 · 𝑁)) |
92 | 41, 34, 91 | syl2anr 288 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑁 · 𝑟) = (𝑟 · 𝑁)) |
93 | 92 | oveq1d 5868 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑁 · 𝑟) mod 𝑃) = ((𝑟 · 𝑁) mod 𝑃)) |
94 | 93 | eqeq1d 2179 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑁 · 𝑟) mod 𝑃) = 1 ↔ ((𝑟 · 𝑁) mod 𝑃) = 1)) |
95 | 94 | biimpd 143 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑁 · 𝑟) mod 𝑃) = 1 → ((𝑟 · 𝑁) mod 𝑃) = 1)) |
96 | 95 | impancom 258 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ((𝑟 · 𝑁) mod 𝑃) = 1)) |
97 | 96 | imp 123 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑟 · 𝑁) mod 𝑃) = 1) |
98 | 97 | oveq1d 5868 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑟 · 𝑁) mod 𝑃) · 𝐼) = (1 · 𝐼)) |
99 | 98 | oveq1d 5868 |
. . . . . . . . . . . . . . 15
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃) = ((1 · 𝐼) mod 𝑃)) |
100 | 99 | oveq2d 5869 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (0 − ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃)) = (0 − ((1 · 𝐼) mod 𝑃))) |
101 | 100 | oveq1d 5868 |
. . . . . . . . . . . . 13
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((0 − ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃)) mod 𝑃) = ((0 − ((1 · 𝐼) mod 𝑃)) mod 𝑃)) |
102 | 60 | mulid2d 7938 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (1 · 𝐼) = 𝐼) |
103 | 102 | oveq1d 5868 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((1 · 𝐼) mod 𝑃) = (𝐼 mod 𝑃)) |
104 | 84 | nnnn0d 9188 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝐼 ∈
ℕ0) |
105 | 104 | nn0ge0d 9191 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 0 ≤ 𝐼) |
106 | | elfzolt2 10112 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐼 ∈ (1..^𝑃) → 𝐼 < 𝑃) |
107 | 106 | 3ad2ant3 1015 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝐼 < 𝑃) |
108 | 107 | adantl 275 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝐼 < 𝑃) |
109 | | modqid 10305 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐼 ∈ ℚ ∧ 𝑃 ∈ ℚ) ∧ (0 ≤
𝐼 ∧ 𝐼 < 𝑃)) → (𝐼 mod 𝑃) = 𝐼) |
110 | 20, 27, 105, 108, 109 | syl22anc 1234 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝐼 mod 𝑃) = 𝐼) |
111 | 103, 110 | eqtrd 2203 |
. . . . . . . . . . . . . . 15
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((1 · 𝐼) mod 𝑃) = 𝐼) |
112 | 111 | oveq2d 5869 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (0 − ((1 · 𝐼) mod 𝑃)) = (0 − 𝐼)) |
113 | 112 | oveq1d 5868 |
. . . . . . . . . . . . 13
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((0 − ((1 · 𝐼) mod 𝑃)) mod 𝑃) = ((0 − 𝐼) mod 𝑃)) |
114 | 101, 113 | eqtrd 2203 |
. . . . . . . . . . . 12
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((0 − ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃)) mod 𝑃) = ((0 − 𝐼) mod 𝑃)) |
115 | 77, 90, 114 | 3eqtr3d 2211 |
. . . . . . . . . . 11
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃) = ((0 − 𝐼) mod 𝑃)) |
116 | 115 | oveq2d 5869 |
. . . . . . . . . 10
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝐼 + (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃)) = (𝐼 + ((0 − 𝐼) mod 𝑃))) |
117 | 116 | oveq1d 5868 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃)) mod 𝑃) = ((𝐼 + ((0 − 𝐼) mod 𝑃)) mod 𝑃)) |
118 | | qsubcl 9597 |
. . . . . . . . . . 11
⊢ (((𝑃 · 𝑁) ∈ ℚ ∧ ((𝑟 · 𝐼) · 𝑁) ∈ ℚ) → ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) ∈ ℚ) |
119 | 80, 88, 118 | syl2anc 409 |
. . . . . . . . . 10
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) ∈ ℚ) |
120 | | modqadd2mod 10330 |
. . . . . . . . . 10
⊢
(((((𝑃 ·
𝑁) − ((𝑟 · 𝐼) · 𝑁)) ∈ ℚ ∧ 𝐼 ∈ ℚ) ∧ (𝑃 ∈ ℚ ∧ 0 < 𝑃)) → ((𝐼 + (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃)) mod 𝑃) = ((𝐼 + ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁))) mod 𝑃)) |
121 | 119, 20, 27, 28, 120 | syl22anc 1234 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃)) mod 𝑃) = ((𝐼 + ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁))) mod 𝑃)) |
122 | | 0zd 9224 |
. . . . . . . . . . . . 13
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 0 ∈
ℤ) |
123 | 122, 18 | zsubcld 9339 |
. . . . . . . . . . . 12
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (0 − 𝐼) ∈ ℤ) |
124 | | zq 9585 |
. . . . . . . . . . . 12
⊢ ((0
− 𝐼) ∈ ℤ
→ (0 − 𝐼) ∈
ℚ) |
125 | 123, 124 | syl 14 |
. . . . . . . . . . 11
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (0 − 𝐼) ∈ ℚ) |
126 | | modqadd2mod 10330 |
. . . . . . . . . . 11
⊢ ((((0
− 𝐼) ∈ ℚ
∧ 𝐼 ∈ ℚ)
∧ (𝑃 ∈ ℚ
∧ 0 < 𝑃)) →
((𝐼 + ((0 − 𝐼) mod 𝑃)) mod 𝑃) = ((𝐼 + (0 − 𝐼)) mod 𝑃)) |
127 | 125, 20, 27, 28, 126 | syl22anc 1234 |
. . . . . . . . . 10
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + ((0 − 𝐼) mod 𝑃)) mod 𝑃) = ((𝐼 + (0 − 𝐼)) mod 𝑃)) |
128 | | 0cnd 7913 |
. . . . . . . . . . . . . 14
⊢ (𝐼 ∈ (1..^𝑃) → 0 ∈ ℂ) |
129 | 36, 128 | pncan3d 8233 |
. . . . . . . . . . . . 13
⊢ (𝐼 ∈ (1..^𝑃) → (𝐼 + (0 − 𝐼)) = 0) |
130 | 129 | 3ad2ant3 1015 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → (𝐼 + (0 − 𝐼)) = 0) |
131 | 130 | adantl 275 |
. . . . . . . . . . 11
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝐼 + (0 − 𝐼)) = 0) |
132 | 131 | oveq1d 5868 |
. . . . . . . . . 10
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + (0 − 𝐼)) mod 𝑃) = (0 mod 𝑃)) |
133 | 3, 26 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℚ) |
134 | | q0mod 10311 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℚ ∧ 0 <
𝑃) → (0 mod 𝑃) = 0) |
135 | 133, 52, 134 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → (0 mod
𝑃) = 0) |
136 | 135 | 3ad2ant1 1013 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → (0 mod 𝑃) = 0) |
137 | 136 | adantl 275 |
. . . . . . . . . 10
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (0 mod 𝑃) = 0) |
138 | 127, 132,
137 | 3eqtrd 2207 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + ((0 − 𝐼) mod 𝑃)) mod 𝑃) = 0) |
139 | 117, 121,
138 | 3eqtr3d 2211 |
. . . . . . . 8
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁))) mod 𝑃) = 0) |
140 | 30, 45, 139 | 3eqtrd 2207 |
. . . . . . 7
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)) mod 𝑃) = 0) |
141 | | oveq1 5860 |
. . . . . . . . . . 11
⊢ (𝑗 = ((𝑃 − (𝑟 · 𝐼)) mod 𝑃) → (𝑗 · 𝑁) = (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)) |
142 | 141 | oveq2d 5869 |
. . . . . . . . . 10
⊢ (𝑗 = ((𝑃 − (𝑟 · 𝐼)) mod 𝑃) → (𝐼 + (𝑗 · 𝑁)) = (𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁))) |
143 | 142 | oveq1d 5868 |
. . . . . . . . 9
⊢ (𝑗 = ((𝑃 − (𝑟 · 𝐼)) mod 𝑃) → ((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = ((𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)) mod 𝑃)) |
144 | 143 | eqeq1d 2179 |
. . . . . . . 8
⊢ (𝑗 = ((𝑃 − (𝑟 · 𝐼)) mod 𝑃) → (((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0 ↔ ((𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)) mod 𝑃) = 0)) |
145 | 144 | rspcev 2834 |
. . . . . . 7
⊢ ((((𝑃 − (𝑟 · 𝐼)) mod 𝑃) ∈ (0..^𝑃) ∧ ((𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)) mod 𝑃) = 0) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
146 | 17, 140, 145 | syl2anc 409 |
. . . . . 6
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
147 | 146 | ex 114 |
. . . . 5
⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
148 | 147 | rexlimiva 2582 |
. . . 4
⊢
(∃𝑟 ∈
(1...(𝑃 − 1))((𝑁 · 𝑟) mod 𝑃) = 1 → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
149 | 1, 2, 148 | 3syl 17 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
150 | 149 | 3adant3 1012 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
151 | 150 | pm2.43i 49 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0) |