Step | Hyp | Ref
| Expression |
1 | | fzfi 13433 |
. . . . . . 7
⊢
(1...𝑁) ∈
Fin |
2 | | diffi 8829 |
. . . . . . 7
⊢
((1...𝑁) ∈ Fin
→ ((1...𝑁) ∖
{𝑝}) ∈
Fin) |
3 | 1, 2 | mp1i 13 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ((1...𝑁) ∖ {𝑝}) ∈ Fin) |
4 | | eldifi 4017 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((1...𝑁) ∖ {𝑝}) → 𝑘 ∈ (1...𝑁)) |
5 | | elfzelz 13000 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℤ) |
6 | 4, 5 | syl 17 |
. . . . . . . 8
⊢ (𝑘 ∈ ((1...𝑁) ∖ {𝑝}) → 𝑘 ∈ ℤ) |
7 | | 1zzd 12096 |
. . . . . . . 8
⊢ (𝑘 ∈ ((1...𝑁) ∖ {𝑝}) → 1 ∈ ℤ) |
8 | 6, 7 | ifcld 4460 |
. . . . . . 7
⊢ (𝑘 ∈ ((1...𝑁) ∖ {𝑝}) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℤ) |
9 | 8 | adantl 485 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) ∧ 𝑘 ∈ ((1...𝑁) ∖ {𝑝})) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℤ) |
10 | 3, 9 | fprodzcl 15402 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℤ) |
11 | | prmz 16118 |
. . . . . . 7
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
12 | 11 | adantl 485 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℤ) |
13 | 12 | adantr 484 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∈ ℤ) |
14 | | dvdsmul2 15726 |
. . . . 5
⊢
((∏𝑘 ∈
((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℤ ∧ 𝑝 ∈ ℤ) → 𝑝 ∥ (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · 𝑝)) |
15 | 10, 13, 14 | syl2anc 587 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∥ (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · 𝑝)) |
16 | | nnnn0 11985 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
17 | | prmoval 16471 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (#p‘𝑁) = ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1)) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(#p‘𝑁) =
∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1)) |
19 | 18 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (#p‘𝑁) = ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1)) |
20 | 19 | breq2d 5042 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (𝑝 ∥ (#p‘𝑁) ↔ 𝑝 ∥ ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1))) |
21 | | neldifsnd 4681 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ¬ 𝑝 ∈ ((1...𝑁) ∖ {𝑝})) |
22 | | disjsn 4602 |
. . . . . . . . 9
⊢
((((1...𝑁) ∖
{𝑝}) ∩ {𝑝}) = ∅ ↔ ¬ 𝑝 ∈ ((1...𝑁) ∖ {𝑝})) |
23 | 21, 22 | sylibr 237 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (((1...𝑁) ∖ {𝑝}) ∩ {𝑝}) = ∅) |
24 | | prmnn 16117 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
25 | 24 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℕ) |
26 | 25 | anim1i 618 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝑁)) |
27 | | nnz 12087 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
28 | | fznn 13068 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → (𝑝 ∈ (1...𝑁) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝑁))) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑝 ∈ (1...𝑁) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝑁))) |
30 | 29 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (𝑝 ∈ (1...𝑁) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝑁))) |
31 | 26, 30 | mpbird 260 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∈ (1...𝑁)) |
32 | | difsnid 4698 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (1...𝑁) → (((1...𝑁) ∖ {𝑝}) ∪ {𝑝}) = (1...𝑁)) |
33 | 32 | eqcomd 2744 |
. . . . . . . . 9
⊢ (𝑝 ∈ (1...𝑁) → (1...𝑁) = (((1...𝑁) ∖ {𝑝}) ∪ {𝑝})) |
34 | 31, 33 | syl 17 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (1...𝑁) = (((1...𝑁) ∖ {𝑝}) ∪ {𝑝})) |
35 | | fzfid 13434 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (1...𝑁) ∈ Fin) |
36 | | 1zzd 12096 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑁) → 1 ∈ ℤ) |
37 | 5, 36 | ifcld 4460 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...𝑁) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℤ) |
38 | 37 | zcnd 12171 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑁) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℂ) |
39 | 38 | adantl 485 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) ∧ 𝑘 ∈ (1...𝑁)) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℂ) |
40 | 23, 34, 35, 39 | fprodsplit 15414 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) = (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · ∏𝑘 ∈ {𝑝}if(𝑘 ∈ ℙ, 𝑘, 1))) |
41 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∈ ℙ) |
42 | 25 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∈ ℕ) |
43 | 42 | nncnd 11734 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∈ ℂ) |
44 | | 1cnd 10716 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 1 ∈ ℂ) |
45 | 43, 44 | ifcld 4460 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → if(𝑝 ∈ ℙ, 𝑝, 1) ∈ ℂ) |
46 | | eleq1w 2815 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑝 → (𝑘 ∈ ℙ ↔ 𝑝 ∈ ℙ)) |
47 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑝 → 𝑘 = 𝑝) |
48 | 46, 47 | ifbieq1d 4438 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑝 → if(𝑘 ∈ ℙ, 𝑘, 1) = if(𝑝 ∈ ℙ, 𝑝, 1)) |
49 | 48 | prodsn 15410 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℙ ∧ if(𝑝 ∈ ℙ, 𝑝, 1) ∈ ℂ) →
∏𝑘 ∈ {𝑝}if(𝑘 ∈ ℙ, 𝑘, 1) = if(𝑝 ∈ ℙ, 𝑝, 1)) |
50 | 41, 45, 49 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ∏𝑘 ∈ {𝑝}if(𝑘 ∈ ℙ, 𝑘, 1) = if(𝑝 ∈ ℙ, 𝑝, 1)) |
51 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℙ) |
52 | 51 | iftrued 4422 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → if(𝑝 ∈ ℙ, 𝑝, 1) = 𝑝) |
53 | 52 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → if(𝑝 ∈ ℙ, 𝑝, 1) = 𝑝) |
54 | 50, 53 | eqtrd 2773 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ∏𝑘 ∈ {𝑝}if(𝑘 ∈ ℙ, 𝑘, 1) = 𝑝) |
55 | 54 | oveq2d 7188 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · ∏𝑘 ∈ {𝑝}if(𝑘 ∈ ℙ, 𝑘, 1)) = (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · 𝑝)) |
56 | 40, 55 | eqtrd 2773 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) = (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · 𝑝)) |
57 | 56 | breq2d 5042 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (𝑝 ∥ ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) ↔ 𝑝 ∥ (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · 𝑝))) |
58 | 20, 57 | bitrd 282 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (𝑝 ∥ (#p‘𝑁) ↔ 𝑝 ∥ (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · 𝑝))) |
59 | 15, 58 | mpbird 260 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∥ (#p‘𝑁)) |
60 | 59 | ex 416 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ≤ 𝑁 → 𝑝 ∥ (#p‘𝑁))) |
61 | 60 | ralrimiva 3096 |
1
⊢ (𝑁 ∈ ℕ →
∀𝑝 ∈ ℙ
(𝑝 ≤ 𝑁 → 𝑝 ∥ (#p‘𝑁))) |