Proof of Theorem nnnn0modprm0
Step | Hyp | Ref
| Expression |
1 | | prmnn 16379 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
2 | 1 | adantr 481 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 𝑃 ∈ ℕ) |
3 | | fzo0sn0fzo1 13476 |
. . . . 5
⊢ (𝑃 ∈ ℕ →
(0..^𝑃) = ({0} ∪
(1..^𝑃))) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (0..^𝑃) = ({0} ∪ (1..^𝑃))) |
5 | 4 | eleq2d 2824 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (𝐼 ∈ (0..^𝑃) ↔ 𝐼 ∈ ({0} ∪ (1..^𝑃)))) |
6 | | elun 4083 |
. . . . 5
⊢ (𝐼 ∈ ({0} ∪ (1..^𝑃)) ↔ (𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑃))) |
7 | | elsni 4578 |
. . . . . . 7
⊢ (𝐼 ∈ {0} → 𝐼 = 0) |
8 | | lbfzo0 13427 |
. . . . . . . . . . . 12
⊢ (0 ∈
(0..^𝑃) ↔ 𝑃 ∈
ℕ) |
9 | 1, 8 | sylibr 233 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℙ → 0 ∈
(0..^𝑃)) |
10 | | elfzoelz 13387 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ (1..^𝑃) → 𝑁 ∈ ℤ) |
11 | | zcn 12324 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
12 | | mul02 11153 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℂ → (0
· 𝑁) =
0) |
13 | 12 | oveq2d 7291 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℂ → (0 + (0
· 𝑁)) = (0 +
0)) |
14 | | 00id 11150 |
. . . . . . . . . . . . . . . 16
⊢ (0 + 0) =
0 |
15 | 13, 14 | eqtrdi 2794 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℂ → (0 + (0
· 𝑁)) =
0) |
16 | 10, 11, 15 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ (1..^𝑃) → (0 + (0 · 𝑁)) = 0) |
17 | 16 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (0 + (0 · 𝑁)) = 0) |
18 | 17 | oveq1d 7290 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ((0 + (0 · 𝑁)) mod 𝑃) = (0 mod 𝑃)) |
19 | | nnrp 12741 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ+) |
20 | | 0mod 13622 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℝ+
→ (0 mod 𝑃) =
0) |
21 | 1, 19, 20 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → (0 mod
𝑃) = 0) |
22 | 21 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (0 mod 𝑃) = 0) |
23 | 18, 22 | eqtrd 2778 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ((0 + (0 · 𝑁)) mod 𝑃) = 0) |
24 | | oveq1 7282 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 0 → (𝑗 · 𝑁) = (0 · 𝑁)) |
25 | 24 | oveq2d 7291 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 0 → (0 + (𝑗 · 𝑁)) = (0 + (0 · 𝑁))) |
26 | 25 | oveq1d 7290 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 0 → ((0 + (𝑗 · 𝑁)) mod 𝑃) = ((0 + (0 · 𝑁)) mod 𝑃)) |
27 | 26 | eqeq1d 2740 |
. . . . . . . . . . . 12
⊢ (𝑗 = 0 → (((0 + (𝑗 · 𝑁)) mod 𝑃) = 0 ↔ ((0 + (0 · 𝑁)) mod 𝑃) = 0)) |
28 | 27 | rspcev 3561 |
. . . . . . . . . . 11
⊢ ((0
∈ (0..^𝑃) ∧ ((0 +
(0 · 𝑁)) mod 𝑃) = 0) → ∃𝑗 ∈ (0..^𝑃)((0 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
29 | 9, 23, 28 | syl2an2r 682 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((0 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
30 | 29 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐼 = 0 ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → ∃𝑗 ∈ (0..^𝑃)((0 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
31 | | oveq1 7282 |
. . . . . . . . . . . . 13
⊢ (𝐼 = 0 → (𝐼 + (𝑗 · 𝑁)) = (0 + (𝑗 · 𝑁))) |
32 | 31 | oveq1d 7290 |
. . . . . . . . . . . 12
⊢ (𝐼 = 0 → ((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = ((0 + (𝑗 · 𝑁)) mod 𝑃)) |
33 | 32 | eqeq1d 2740 |
. . . . . . . . . . 11
⊢ (𝐼 = 0 → (((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0 ↔ ((0 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
34 | 33 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐼 = 0 ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → (((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0 ↔ ((0 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
35 | 34 | rexbidv 3226 |
. . . . . . . . 9
⊢ ((𝐼 = 0 ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → (∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0 ↔ ∃𝑗 ∈ (0..^𝑃)((0 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
36 | 30, 35 | mpbird 256 |
. . . . . . . 8
⊢ ((𝐼 = 0 ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
37 | 36 | ex 413 |
. . . . . . 7
⊢ (𝐼 = 0 → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
38 | 7, 37 | syl 17 |
. . . . . 6
⊢ (𝐼 ∈ {0} → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
39 | | simpl 483 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 𝑃 ∈ ℙ) |
40 | 39 | adantl 482 |
. . . . . . . 8
⊢ ((𝐼 ∈ (1..^𝑃) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → 𝑃 ∈ ℙ) |
41 | | simprr 770 |
. . . . . . . 8
⊢ ((𝐼 ∈ (1..^𝑃) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → 𝑁 ∈ (1..^𝑃)) |
42 | | simpl 483 |
. . . . . . . 8
⊢ ((𝐼 ∈ (1..^𝑃) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → 𝐼 ∈ (1..^𝑃)) |
43 | | modprm0 16506 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
44 | 40, 41, 42, 43 | syl3anc 1370 |
. . . . . . 7
⊢ ((𝐼 ∈ (1..^𝑃) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
45 | 44 | ex 413 |
. . . . . 6
⊢ (𝐼 ∈ (1..^𝑃) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
46 | 38, 45 | jaoi 854 |
. . . . 5
⊢ ((𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑃)) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
47 | 6, 46 | sylbi 216 |
. . . 4
⊢ (𝐼 ∈ ({0} ∪ (1..^𝑃)) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
48 | 47 | com12 32 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (𝐼 ∈ ({0} ∪ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
49 | 5, 48 | sylbid 239 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (𝐼 ∈ (0..^𝑃) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
50 | 49 | 3impia 1116 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (0..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0) |