Proof of Theorem ppidif
Step | Hyp | Ref
| Expression |
1 | | eluzelz 11810 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
2 | | eluzel2 11805 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
3 | | 2z 11522 |
. . . . . . 7
⊢ 2 ∈
ℤ |
4 | | ifcl 4238 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 2 ∈
ℤ) → if(𝑀 ≤
2, 𝑀, 2) ∈
ℤ) |
5 | 2, 3, 4 | sylancl 697 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → if(𝑀 ≤ 2, 𝑀, 2) ∈ ℤ) |
6 | 3 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 2 ∈ ℤ) |
7 | 2 | zred 11595 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℝ) |
8 | | 2re 11203 |
. . . . . . 7
⊢ 2 ∈
ℝ |
9 | | min2 12135 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 2 ∈
ℝ) → if(𝑀 ≤
2, 𝑀, 2) ≤
2) |
10 | 7, 8, 9 | sylancl 697 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → if(𝑀 ≤ 2, 𝑀, 2) ≤ 2) |
11 | | eluz2 11806 |
. . . . . 6
⊢ (2 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2)) ↔ (if(𝑀 ≤ 2, 𝑀, 2) ∈ ℤ ∧ 2 ∈ ℤ
∧ if(𝑀 ≤ 2, 𝑀, 2) ≤ 2)) |
12 | 5, 6, 10, 11 | syl3anbrc 1383 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 2 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2))) |
13 | | ppival2g 24975 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 2 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2))) → (π‘𝑁) = (♯‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ))) |
14 | 1, 12, 13 | syl2anc 696 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (π‘𝑁) = (♯‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ))) |
15 | | min1 12134 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℝ ∧ 2 ∈
ℝ) → if(𝑀 ≤
2, 𝑀, 2) ≤ 𝑀) |
16 | 7, 8, 15 | sylancl 697 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → if(𝑀 ≤ 2, 𝑀, 2) ≤ 𝑀) |
17 | | eluz2 11806 |
. . . . . . . . . 10
⊢ (𝑀 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2)) ↔ (if(𝑀 ≤ 2, 𝑀, 2) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ if(𝑀 ≤ 2, 𝑀, 2) ≤ 𝑀)) |
18 | 5, 2, 16, 17 | syl3anbrc 1383 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2))) |
19 | | id 22 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (ℤ≥‘𝑀)) |
20 | | elfzuzb 12450 |
. . . . . . . . 9
⊢ (𝑀 ∈ (if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ↔ (𝑀 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2)) ∧ 𝑁 ∈ (ℤ≥‘𝑀))) |
21 | 18, 19, 20 | sylanbrc 701 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (if(𝑀 ≤ 2, 𝑀, 2)...𝑁)) |
22 | | fzsplit 12481 |
. . . . . . . 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 3921 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ) = (((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∩ ℙ)) |
25 | | indir 3983 |
. . . . . 6
⊢
(((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∩ ℙ) = (((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∪ (((𝑀 + 1)...𝑁) ∩ ℙ)) |
26 | 24, 25 | syl6eq 2774 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ) = (((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∪ (((𝑀 + 1)...𝑁) ∩ ℙ))) |
27 | 26 | fveq2d 6308 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (♯‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ)) =
(♯‘(((if(𝑀 ≤
2, 𝑀, 2)...𝑀) ∩ ℙ) ∪ (((𝑀 + 1)...𝑁) ∩ ℙ)))) |
28 | 7 | ltp1d 11067 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 < (𝑀 + 1)) |
29 | | fzdisj 12482 |
. . . . . . . 8
⊢ (𝑀 < (𝑀 + 1) → ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅) |
30 | 28, 29 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅) |
31 | 30 | ineq1d 3921 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ((𝑀 + 1)...𝑁)) ∩ ℙ) = (∅ ∩
ℙ)) |
32 | | inindir 3939 |
. . . . . 6
⊢
(((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∩ ((𝑀 + 1)...𝑁)) ∩ ℙ) = (((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∩ (((𝑀 + 1)...𝑁) ∩ ℙ)) |
33 | | 0in 4077 |
. . . . . 6
⊢ (∅
∩ ℙ) = ∅ |
34 | 31, 32, 33 | 3eqtr3g 2781 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∩ (((𝑀 + 1)...𝑁) ∩ ℙ)) =
∅) |
35 | | fzfi 12886 |
. . . . . . 7
⊢ (if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∈ Fin |
36 | | inss1 3941 |
. . . . . . 7
⊢
((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ⊆ (if(𝑀 ≤ 2, 𝑀, 2)...𝑀) |
37 | | ssfi 8296 |
. . . . . . 7
⊢
(((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∈ Fin ∧ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ⊆ (if(𝑀 ≤ 2, 𝑀, 2)...𝑀)) → ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∈
Fin) |
38 | 35, 36, 37 | mp2an 710 |
. . . . . 6
⊢
((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∈ Fin |
39 | | fzfi 12886 |
. . . . . . 7
⊢ ((𝑀 + 1)...𝑁) ∈ Fin |
40 | | inss1 3941 |
. . . . . . 7
⊢ (((𝑀 + 1)...𝑁) ∩ ℙ) ⊆ ((𝑀 + 1)...𝑁) |
41 | | ssfi 8296 |
. . . . . . 7
⊢ ((((𝑀 + 1)...𝑁) ∈ Fin ∧ (((𝑀 + 1)...𝑁) ∩ ℙ) ⊆ ((𝑀 + 1)...𝑁)) → (((𝑀 + 1)...𝑁) ∩ ℙ) ∈
Fin) |
42 | 39, 40, 41 | mp2an 710 |
. . . . . 6
⊢ (((𝑀 + 1)...𝑁) ∩ ℙ) ∈ Fin |
43 | | hashun 13284 |
. . . . . 6
⊢
((((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∩ ℙ) ∈ Fin ∧ (((𝑀 + 1)...𝑁) ∩ ℙ) ∈ Fin ∧
(((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∩ (((𝑀 + 1)...𝑁) ∩ ℙ)) = ∅) →
(♯‘(((if(𝑀 ≤
2, 𝑀, 2)...𝑀) ∩ ℙ) ∪ (((𝑀 + 1)...𝑁) ∩ ℙ))) =
((♯‘((if(𝑀 ≤
2, 𝑀, 2)...𝑀) ∩ ℙ)) +
(♯‘(((𝑀 +
1)...𝑁) ∩
ℙ)))) |
44 | 38, 42, 43 | mp3an12 1527 |
. . . . 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 2762 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (π‘𝑁) = ((♯‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)) + (♯‘(((𝑀 + 1)...𝑁) ∩ ℙ)))) |
47 | | ppival2g 24975 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 2 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2))) → (π‘𝑀) = (♯‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ))) |
48 | 2, 12, 47 | syl2anc 696 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (π‘𝑀) = (♯‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ))) |
49 | 46, 48 | oveq12d 6783 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((π‘𝑁) −
(π‘𝑀)) =
(((♯‘((if(𝑀
≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)) +
(♯‘(((𝑀 +
1)...𝑁) ∩ ℙ)))
− (♯‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)))) |
50 | | hashcl 13260 |
. . . . 5
⊢
(((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∩ ℙ) ∈ Fin →
(♯‘((if(𝑀 ≤
2, 𝑀, 2)...𝑀) ∩ ℙ)) ∈
ℕ0) |
51 | 38, 50 | ax-mp 5 |
. . . 4
⊢
(♯‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)) ∈
ℕ0 |
52 | 51 | nn0cni 11417 |
. . 3
⊢
(♯‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)) ∈
ℂ |
53 | | hashcl 13260 |
. . . . 5
⊢ ((((𝑀 + 1)...𝑁) ∩ ℙ) ∈ Fin →
(♯‘(((𝑀 +
1)...𝑁) ∩ ℙ))
∈ ℕ0) |
54 | 42, 53 | ax-mp 5 |
. . . 4
⊢
(♯‘(((𝑀
+ 1)...𝑁) ∩ ℙ))
∈ ℕ0 |
55 | 54 | nn0cni 11417 |
. . 3
⊢
(♯‘(((𝑀
+ 1)...𝑁) ∩ ℙ))
∈ ℂ |
56 | | pncan2 10401 |
. . 3
⊢
(((♯‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)) ∈ ℂ ∧
(♯‘(((𝑀 +
1)...𝑁) ∩ ℙ))
∈ ℂ) → (((♯‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)) + (♯‘(((𝑀 + 1)...𝑁) ∩ ℙ))) −
(♯‘((if(𝑀 ≤
2, 𝑀, 2)...𝑀) ∩ ℙ))) =
(♯‘(((𝑀 +
1)...𝑁) ∩
ℙ))) |
57 | 52, 55, 56 | mp2an 710 |
. 2
⊢
(((♯‘((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)) + (♯‘(((𝑀 + 1)...𝑁) ∩ ℙ))) −
(♯‘((if(𝑀 ≤
2, 𝑀, 2)...𝑀) ∩ ℙ))) =
(♯‘(((𝑀 +
1)...𝑁) ∩
ℙ)) |
58 | 49, 57 | syl6eq 2774 |
1
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((π‘𝑁) −
(π‘𝑀)) =
(♯‘(((𝑀 +
1)...𝑁) ∩
ℙ))) |