Step | Hyp | Ref
| Expression |
1 | | fzfi 13692 |
. . . . . . 7
⊢
(1...𝑁) ∈
Fin |
2 | | diffi 8962 |
. . . . . . 7
⊢
((1...𝑁) ∈ Fin
→ ((1...𝑁) ∖
{𝑝}) ∈
Fin) |
3 | 1, 2 | mp1i 13 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ((1...𝑁) ∖ {𝑝}) ∈ Fin) |
4 | | eldifi 4061 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((1...𝑁) ∖ {𝑝}) → 𝑘 ∈ (1...𝑁)) |
5 | | elfzelz 13256 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℤ) |
6 | 4, 5 | syl 17 |
. . . . . . . 8
⊢ (𝑘 ∈ ((1...𝑁) ∖ {𝑝}) → 𝑘 ∈ ℤ) |
7 | | 1zzd 12351 |
. . . . . . . 8
⊢ (𝑘 ∈ ((1...𝑁) ∖ {𝑝}) → 1 ∈ ℤ) |
8 | 6, 7 | ifcld 4505 |
. . . . . . 7
⊢ (𝑘 ∈ ((1...𝑁) ∖ {𝑝}) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℤ) |
9 | 8 | adantl 482 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) ∧ 𝑘 ∈ ((1...𝑁) ∖ {𝑝})) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℤ) |
10 | 3, 9 | fprodzcl 15664 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℤ) |
11 | | prmz 16380 |
. . . . . . 7
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
12 | 11 | adantl 482 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℤ) |
13 | 12 | adantr 481 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∈ ℤ) |
14 | | dvdsmul2 15988 |
. . . . 5
⊢
((∏𝑘 ∈
((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℤ ∧ 𝑝 ∈ ℤ) → 𝑝 ∥ (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · 𝑝)) |
15 | 10, 13, 14 | syl2anc 584 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∥ (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · 𝑝)) |
16 | | nnnn0 12240 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
17 | | prmoval 16734 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (#p‘𝑁) = ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1)) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(#p‘𝑁) =
∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1)) |
19 | 18 | ad2antrr 723 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (#p‘𝑁) = ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1)) |
20 | 19 | breq2d 5086 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (𝑝 ∥ (#p‘𝑁) ↔ 𝑝 ∥ ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1))) |
21 | | neldifsnd 4726 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ¬ 𝑝 ∈ ((1...𝑁) ∖ {𝑝})) |
22 | | disjsn 4647 |
. . . . . . . . 9
⊢
((((1...𝑁) ∖
{𝑝}) ∩ {𝑝}) = ∅ ↔ ¬ 𝑝 ∈ ((1...𝑁) ∖ {𝑝})) |
23 | 21, 22 | sylibr 233 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (((1...𝑁) ∖ {𝑝}) ∩ {𝑝}) = ∅) |
24 | | prmnn 16379 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
25 | 24 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℕ) |
26 | 25 | anim1i 615 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝑁)) |
27 | | nnz 12342 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
28 | | fznn 13324 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → (𝑝 ∈ (1...𝑁) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝑁))) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑝 ∈ (1...𝑁) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝑁))) |
30 | 29 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (𝑝 ∈ (1...𝑁) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝑁))) |
31 | 26, 30 | mpbird 256 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∈ (1...𝑁)) |
32 | | difsnid 4743 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (1...𝑁) → (((1...𝑁) ∖ {𝑝}) ∪ {𝑝}) = (1...𝑁)) |
33 | 32 | eqcomd 2744 |
. . . . . . . . 9
⊢ (𝑝 ∈ (1...𝑁) → (1...𝑁) = (((1...𝑁) ∖ {𝑝}) ∪ {𝑝})) |
34 | 31, 33 | syl 17 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (1...𝑁) = (((1...𝑁) ∖ {𝑝}) ∪ {𝑝})) |
35 | | fzfid 13693 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (1...𝑁) ∈ Fin) |
36 | | 1zzd 12351 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑁) → 1 ∈ ℤ) |
37 | 5, 36 | ifcld 4505 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...𝑁) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℤ) |
38 | 37 | zcnd 12427 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑁) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℂ) |
39 | 38 | adantl 482 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) ∧ 𝑘 ∈ (1...𝑁)) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℂ) |
40 | 23, 34, 35, 39 | fprodsplit 15676 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) = (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · ∏𝑘 ∈ {𝑝}if(𝑘 ∈ ℙ, 𝑘, 1))) |
41 | | simplr 766 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∈ ℙ) |
42 | 25 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∈ ℕ) |
43 | 42 | nncnd 11989 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∈ ℂ) |
44 | | 1cnd 10970 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 1 ∈ ℂ) |
45 | 43, 44 | ifcld 4505 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → if(𝑝 ∈ ℙ, 𝑝, 1) ∈ ℂ) |
46 | | eleq1w 2821 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑝 → (𝑘 ∈ ℙ ↔ 𝑝 ∈ ℙ)) |
47 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑝 → 𝑘 = 𝑝) |
48 | 46, 47 | ifbieq1d 4483 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑝 → if(𝑘 ∈ ℙ, 𝑘, 1) = if(𝑝 ∈ ℙ, 𝑝, 1)) |
49 | 48 | prodsn 15672 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℙ ∧ if(𝑝 ∈ ℙ, 𝑝, 1) ∈ ℂ) →
∏𝑘 ∈ {𝑝}if(𝑘 ∈ ℙ, 𝑘, 1) = if(𝑝 ∈ ℙ, 𝑝, 1)) |
50 | 41, 45, 49 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ∏𝑘 ∈ {𝑝}if(𝑘 ∈ ℙ, 𝑘, 1) = if(𝑝 ∈ ℙ, 𝑝, 1)) |
51 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℙ) |
52 | 51 | iftrued 4467 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → if(𝑝 ∈ ℙ, 𝑝, 1) = 𝑝) |
53 | 52 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → if(𝑝 ∈ ℙ, 𝑝, 1) = 𝑝) |
54 | 50, 53 | eqtrd 2778 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ∏𝑘 ∈ {𝑝}if(𝑘 ∈ ℙ, 𝑘, 1) = 𝑝) |
55 | 54 | oveq2d 7291 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · ∏𝑘 ∈ {𝑝}if(𝑘 ∈ ℙ, 𝑘, 1)) = (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · 𝑝)) |
56 | 40, 55 | eqtrd 2778 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) = (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · 𝑝)) |
57 | 56 | breq2d 5086 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (𝑝 ∥ ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) ↔ 𝑝 ∥ (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · 𝑝))) |
58 | 20, 57 | bitrd 278 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (𝑝 ∥ (#p‘𝑁) ↔ 𝑝 ∥ (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · 𝑝))) |
59 | 15, 58 | mpbird 256 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∥ (#p‘𝑁)) |
60 | 59 | ex 413 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ≤ 𝑁 → 𝑝 ∥ (#p‘𝑁))) |
61 | 60 | ralrimiva 3103 |
1
⊢ (𝑁 ∈ ℕ →
∀𝑝 ∈ ℙ
(𝑝 ≤ 𝑁 → 𝑝 ∥ (#p‘𝑁))) |