| Step | Hyp | Ref
| Expression |
| 1 | | fzfi 14013 |
. . . . . . 7
⊢
(1...𝑁) ∈
Fin |
| 2 | | diffi 9215 |
. . . . . . 7
⊢
((1...𝑁) ∈ Fin
→ ((1...𝑁) ∖
{𝑝}) ∈
Fin) |
| 3 | 1, 2 | mp1i 13 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ((1...𝑁) ∖ {𝑝}) ∈ Fin) |
| 4 | | eldifi 4131 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((1...𝑁) ∖ {𝑝}) → 𝑘 ∈ (1...𝑁)) |
| 5 | | elfzelz 13564 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℤ) |
| 6 | 4, 5 | syl 17 |
. . . . . . . 8
⊢ (𝑘 ∈ ((1...𝑁) ∖ {𝑝}) → 𝑘 ∈ ℤ) |
| 7 | | 1zzd 12648 |
. . . . . . . 8
⊢ (𝑘 ∈ ((1...𝑁) ∖ {𝑝}) → 1 ∈ ℤ) |
| 8 | 6, 7 | ifcld 4572 |
. . . . . . 7
⊢ (𝑘 ∈ ((1...𝑁) ∖ {𝑝}) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℤ) |
| 9 | 8 | adantl 481 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) ∧ 𝑘 ∈ ((1...𝑁) ∖ {𝑝})) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℤ) |
| 10 | 3, 9 | fprodzcl 15990 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℤ) |
| 11 | | prmz 16712 |
. . . . . . 7
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
| 12 | 11 | adantl 481 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℤ) |
| 13 | 12 | adantr 480 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∈ ℤ) |
| 14 | | dvdsmul2 16316 |
. . . . 5
⊢
((∏𝑘 ∈
((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℤ ∧ 𝑝 ∈ ℤ) → 𝑝 ∥ (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · 𝑝)) |
| 15 | 10, 13, 14 | syl2anc 584 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∥ (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · 𝑝)) |
| 16 | | nnnn0 12533 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
| 17 | | prmoval 17071 |
. . . . . . . 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 5155 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (𝑝 ∥ (#p‘𝑁) ↔ 𝑝 ∥ ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1))) |
| 21 | | neldifsnd 4793 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ¬ 𝑝 ∈ ((1...𝑁) ∖ {𝑝})) |
| 22 | | disjsn 4711 |
. . . . . . . . 9
⊢
((((1...𝑁) ∖
{𝑝}) ∩ {𝑝}) = ∅ ↔ ¬ 𝑝 ∈ ((1...𝑁) ∖ {𝑝})) |
| 23 | 21, 22 | sylibr 234 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (((1...𝑁) ∖ {𝑝}) ∩ {𝑝}) = ∅) |
| 24 | | prmnn 16711 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
| 25 | 24 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℕ) |
| 26 | 25 | anim1i 615 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝑁)) |
| 27 | | nnz 12634 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
| 28 | | fznn 13632 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → (𝑝 ∈ (1...𝑁) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝑁))) |
| 29 | 27, 28 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑝 ∈ (1...𝑁) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝑁))) |
| 30 | 29 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (𝑝 ∈ (1...𝑁) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝑁))) |
| 31 | 26, 30 | mpbird 257 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∈ (1...𝑁)) |
| 32 | | difsnid 4810 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (1...𝑁) → (((1...𝑁) ∖ {𝑝}) ∪ {𝑝}) = (1...𝑁)) |
| 33 | 32 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝑝 ∈ (1...𝑁) → (1...𝑁) = (((1...𝑁) ∖ {𝑝}) ∪ {𝑝})) |
| 34 | 31, 33 | syl 17 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (1...𝑁) = (((1...𝑁) ∖ {𝑝}) ∪ {𝑝})) |
| 35 | | fzfid 14014 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (1...𝑁) ∈ Fin) |
| 36 | | 1zzd 12648 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑁) → 1 ∈ ℤ) |
| 37 | 5, 36 | ifcld 4572 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...𝑁) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℤ) |
| 38 | 37 | zcnd 12723 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑁) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℂ) |
| 39 | 38 | adantl 481 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) ∧ 𝑘 ∈ (1...𝑁)) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℂ) |
| 40 | 23, 34, 35, 39 | fprodsplit 16002 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) = (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · ∏𝑘 ∈ {𝑝}if(𝑘 ∈ ℙ, 𝑘, 1))) |
| 41 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∈ ℙ) |
| 42 | 25 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∈ ℕ) |
| 43 | 42 | nncnd 12282 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∈ ℂ) |
| 44 | | 1cnd 11256 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 1 ∈ ℂ) |
| 45 | 43, 44 | ifcld 4572 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → if(𝑝 ∈ ℙ, 𝑝, 1) ∈ ℂ) |
| 46 | | eleq1w 2824 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑝 → (𝑘 ∈ ℙ ↔ 𝑝 ∈ ℙ)) |
| 47 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑝 → 𝑘 = 𝑝) |
| 48 | 46, 47 | ifbieq1d 4550 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑝 → if(𝑘 ∈ ℙ, 𝑘, 1) = if(𝑝 ∈ ℙ, 𝑝, 1)) |
| 49 | 48 | prodsn 15998 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℙ ∧ if(𝑝 ∈ ℙ, 𝑝, 1) ∈ ℂ) →
∏𝑘 ∈ {𝑝}if(𝑘 ∈ ℙ, 𝑘, 1) = if(𝑝 ∈ ℙ, 𝑝, 1)) |
| 50 | 41, 45, 49 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ∏𝑘 ∈ {𝑝}if(𝑘 ∈ ℙ, 𝑘, 1) = if(𝑝 ∈ ℙ, 𝑝, 1)) |
| 51 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℙ) |
| 52 | 51 | iftrued 4533 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → if(𝑝 ∈ ℙ, 𝑝, 1) = 𝑝) |
| 53 | 52 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → if(𝑝 ∈ ℙ, 𝑝, 1) = 𝑝) |
| 54 | 50, 53 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ∏𝑘 ∈ {𝑝}if(𝑘 ∈ ℙ, 𝑘, 1) = 𝑝) |
| 55 | 54 | oveq2d 7447 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · ∏𝑘 ∈ {𝑝}if(𝑘 ∈ ℙ, 𝑘, 1)) = (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · 𝑝)) |
| 56 | 40, 55 | eqtrd 2777 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) = (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · 𝑝)) |
| 57 | 56 | breq2d 5155 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (𝑝 ∥ ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) ↔ 𝑝 ∥ (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · 𝑝))) |
| 58 | 20, 57 | bitrd 279 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → (𝑝 ∥ (#p‘𝑁) ↔ 𝑝 ∥ (∏𝑘 ∈ ((1...𝑁) ∖ {𝑝})if(𝑘 ∈ ℙ, 𝑘, 1) · 𝑝))) |
| 59 | 15, 58 | mpbird 257 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝑁) → 𝑝 ∥ (#p‘𝑁)) |
| 60 | 59 | ex 412 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ≤ 𝑁 → 𝑝 ∥ (#p‘𝑁))) |
| 61 | 60 | ralrimiva 3146 |
1
⊢ (𝑁 ∈ ℕ →
∀𝑝 ∈ ℙ
(𝑝 ≤ 𝑁 → 𝑝 ∥ (#p‘𝑁))) |