Proof of Theorem nnnn0modprm0
Step | Hyp | Ref
| Expression |
1 | | prmnn 15767 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
2 | 1 | adantr 474 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 𝑃 ∈ ℕ) |
3 | | fzo0sn0fzo1 12859 |
. . . . 5
⊢ (𝑃 ∈ ℕ →
(0..^𝑃) = ({0} ∪
(1..^𝑃))) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (0..^𝑃) = ({0} ∪ (1..^𝑃))) |
5 | 4 | eleq2d 2892 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (𝐼 ∈ (0..^𝑃) ↔ 𝐼 ∈ ({0} ∪ (1..^𝑃)))) |
6 | | elun 3982 |
. . . . 5
⊢ (𝐼 ∈ ({0} ∪ (1..^𝑃)) ↔ (𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑃))) |
7 | | elsni 4416 |
. . . . . . 7
⊢ (𝐼 ∈ {0} → 𝐼 = 0) |
8 | | lbfzo0 12810 |
. . . . . . . . . . . . 13
⊢ (0 ∈
(0..^𝑃) ↔ 𝑃 ∈
ℕ) |
9 | 1, 8 | sylibr 226 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 0 ∈
(0..^𝑃)) |
10 | 9 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 0 ∈ (0..^𝑃)) |
11 | | elfzoelz 12772 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ (1..^𝑃) → 𝑁 ∈ ℤ) |
12 | | zcn 11716 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
13 | | mul02 10540 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℂ → (0
· 𝑁) =
0) |
14 | 13 | oveq2d 6926 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℂ → (0 + (0
· 𝑁)) = (0 +
0)) |
15 | | 00id 10537 |
. . . . . . . . . . . . . . . 16
⊢ (0 + 0) =
0 |
16 | 14, 15 | syl6eq 2877 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℂ → (0 + (0
· 𝑁)) =
0) |
17 | 11, 12, 16 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ (1..^𝑃) → (0 + (0 · 𝑁)) = 0) |
18 | 17 | adantl 475 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (0 + (0 · 𝑁)) = 0) |
19 | 18 | oveq1d 6925 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ((0 + (0 · 𝑁)) mod 𝑃) = (0 mod 𝑃)) |
20 | | nnrp 12132 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ+) |
21 | | 0mod 13003 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℝ+
→ (0 mod 𝑃) =
0) |
22 | 1, 20, 21 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → (0 mod
𝑃) = 0) |
23 | 22 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (0 mod 𝑃) = 0) |
24 | 19, 23 | eqtrd 2861 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ((0 + (0 · 𝑁)) mod 𝑃) = 0) |
25 | | oveq1 6917 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 0 → (𝑗 · 𝑁) = (0 · 𝑁)) |
26 | 25 | oveq2d 6926 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 0 → (0 + (𝑗 · 𝑁)) = (0 + (0 · 𝑁))) |
27 | 26 | oveq1d 6925 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 0 → ((0 + (𝑗 · 𝑁)) mod 𝑃) = ((0 + (0 · 𝑁)) mod 𝑃)) |
28 | 27 | eqeq1d 2827 |
. . . . . . . . . . . 12
⊢ (𝑗 = 0 → (((0 + (𝑗 · 𝑁)) mod 𝑃) = 0 ↔ ((0 + (0 · 𝑁)) mod 𝑃) = 0)) |
29 | 28 | rspcev 3526 |
. . . . . . . . . . 11
⊢ ((0
∈ (0..^𝑃) ∧ ((0 +
(0 · 𝑁)) mod 𝑃) = 0) → ∃𝑗 ∈ (0..^𝑃)((0 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
30 | 10, 24, 29 | syl2anc 579 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((0 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
31 | 30 | adantl 475 |
. . . . . . . . 9
⊢ ((𝐼 = 0 ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → ∃𝑗 ∈ (0..^𝑃)((0 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
32 | | oveq1 6917 |
. . . . . . . . . . . . 13
⊢ (𝐼 = 0 → (𝐼 + (𝑗 · 𝑁)) = (0 + (𝑗 · 𝑁))) |
33 | 32 | oveq1d 6925 |
. . . . . . . . . . . 12
⊢ (𝐼 = 0 → ((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = ((0 + (𝑗 · 𝑁)) mod 𝑃)) |
34 | 33 | eqeq1d 2827 |
. . . . . . . . . . 11
⊢ (𝐼 = 0 → (((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0 ↔ ((0 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
35 | 34 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝐼 = 0 ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → (((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0 ↔ ((0 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
36 | 35 | rexbidv 3262 |
. . . . . . . . 9
⊢ ((𝐼 = 0 ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → (∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0 ↔ ∃𝑗 ∈ (0..^𝑃)((0 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
37 | 31, 36 | mpbird 249 |
. . . . . . . 8
⊢ ((𝐼 = 0 ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
38 | 37 | ex 403 |
. . . . . . 7
⊢ (𝐼 = 0 → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
39 | 7, 38 | syl 17 |
. . . . . 6
⊢ (𝐼 ∈ {0} → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
40 | | simpl 476 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 𝑃 ∈ ℙ) |
41 | 40 | adantl 475 |
. . . . . . . 8
⊢ ((𝐼 ∈ (1..^𝑃) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → 𝑃 ∈ ℙ) |
42 | | simprr 789 |
. . . . . . . 8
⊢ ((𝐼 ∈ (1..^𝑃) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → 𝑁 ∈ (1..^𝑃)) |
43 | | simpl 476 |
. . . . . . . 8
⊢ ((𝐼 ∈ (1..^𝑃) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → 𝐼 ∈ (1..^𝑃)) |
44 | | modprm0 15888 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
45 | 41, 42, 43, 44 | syl3anc 1494 |
. . . . . . 7
⊢ ((𝐼 ∈ (1..^𝑃) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
46 | 45 | ex 403 |
. . . . . 6
⊢ (𝐼 ∈ (1..^𝑃) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
47 | 39, 46 | jaoi 888 |
. . . . 5
⊢ ((𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑃)) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
48 | 6, 47 | sylbi 209 |
. . . 4
⊢ (𝐼 ∈ ({0} ∪ (1..^𝑃)) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
49 | 48 | com12 32 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (𝐼 ∈ ({0} ∪ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
50 | 5, 49 | sylbid 232 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (𝐼 ∈ (0..^𝑃) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
51 | 50 | 3impia 1149 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (0..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0) |