Step | Hyp | Ref
| Expression |
1 | | reumodprminv 16254 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃!𝑟 ∈ (1...(𝑃 − 1))((𝑁 · 𝑟) mod 𝑃) = 1) |
2 | | reurex 3330 |
. . . 4
⊢
(∃!𝑟 ∈
(1...(𝑃 − 1))((𝑁 · 𝑟) mod 𝑃) = 1 → ∃𝑟 ∈ (1...(𝑃 − 1))((𝑁 · 𝑟) mod 𝑃) = 1) |
3 | | prmz 16129 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
4 | 3 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑃 ∈ ℤ) |
5 | 4 | adantl 485 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑃 ∈ ℤ) |
6 | | elfzelz 13011 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ (1...(𝑃 − 1)) → 𝑟 ∈ ℤ) |
7 | 6 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) → 𝑟 ∈ ℤ) |
8 | | elfzoelz 13142 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ (1..^𝑃) → 𝐼 ∈ ℤ) |
9 | 8 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝐼 ∈ ℤ) |
10 | | zmulcl 12125 |
. . . . . . . . . 10
⊢ ((𝑟 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝑟 · 𝐼) ∈ ℤ) |
11 | 7, 9, 10 | syl2an 599 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑟 · 𝐼) ∈ ℤ) |
12 | 5, 11 | zsubcld 12186 |
. . . . . . . 8
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑃 − (𝑟 · 𝐼)) ∈ ℤ) |
13 | | prmnn 16128 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
14 | 13 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑃 ∈ ℕ) |
15 | 14 | adantl 485 |
. . . . . . . 8
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑃 ∈ ℕ) |
16 | | zmodfzo 13366 |
. . . . . . . 8
⊢ (((𝑃 − (𝑟 · 𝐼)) ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑃 − (𝑟 · 𝐼)) mod 𝑃) ∈ (0..^𝑃)) |
17 | 12, 15, 16 | syl2anc 587 |
. . . . . . 7
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑃 − (𝑟 · 𝐼)) mod 𝑃) ∈ (0..^𝑃)) |
18 | 8 | zred 12181 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ (1..^𝑃) → 𝐼 ∈ ℝ) |
19 | 18 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝐼 ∈ ℝ) |
20 | 19 | adantl 485 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝐼 ∈ ℝ) |
21 | 13 | nnred 11744 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ) |
22 | 21 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑃 ∈ ℝ) |
23 | 22 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑃 ∈ ℝ) |
24 | 6 | zred 12181 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ (1...(𝑃 − 1)) → 𝑟 ∈ ℝ) |
25 | 24 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) → 𝑟 ∈ ℝ) |
26 | | remulcl 10713 |
. . . . . . . . . . 11
⊢ ((𝑟 ∈ ℝ ∧ 𝐼 ∈ ℝ) → (𝑟 · 𝐼) ∈ ℝ) |
27 | 25, 19, 26 | syl2an 599 |
. . . . . . . . . 10
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑟 · 𝐼) ∈ ℝ) |
28 | 23, 27 | resubcld 11159 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑃 − (𝑟 · 𝐼)) ∈ ℝ) |
29 | | elfzoelz 13142 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ (1..^𝑃) → 𝑁 ∈ ℤ) |
30 | 29 | 3ad2ant2 1135 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑁 ∈ ℤ) |
31 | 30 | adantl 485 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑁 ∈ ℤ) |
32 | 13 | nnrpd 12525 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ+) |
33 | 32 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑃 ∈
ℝ+) |
34 | 33 | adantl 485 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑃 ∈
ℝ+) |
35 | | modaddmulmod 13410 |
. . . . . . . . 9
⊢ (((𝐼 ∈ ℝ ∧ (𝑃 − (𝑟 · 𝐼)) ∈ ℝ ∧ 𝑁 ∈ ℤ) ∧ 𝑃 ∈ ℝ+) → ((𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)) mod 𝑃) = ((𝐼 + ((𝑃 − (𝑟 · 𝐼)) · 𝑁)) mod 𝑃)) |
36 | 20, 28, 31, 34, 35 | syl31anc 1374 |
. . . . . . . 8
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)) mod 𝑃) = ((𝐼 + ((𝑃 − (𝑟 · 𝐼)) · 𝑁)) mod 𝑃)) |
37 | 13 | nncnd 11745 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℂ) |
38 | 37 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑃 ∈ ℂ) |
39 | 38 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑃 ∈ ℂ) |
40 | 6 | zcnd 12182 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ (1...(𝑃 − 1)) → 𝑟 ∈ ℂ) |
41 | 40 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) → 𝑟 ∈ ℂ) |
42 | 8 | zcnd 12182 |
. . . . . . . . . . . . 13
⊢ (𝐼 ∈ (1..^𝑃) → 𝐼 ∈ ℂ) |
43 | 42 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝐼 ∈ ℂ) |
44 | | mulcl 10712 |
. . . . . . . . . . . 12
⊢ ((𝑟 ∈ ℂ ∧ 𝐼 ∈ ℂ) → (𝑟 · 𝐼) ∈ ℂ) |
45 | 41, 43, 44 | syl2an 599 |
. . . . . . . . . . 11
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑟 · 𝐼) ∈ ℂ) |
46 | 29 | zcnd 12182 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ (1..^𝑃) → 𝑁 ∈ ℂ) |
47 | 46 | 3ad2ant2 1135 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑁 ∈ ℂ) |
48 | 47 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑁 ∈ ℂ) |
49 | 39, 45, 48 | subdird 11188 |
. . . . . . . . . 10
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑃 − (𝑟 · 𝐼)) · 𝑁) = ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁))) |
50 | 49 | oveq2d 7199 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝐼 + ((𝑃 − (𝑟 · 𝐼)) · 𝑁)) = (𝐼 + ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)))) |
51 | 50 | oveq1d 7198 |
. . . . . . . 8
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + ((𝑃 − (𝑟 · 𝐼)) · 𝑁)) mod 𝑃) = ((𝐼 + ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁))) mod 𝑃)) |
52 | | mulcom 10714 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑃 · 𝑁) = (𝑁 · 𝑃)) |
53 | 37, 46, 52 | syl2an 599 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (𝑃 · 𝑁) = (𝑁 · 𝑃)) |
54 | 53 | oveq1d 7198 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ((𝑃 · 𝑁) mod 𝑃) = ((𝑁 · 𝑃) mod 𝑃)) |
55 | | mulmod0 13349 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℤ ∧ 𝑃 ∈ ℝ+)
→ ((𝑁 · 𝑃) mod 𝑃) = 0) |
56 | 29, 32, 55 | syl2anr 600 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ((𝑁 · 𝑃) mod 𝑃) = 0) |
57 | 54, 56 | eqtrd 2774 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ((𝑃 · 𝑁) mod 𝑃) = 0) |
58 | 57 | 3adant3 1133 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ((𝑃 · 𝑁) mod 𝑃) = 0) |
59 | 58 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑃 · 𝑁) mod 𝑃) = 0) |
60 | 41 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑟 ∈ ℂ) |
61 | 43 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝐼 ∈ ℂ) |
62 | 60, 61, 48 | mul32d 10941 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑟 · 𝐼) · 𝑁) = ((𝑟 · 𝑁) · 𝐼)) |
63 | 62 | oveq1d 7198 |
. . . . . . . . . . . . . . 15
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑟 · 𝐼) · 𝑁) mod 𝑃) = (((𝑟 · 𝑁) · 𝐼) mod 𝑃)) |
64 | 29 | zred 12181 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ (1..^𝑃) → 𝑁 ∈ ℝ) |
65 | 64 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑁 ∈ ℝ) |
66 | | remulcl 10713 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑟 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑟 · 𝑁) ∈ ℝ) |
67 | 25, 65, 66 | syl2an 599 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑟 · 𝑁) ∈ ℝ) |
68 | 9 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝐼 ∈ ℤ) |
69 | | modmulmod 13408 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑟 · 𝑁) ∈ ℝ ∧ 𝐼 ∈ ℤ ∧ 𝑃 ∈ ℝ+) →
((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃) = (((𝑟 · 𝑁) · 𝐼) mod 𝑃)) |
70 | 67, 68, 34, 69 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃) = (((𝑟 · 𝑁) · 𝐼) mod 𝑃)) |
71 | 63, 70 | eqtr4d 2777 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑟 · 𝐼) · 𝑁) mod 𝑃) = ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃)) |
72 | 59, 71 | oveq12d 7201 |
. . . . . . . . . . . . 13
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑃 · 𝑁) mod 𝑃) − (((𝑟 · 𝐼) · 𝑁) mod 𝑃)) = (0 − ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃))) |
73 | 72 | oveq1d 7198 |
. . . . . . . . . . . 12
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((((𝑃 · 𝑁) mod 𝑃) − (((𝑟 · 𝐼) · 𝑁) mod 𝑃)) mod 𝑃) = ((0 − ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃)) mod 𝑃)) |
74 | | remulcl 10713 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑃 · 𝑁) ∈ ℝ) |
75 | 21, 64, 74 | syl2an 599 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (𝑃 · 𝑁) ∈ ℝ) |
76 | 75 | 3adant3 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → (𝑃 · 𝑁) ∈ ℝ) |
77 | 76 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑃 · 𝑁) ∈ ℝ) |
78 | 65 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑁 ∈ ℝ) |
79 | 27, 78 | remulcld 10762 |
. . . . . . . . . . . . 13
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑟 · 𝐼) · 𝑁) ∈ ℝ) |
80 | | modsubmodmod 13402 |
. . . . . . . . . . . . 13
⊢ (((𝑃 · 𝑁) ∈ ℝ ∧ ((𝑟 · 𝐼) · 𝑁) ∈ ℝ ∧ 𝑃 ∈ ℝ+) →
((((𝑃 · 𝑁) mod 𝑃) − (((𝑟 · 𝐼) · 𝑁) mod 𝑃)) mod 𝑃) = (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃)) |
81 | 77, 79, 34, 80 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((((𝑃 · 𝑁) mod 𝑃) − (((𝑟 · 𝐼) · 𝑁) mod 𝑃)) mod 𝑃) = (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃)) |
82 | | mulcom 10714 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℂ ∧ 𝑟 ∈ ℂ) → (𝑁 · 𝑟) = (𝑟 · 𝑁)) |
83 | 47, 40, 82 | syl2anr 600 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑁 · 𝑟) = (𝑟 · 𝑁)) |
84 | 83 | oveq1d 7198 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑁 · 𝑟) mod 𝑃) = ((𝑟 · 𝑁) mod 𝑃)) |
85 | 84 | eqeq1d 2741 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑁 · 𝑟) mod 𝑃) = 1 ↔ ((𝑟 · 𝑁) mod 𝑃) = 1)) |
86 | 85 | biimpd 232 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑁 · 𝑟) mod 𝑃) = 1 → ((𝑟 · 𝑁) mod 𝑃) = 1)) |
87 | 86 | impancom 455 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ((𝑟 · 𝑁) mod 𝑃) = 1)) |
88 | 87 | imp 410 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑟 · 𝑁) mod 𝑃) = 1) |
89 | 88 | oveq1d 7198 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑟 · 𝑁) mod 𝑃) · 𝐼) = (1 · 𝐼)) |
90 | 89 | oveq1d 7198 |
. . . . . . . . . . . . . . 15
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃) = ((1 · 𝐼) mod 𝑃)) |
91 | 90 | oveq2d 7199 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (0 − ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃)) = (0 − ((1 · 𝐼) mod 𝑃))) |
92 | 91 | oveq1d 7198 |
. . . . . . . . . . . . 13
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((0 − ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃)) mod 𝑃) = ((0 − ((1 · 𝐼) mod 𝑃)) mod 𝑃)) |
93 | 61 | mulid2d 10750 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (1 · 𝐼) = 𝐼) |
94 | 93 | oveq1d 7198 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((1 · 𝐼) mod 𝑃) = (𝐼 mod 𝑃)) |
95 | 32, 18 | anim12ci 617 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℙ ∧ 𝐼 ∈ (1..^𝑃)) → (𝐼 ∈ ℝ ∧ 𝑃 ∈
ℝ+)) |
96 | | elfzo2 13145 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐼 ∈ (1..^𝑃) ↔ (𝐼 ∈ (ℤ≥‘1)
∧ 𝑃 ∈ ℤ
∧ 𝐼 < 𝑃)) |
97 | | eluz2 12343 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐼 ∈
(ℤ≥‘1) ↔ (1 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 1 ≤
𝐼)) |
98 | | 0red 10735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐼 ∈ ℤ → 0 ∈
ℝ) |
99 | | 1red 10733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐼 ∈ ℤ → 1 ∈
ℝ) |
100 | | zre 12079 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐼 ∈ ℤ → 𝐼 ∈
ℝ) |
101 | 98, 99, 100 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐼 ∈ ℤ → (0 ∈
ℝ ∧ 1 ∈ ℝ ∧ 𝐼 ∈ ℝ)) |
102 | 101 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐼 ∈ ℤ ∧ 1 ≤
𝐼) → (0 ∈ ℝ
∧ 1 ∈ ℝ ∧ 𝐼 ∈ ℝ)) |
103 | | 0le1 11254 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 0 ≤
1 |
104 | 103 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐼 ∈ ℤ → 0 ≤
1) |
105 | 104 | anim1i 618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐼 ∈ ℤ ∧ 1 ≤
𝐼) → (0 ≤ 1 ∧ 1
≤ 𝐼)) |
106 | | letr 10825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐼 ∈ ℝ) → ((0 ≤ 1 ∧ 1
≤ 𝐼) → 0 ≤ 𝐼)) |
107 | 102, 105,
106 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐼 ∈ ℤ ∧ 1 ≤
𝐼) → 0 ≤ 𝐼) |
108 | 107 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((1
∈ ℤ ∧ 𝐼
∈ ℤ ∧ 1 ≤ 𝐼) → 0 ≤ 𝐼) |
109 | 97, 108 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐼 ∈
(ℤ≥‘1) → 0 ≤ 𝐼) |
110 | 109 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐼 ∈
(ℤ≥‘1) ∧ 𝑃 ∈ ℤ ∧ 𝐼 < 𝑃) → 0 ≤ 𝐼) |
111 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐼 ∈
(ℤ≥‘1) ∧ 𝑃 ∈ ℤ ∧ 𝐼 < 𝑃) → 𝐼 < 𝑃) |
112 | 110, 111 | jca 515 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐼 ∈
(ℤ≥‘1) ∧ 𝑃 ∈ ℤ ∧ 𝐼 < 𝑃) → (0 ≤ 𝐼 ∧ 𝐼 < 𝑃)) |
113 | 96, 112 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐼 ∈ (1..^𝑃) → (0 ≤ 𝐼 ∧ 𝐼 < 𝑃)) |
114 | 113 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℙ ∧ 𝐼 ∈ (1..^𝑃)) → (0 ≤ 𝐼 ∧ 𝐼 < 𝑃)) |
115 | 95, 114 | jca 515 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ ℙ ∧ 𝐼 ∈ (1..^𝑃)) → ((𝐼 ∈ ℝ ∧ 𝑃 ∈ ℝ+) ∧ (0 ≤
𝐼 ∧ 𝐼 < 𝑃))) |
116 | 115 | 3adant2 1132 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ((𝐼 ∈ ℝ ∧ 𝑃 ∈ ℝ+) ∧ (0 ≤
𝐼 ∧ 𝐼 < 𝑃))) |
117 | 116 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 ∈ ℝ ∧ 𝑃 ∈ ℝ+) ∧ (0 ≤
𝐼 ∧ 𝐼 < 𝑃))) |
118 | | modid 13368 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐼 ∈ ℝ ∧ 𝑃 ∈ ℝ+)
∧ (0 ≤ 𝐼 ∧ 𝐼 < 𝑃)) → (𝐼 mod 𝑃) = 𝐼) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝐼 mod 𝑃) = 𝐼) |
120 | 94, 119 | eqtrd 2774 |
. . . . . . . . . . . . . . 15
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((1 · 𝐼) mod 𝑃) = 𝐼) |
121 | 120 | oveq2d 7199 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (0 − ((1 · 𝐼) mod 𝑃)) = (0 − 𝐼)) |
122 | 121 | oveq1d 7198 |
. . . . . . . . . . . . 13
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((0 − ((1 · 𝐼) mod 𝑃)) mod 𝑃) = ((0 − 𝐼) mod 𝑃)) |
123 | 92, 122 | eqtrd 2774 |
. . . . . . . . . . . 12
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((0 − ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃)) mod 𝑃) = ((0 − 𝐼) mod 𝑃)) |
124 | 73, 81, 123 | 3eqtr3d 2782 |
. . . . . . . . . . 11
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃) = ((0 − 𝐼) mod 𝑃)) |
125 | 124 | oveq2d 7199 |
. . . . . . . . . 10
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝐼 + (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃)) = (𝐼 + ((0 − 𝐼) mod 𝑃))) |
126 | 125 | oveq1d 7198 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃)) mod 𝑃) = ((𝐼 + ((0 − 𝐼) mod 𝑃)) mod 𝑃)) |
127 | 77, 79 | resubcld 11159 |
. . . . . . . . . 10
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) ∈ ℝ) |
128 | | modadd2mod 13393 |
. . . . . . . . . 10
⊢ ((((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) ∈ ℝ ∧ 𝐼 ∈ ℝ ∧ 𝑃 ∈ ℝ+) → ((𝐼 + (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃)) mod 𝑃) = ((𝐼 + ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁))) mod 𝑃)) |
129 | 127, 20, 34, 128 | syl3anc 1372 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃)) mod 𝑃) = ((𝐼 + ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁))) mod 𝑃)) |
130 | | 0red 10735 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼 ∈ (1..^𝑃) → 0 ∈ ℝ) |
131 | 130, 18 | resubcld 11159 |
. . . . . . . . . . . . . . 15
⊢ (𝐼 ∈ (1..^𝑃) → (0 − 𝐼) ∈ ℝ) |
132 | 131 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐼 ∈ (1..^𝑃)) → (0 − 𝐼) ∈ ℝ) |
133 | 18 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐼 ∈ (1..^𝑃)) → 𝐼 ∈ ℝ) |
134 | 32 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐼 ∈ (1..^𝑃)) → 𝑃 ∈
ℝ+) |
135 | 132, 133,
134 | 3jca 1129 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐼 ∈ (1..^𝑃)) → ((0 − 𝐼) ∈ ℝ ∧ 𝐼 ∈ ℝ ∧ 𝑃 ∈
ℝ+)) |
136 | 135 | 3adant2 1132 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ((0 − 𝐼) ∈ ℝ ∧ 𝐼 ∈ ℝ ∧ 𝑃 ∈
ℝ+)) |
137 | 136 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((0 − 𝐼) ∈ ℝ ∧ 𝐼 ∈ ℝ ∧ 𝑃 ∈
ℝ+)) |
138 | | modadd2mod 13393 |
. . . . . . . . . . 11
⊢ (((0
− 𝐼) ∈ ℝ
∧ 𝐼 ∈ ℝ
∧ 𝑃 ∈
ℝ+) → ((𝐼 + ((0 − 𝐼) mod 𝑃)) mod 𝑃) = ((𝐼 + (0 − 𝐼)) mod 𝑃)) |
139 | 137, 138 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + ((0 − 𝐼) mod 𝑃)) mod 𝑃) = ((𝐼 + (0 − 𝐼)) mod 𝑃)) |
140 | | 0cnd 10725 |
. . . . . . . . . . . . . 14
⊢ (𝐼 ∈ (1..^𝑃) → 0 ∈ ℂ) |
141 | 42, 140 | pncan3d 11091 |
. . . . . . . . . . . . 13
⊢ (𝐼 ∈ (1..^𝑃) → (𝐼 + (0 − 𝐼)) = 0) |
142 | 141 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → (𝐼 + (0 − 𝐼)) = 0) |
143 | 142 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝐼 + (0 − 𝐼)) = 0) |
144 | 143 | oveq1d 7198 |
. . . . . . . . . 10
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + (0 − 𝐼)) mod 𝑃) = (0 mod 𝑃)) |
145 | | 0mod 13374 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℝ+
→ (0 mod 𝑃) =
0) |
146 | 32, 145 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → (0 mod
𝑃) = 0) |
147 | 146 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → (0 mod 𝑃) = 0) |
148 | 147 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (0 mod 𝑃) = 0) |
149 | 139, 144,
148 | 3eqtrd 2778 |
. . . . . . . . 9
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + ((0 − 𝐼) mod 𝑃)) mod 𝑃) = 0) |
150 | 126, 129,
149 | 3eqtr3d 2782 |
. . . . . . . 8
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁))) mod 𝑃) = 0) |
151 | 36, 51, 150 | 3eqtrd 2778 |
. . . . . . 7
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)) mod 𝑃) = 0) |
152 | | oveq1 7190 |
. . . . . . . . . . 11
⊢ (𝑗 = ((𝑃 − (𝑟 · 𝐼)) mod 𝑃) → (𝑗 · 𝑁) = (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)) |
153 | 152 | oveq2d 7199 |
. . . . . . . . . 10
⊢ (𝑗 = ((𝑃 − (𝑟 · 𝐼)) mod 𝑃) → (𝐼 + (𝑗 · 𝑁)) = (𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁))) |
154 | 153 | oveq1d 7198 |
. . . . . . . . 9
⊢ (𝑗 = ((𝑃 − (𝑟 · 𝐼)) mod 𝑃) → ((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = ((𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)) mod 𝑃)) |
155 | 154 | eqeq1d 2741 |
. . . . . . . 8
⊢ (𝑗 = ((𝑃 − (𝑟 · 𝐼)) mod 𝑃) → (((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0 ↔ ((𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)) mod 𝑃) = 0)) |
156 | 155 | rspcev 3529 |
. . . . . . 7
⊢ ((((𝑃 − (𝑟 · 𝐼)) mod 𝑃) ∈ (0..^𝑃) ∧ ((𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)) mod 𝑃) = 0) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
157 | 17, 151, 156 | syl2anc 587 |
. . . . . 6
⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
158 | 157 | ex 416 |
. . . . 5
⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
159 | 158 | rexlimiva 3192 |
. . . 4
⊢
(∃𝑟 ∈
(1...(𝑃 − 1))((𝑁 · 𝑟) mod 𝑃) = 1 → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
160 | 1, 2, 159 | 3syl 18 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
161 | 160 | 3adant3 1133 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
162 | 161 | pm2.43i 52 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0) |