Proof of Theorem nnnn0modprm0
Step | Hyp | Ref
| Expression |
1 | | prmnn 12057 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
2 | 1 | adantr 274 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 𝑃 ∈ ℕ) |
3 | | fzo0sn0fzo1 10170 |
. . . . 5
⊢ (𝑃 ∈ ℕ →
(0..^𝑃) = ({0} ∪
(1..^𝑃))) |
4 | 2, 3 | syl 14 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (0..^𝑃) = ({0} ∪ (1..^𝑃))) |
5 | 4 | eleq2d 2240 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (𝐼 ∈ (0..^𝑃) ↔ 𝐼 ∈ ({0} ∪ (1..^𝑃)))) |
6 | | elun 3268 |
. . . . 5
⊢ (𝐼 ∈ ({0} ∪ (1..^𝑃)) ↔ (𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑃))) |
7 | | elsni 3599 |
. . . . . . 7
⊢ (𝐼 ∈ {0} → 𝐼 = 0) |
8 | | lbfzo0 10130 |
. . . . . . . . . . . 12
⊢ (0 ∈
(0..^𝑃) ↔ 𝑃 ∈
ℕ) |
9 | 1, 8 | sylibr 133 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℙ → 0 ∈
(0..^𝑃)) |
10 | | elfzoelz 10096 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ (1..^𝑃) → 𝑁 ∈ ℤ) |
11 | | zcn 9210 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
12 | | mul02 8299 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℂ → (0
· 𝑁) =
0) |
13 | 12 | oveq2d 5867 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℂ → (0 + (0
· 𝑁)) = (0 +
0)) |
14 | | 00id 8053 |
. . . . . . . . . . . . . . . 16
⊢ (0 + 0) =
0 |
15 | 13, 14 | eqtrdi 2219 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℂ → (0 + (0
· 𝑁)) =
0) |
16 | 10, 11, 15 | 3syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ (1..^𝑃) → (0 + (0 · 𝑁)) = 0) |
17 | 16 | adantl 275 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (0 + (0 · 𝑁)) = 0) |
18 | 17 | oveq1d 5866 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ((0 + (0 · 𝑁)) mod 𝑃) = (0 mod 𝑃)) |
19 | | nnq 9585 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℚ) |
20 | 1, 19 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℚ) |
21 | 1 | nngt0d 8915 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ → 0 <
𝑃) |
22 | | q0mod 10304 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℚ ∧ 0 <
𝑃) → (0 mod 𝑃) = 0) |
23 | 20, 21, 22 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → (0 mod
𝑃) = 0) |
24 | 23 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (0 mod 𝑃) = 0) |
25 | 18, 24 | eqtrd 2203 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ((0 + (0 · 𝑁)) mod 𝑃) = 0) |
26 | | oveq1 5858 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 0 → (𝑗 · 𝑁) = (0 · 𝑁)) |
27 | 26 | oveq2d 5867 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 0 → (0 + (𝑗 · 𝑁)) = (0 + (0 · 𝑁))) |
28 | 27 | oveq1d 5866 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 0 → ((0 + (𝑗 · 𝑁)) mod 𝑃) = ((0 + (0 · 𝑁)) mod 𝑃)) |
29 | 28 | eqeq1d 2179 |
. . . . . . . . . . . 12
⊢ (𝑗 = 0 → (((0 + (𝑗 · 𝑁)) mod 𝑃) = 0 ↔ ((0 + (0 · 𝑁)) mod 𝑃) = 0)) |
30 | 29 | rspcev 2834 |
. . . . . . . . . . 11
⊢ ((0
∈ (0..^𝑃) ∧ ((0 +
(0 · 𝑁)) mod 𝑃) = 0) → ∃𝑗 ∈ (0..^𝑃)((0 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
31 | 9, 25, 30 | syl2an2r 590 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((0 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
32 | 31 | adantl 275 |
. . . . . . . . 9
⊢ ((𝐼 = 0 ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → ∃𝑗 ∈ (0..^𝑃)((0 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
33 | | oveq1 5858 |
. . . . . . . . . . . . 13
⊢ (𝐼 = 0 → (𝐼 + (𝑗 · 𝑁)) = (0 + (𝑗 · 𝑁))) |
34 | 33 | oveq1d 5866 |
. . . . . . . . . . . 12
⊢ (𝐼 = 0 → ((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = ((0 + (𝑗 · 𝑁)) mod 𝑃)) |
35 | 34 | eqeq1d 2179 |
. . . . . . . . . . 11
⊢ (𝐼 = 0 → (((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0 ↔ ((0 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
36 | 35 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝐼 = 0 ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → (((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0 ↔ ((0 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
37 | 36 | rexbidv 2471 |
. . . . . . . . 9
⊢ ((𝐼 = 0 ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → (∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0 ↔ ∃𝑗 ∈ (0..^𝑃)((0 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
38 | 32, 37 | mpbird 166 |
. . . . . . . 8
⊢ ((𝐼 = 0 ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
39 | 38 | ex 114 |
. . . . . . 7
⊢ (𝐼 = 0 → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
40 | 7, 39 | syl 14 |
. . . . . 6
⊢ (𝐼 ∈ {0} → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
41 | | simpl 108 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 𝑃 ∈ ℙ) |
42 | 41 | adantl 275 |
. . . . . . . 8
⊢ ((𝐼 ∈ (1..^𝑃) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → 𝑃 ∈ ℙ) |
43 | | simprr 527 |
. . . . . . . 8
⊢ ((𝐼 ∈ (1..^𝑃) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → 𝑁 ∈ (1..^𝑃)) |
44 | | simpl 108 |
. . . . . . . 8
⊢ ((𝐼 ∈ (1..^𝑃) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → 𝐼 ∈ (1..^𝑃)) |
45 | | modprm0 12201 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
46 | 42, 43, 44, 45 | syl3anc 1233 |
. . . . . . 7
⊢ ((𝐼 ∈ (1..^𝑃) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃))) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0) |
47 | 46 | ex 114 |
. . . . . 6
⊢ (𝐼 ∈ (1..^𝑃) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
48 | 40, 47 | jaoi 711 |
. . . . 5
⊢ ((𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑃)) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
49 | 6, 48 | sylbi 120 |
. . . 4
⊢ (𝐼 ∈ ({0} ∪ (1..^𝑃)) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
50 | 49 | com12 30 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (𝐼 ∈ ({0} ∪ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
51 | 5, 50 | sylbid 149 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (𝐼 ∈ (0..^𝑃) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) |
52 | 51 | 3impia 1195 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (0..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0) |