Proof of Theorem ppidif
Step | Hyp | Ref
| Expression |
1 | | eluzelz 11573 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
2 | | eluzel2 11568 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
3 | | 2z 11286 |
. . . . . . 7
⊢ 2 ∈
ℤ |
4 | | ifcl 4080 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 2 ∈
ℤ) → if(𝑀 ≤
2, 𝑀, 2) ∈
ℤ) |
5 | 2, 3, 4 | sylancl 693 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → if(𝑀 ≤ 2, 𝑀, 2) ∈ ℤ) |
6 | 3 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 2 ∈ ℤ) |
7 | 2 | zred 11358 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℝ) |
8 | | 2re 10967 |
. . . . . . 7
⊢ 2 ∈
ℝ |
9 | | min2 11895 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 2 ∈
ℝ) → if(𝑀 ≤
2, 𝑀, 2) ≤
2) |
10 | 7, 8, 9 | sylancl 693 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → if(𝑀 ≤ 2, 𝑀, 2) ≤ 2) |
11 | | eluz2 11569 |
. . . . . 6
⊢ (2 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2)) ↔ (if(𝑀 ≤ 2, 𝑀, 2) ∈ ℤ ∧ 2 ∈ ℤ
∧ if(𝑀 ≤ 2, 𝑀, 2) ≤ 2)) |
12 | 5, 6, 10, 11 | syl3anbrc 1239 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 2 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2))) |
13 | | ppival2g 24655 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 2 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2))) → (π‘𝑁) = (#‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ))) |
14 | 1, 12, 13 | syl2anc 691 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (π‘𝑁) = (#‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ))) |
15 | | min1 11894 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℝ ∧ 2 ∈
ℝ) → if(𝑀 ≤
2, 𝑀, 2) ≤ 𝑀) |
16 | 7, 8, 15 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → if(𝑀 ≤ 2, 𝑀, 2) ≤ 𝑀) |
17 | | eluz2 11569 |
. . . . . . . . . 10
⊢ (𝑀 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2)) ↔ (if(𝑀 ≤ 2, 𝑀, 2) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ if(𝑀 ≤ 2, 𝑀, 2) ≤ 𝑀)) |
18 | 5, 2, 16, 17 | syl3anbrc 1239 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2))) |
19 | | id 22 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (ℤ≥‘𝑀)) |
20 | | elfzuzb 12207 |
. . . . . . . . 9
⊢ (𝑀 ∈ (if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ↔ (𝑀 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2)) ∧ 𝑁 ∈ (ℤ≥‘𝑀))) |
21 | 18, 19, 20 | sylanbrc 695 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (if(𝑀 ≤ 2, 𝑀, 2)...𝑁)) |
22 | | fzsplit 12238 |
. . . . . . . 8
⊢ (𝑀 ∈ (if(𝑀 ≤ 2, 𝑀, 2)...𝑁) → (if(𝑀 ≤ 2, 𝑀, 2)...𝑁) = ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∪ ((𝑀 + 1)...𝑁))) |
23 | 21, 22 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (if(𝑀 ≤ 2, 𝑀, 2)...𝑁) = ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∪ ((𝑀 + 1)...𝑁))) |
24 | 23 | ineq1d 3775 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ) = (((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∩ ℙ)) |
25 | | indir 3834 |
. . . . . 6
⊢
(((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∩ ℙ) = (((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∪ (((𝑀 + 1)...𝑁) ∩ ℙ)) |
26 | 24, 25 | syl6eq 2660 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ) = (((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∪ (((𝑀 + 1)...𝑁) ∩ ℙ))) |
27 | 26 | fveq2d 6107 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (#‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ)) = (#‘(((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∪ (((𝑀 + 1)...𝑁) ∩ ℙ)))) |
28 | 7 | ltp1d 10833 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 < (𝑀 + 1)) |
29 | | fzdisj 12239 |
. . . . . . . 8
⊢ (𝑀 < (𝑀 + 1) → ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅) |
30 | 28, 29 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅) |
31 | 30 | ineq1d 3775 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ((𝑀 + 1)...𝑁)) ∩ ℙ) = (∅ ∩
ℙ)) |
32 | | inindir 3793 |
. . . . . 6
⊢
(((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∩ ((𝑀 + 1)...𝑁)) ∩ ℙ) = (((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∩ (((𝑀 + 1)...𝑁) ∩ ℙ)) |
33 | | 0in 3921 |
. . . . . 6
⊢ (∅
∩ ℙ) = ∅ |
34 | 31, 32, 33 | 3eqtr3g 2667 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∩ (((𝑀 + 1)...𝑁) ∩ ℙ)) =
∅) |
35 | | fzfi 12633 |
. . . . . . 7
⊢ (if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∈ Fin |
36 | | inss1 3795 |
. . . . . . 7
⊢
((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ⊆ (if(𝑀 ≤ 2, 𝑀, 2)...𝑀) |
37 | | ssfi 8065 |
. . . . . . 7
⊢
(((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∈ Fin ∧ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ⊆ (if(𝑀 ≤ 2, 𝑀, 2)...𝑀)) → ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∈
Fin) |
38 | 35, 36, 37 | mp2an 704 |
. . . . . 6
⊢
((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∈ Fin |
39 | | fzfi 12633 |
. . . . . . 7
⊢ ((𝑀 + 1)...𝑁) ∈ Fin |
40 | | inss1 3795 |
. . . . . . 7
⊢ (((𝑀 + 1)...𝑁) ∩ ℙ) ⊆ ((𝑀 + 1)...𝑁) |
41 | | ssfi 8065 |
. . . . . . 7
⊢ ((((𝑀 + 1)...𝑁) ∈ Fin ∧ (((𝑀 + 1)...𝑁) ∩ ℙ) ⊆ ((𝑀 + 1)...𝑁)) → (((𝑀 + 1)...𝑁) ∩ ℙ) ∈
Fin) |
42 | 39, 40, 41 | mp2an 704 |
. . . . . 6
⊢ (((𝑀 + 1)...𝑁) ∩ ℙ) ∈ Fin |
43 | | hashun 13032 |
. . . . . 6
⊢
((((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∩ ℙ) ∈ Fin ∧ (((𝑀 + 1)...𝑁) ∩ ℙ) ∈ Fin ∧
(((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∩ (((𝑀 + 1)...𝑁) ∩ ℙ)) = ∅) →
(#‘(((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∩ ℙ) ∪ (((𝑀 + 1)...𝑁) ∩ ℙ))) = ((#‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)) + (#‘(((𝑀 + 1)...𝑁) ∩ ℙ)))) |
44 | 38, 42, 43 | mp3an12 1406 |
. . . . 5
⊢
((((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∩ ℙ) ∩ (((𝑀 + 1)...𝑁) ∩ ℙ)) = ∅ →
(#‘(((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∩ ℙ) ∪ (((𝑀 + 1)...𝑁) ∩ ℙ))) = ((#‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)) + (#‘(((𝑀 + 1)...𝑁) ∩ ℙ)))) |
45 | 34, 44 | syl 17 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (#‘(((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∪ (((𝑀 + 1)...𝑁) ∩ ℙ))) = ((#‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)) + (#‘(((𝑀 + 1)...𝑁) ∩ ℙ)))) |
46 | 14, 27, 45 | 3eqtrd 2648 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (π‘𝑁) = ((#‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)) + (#‘(((𝑀 + 1)...𝑁) ∩ ℙ)))) |
47 | | ppival2g 24655 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 2 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2))) → (π‘𝑀) = (#‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ))) |
48 | 2, 12, 47 | syl2anc 691 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (π‘𝑀) = (#‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ))) |
49 | 46, 48 | oveq12d 6567 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((π‘𝑁) −
(π‘𝑀)) =
(((#‘((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∩ ℙ)) + (#‘(((𝑀 + 1)...𝑁) ∩ ℙ))) −
(#‘((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∩ ℙ)))) |
50 | | hashcl 13009 |
. . . . 5
⊢
(((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∩ ℙ) ∈ Fin →
(#‘((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∩ ℙ)) ∈
ℕ0) |
51 | 38, 50 | ax-mp 5 |
. . . 4
⊢
(#‘((if(𝑀 ≤
2, 𝑀, 2)...𝑀) ∩ ℙ)) ∈
ℕ0 |
52 | 51 | nn0cni 11181 |
. . 3
⊢
(#‘((if(𝑀 ≤
2, 𝑀, 2)...𝑀) ∩ ℙ)) ∈
ℂ |
53 | | hashcl 13009 |
. . . . 5
⊢ ((((𝑀 + 1)...𝑁) ∩ ℙ) ∈ Fin →
(#‘(((𝑀 + 1)...𝑁) ∩ ℙ)) ∈
ℕ0) |
54 | 42, 53 | ax-mp 5 |
. . . 4
⊢
(#‘(((𝑀 +
1)...𝑁) ∩ ℙ))
∈ ℕ0 |
55 | 54 | nn0cni 11181 |
. . 3
⊢
(#‘(((𝑀 +
1)...𝑁) ∩ ℙ))
∈ ℂ |
56 | | pncan2 10167 |
. . 3
⊢
(((#‘((if(𝑀
≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)) ∈ ℂ
∧ (#‘(((𝑀 +
1)...𝑁) ∩ ℙ))
∈ ℂ) → (((#‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)) + (#‘(((𝑀 + 1)...𝑁) ∩ ℙ))) −
(#‘((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∩ ℙ))) = (#‘(((𝑀 + 1)...𝑁) ∩ ℙ))) |
57 | 52, 55, 56 | mp2an 704 |
. 2
⊢
(((#‘((if(𝑀
≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)) +
(#‘(((𝑀 + 1)...𝑁) ∩ ℙ))) −
(#‘((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∩ ℙ))) = (#‘(((𝑀 + 1)...𝑁) ∩ ℙ)) |
58 | 49, 57 | syl6eq 2660 |
1
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((π‘𝑁) −
(π‘𝑀)) =
(#‘(((𝑀 + 1)...𝑁) ∩
ℙ))) |