Metamath Proof Explorer

Theorem ppidif

Description: The difference of the prime-counting function ppi at two points counts the number of primes in an interval. (Contributed by Mario Carneiro, 21-Sep-2014)

Ref Expression
Assertion ppidif ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( π ‘ 𝑁 ) − ( π ‘ 𝑀 ) ) = ( ♯ ‘ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ) )

Proof

Step Hyp Ref Expression
1 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
2 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
3 2z ⊢ 2 ∈ ℤ
4 ifcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 2 ∈ ℤ ) → if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ∈ ℤ )
5 2 3 4 sylancl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ∈ ℤ )
6 3 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 2 ∈ ℤ )
7 2 zred ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℝ )
8 2re ⊢ 2 ∈ ℝ
9 min2 ⊢ ( ( 𝑀 ∈ ℝ ∧ 2 ∈ ℝ ) → if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ≤ 2 )
10 7 8 9 sylancl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ≤ 2 )
11 eluz2 ⊢ ( 2 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ) ↔ ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ∈ ℤ ∧ 2 ∈ ℤ ∧ if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ≤ 2 ) )
12 5 6 10 11 syl3anbrc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 2 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ) )
13 ppival2g ⊢ ( ( 𝑁 ∈ ℤ ∧ 2 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ) ) → ( π ‘ 𝑁 ) = ( ♯ ‘ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑁 ) ∩ ℙ ) ) )
14 1 12 13 syl2anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( π ‘ 𝑁 ) = ( ♯ ‘ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑁 ) ∩ ℙ ) ) )
15 min1 ⊢ ( ( 𝑀 ∈ ℝ ∧ 2 ∈ ℝ ) → if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ≤ 𝑀 )
16 7 8 15 sylancl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ≤ 𝑀 )
17 eluz2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ) ↔ ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ≤ 𝑀 ) )
18 5 2 16 17 syl3anbrc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ) )
19 id ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
20 elfzuzb ⊢ ( 𝑀 ∈ ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑁 ) ↔ ( 𝑀 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
21 18 19 20 sylanbrc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑁 ) )
22 fzsplit ⊢ ( 𝑀 ∈ ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑁 ) → ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑁 ) = ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
23 21 22 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑁 ) = ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
24 23 ineq1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑁 ) ∩ ℙ ) = ( ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ∩ ℙ ) )
25 indir ⊢ ( ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ∩ ℙ ) = ( ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ∪ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) )
26 24 25 eqtrdi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑁 ) ∩ ℙ ) = ( ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ∪ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ) )
27 26 fveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ♯ ‘ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑁 ) ∩ ℙ ) ) = ( ♯ ‘ ( ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ∪ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ) ) )
28 fzfi ⊢ ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∈ Fin
29 inss1 ⊢ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ⊆ ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 )
30 ssfi ⊢ ( ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∈ Fin ∧ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ⊆ ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ) → ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ∈ Fin )
31 28 29 30 mp2an ⊢ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ∈ Fin
32 fzfi ⊢ ( ( 𝑀 + 1 ) ... 𝑁 ) ∈ Fin
33 inss1 ⊢ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ⊆ ( ( 𝑀 + 1 ) ... 𝑁 )
34 ssfi ⊢ ( ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∈ Fin ∧ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ⊆ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ∈ Fin )
35 32 33 34 mp2an ⊢ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ∈ Fin
36 7 ltp1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 < ( 𝑀 + 1 ) )
37 fzdisj ⊢ ( 𝑀 < ( 𝑀 + 1 ) → ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ∅ )
38 36 37 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ∅ )
39 38 ineq1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ∩ ℙ ) = ( ∅ ∩ ℙ ) )
40 inindir ⊢ ( ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ∩ ℙ ) = ( ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ∩ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) )
41 0in ⊢ ( ∅ ∩ ℙ ) = ∅
42 39 40 41 3eqtr3g ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ∩ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ) = ∅ )
43 hashun ⊢ ( ( ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ∈ Fin ∧ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ∈ Fin ∧ ( ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ∩ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ) = ∅ ) → ( ♯ ‘ ( ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ∪ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ) ) = ( ( ♯ ‘ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ) + ( ♯ ‘ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ) ) )
44 31 35 42 43 mp3an12i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ♯ ‘ ( ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ∪ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ) ) = ( ( ♯ ‘ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ) + ( ♯ ‘ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ) ) )
45 14 27 44 3eqtrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( π ‘ 𝑁 ) = ( ( ♯ ‘ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ) + ( ♯ ‘ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ) ) )
46 ppival2g ⊢ ( ( 𝑀 ∈ ℤ ∧ 2 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ) ) → ( π ‘ 𝑀 ) = ( ♯ ‘ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ) )
47 2 12 46 syl2anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( π ‘ 𝑀 ) = ( ♯ ‘ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ) )
48 45 47 oveq12d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( π ‘ 𝑁 ) − ( π ‘ 𝑀 ) ) = ( ( ( ♯ ‘ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ) + ( ♯ ‘ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ) ) − ( ♯ ‘ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ) ) )
49 hashcl ⊢ ( ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ∈ Fin → ( ♯ ‘ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ) ∈ ℕ0 )
50 31 49 ax-mp ⊢ ( ♯ ‘ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ) ∈ ℕ0
51 50 nn0cni ⊢ ( ♯ ‘ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ) ∈ ℂ
52 hashcl ⊢ ( ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ∈ Fin → ( ♯ ‘ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ) ∈ ℕ0 )
53 35 52 ax-mp ⊢ ( ♯ ‘ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ) ∈ ℕ0
54 53 nn0cni ⊢ ( ♯ ‘ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ) ∈ ℂ
55 pncan2 ⊢ ( ( ( ♯ ‘ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ) ∈ ℂ ∧ ( ♯ ‘ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ) ∈ ℂ ) → ( ( ( ♯ ‘ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ) + ( ♯ ‘ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ) ) − ( ♯ ‘ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ) ) = ( ♯ ‘ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ) )
56 51 54 55 mp2an ⊢ ( ( ( ♯ ‘ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ) + ( ♯ ‘ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ) ) − ( ♯ ‘ ( ( if ( 𝑀 ≤ 2 , 𝑀 , 2 ) ... 𝑀 ) ∩ ℙ ) ) ) = ( ♯ ‘ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) )
57 48 56 eqtrdi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( π ‘ 𝑁 ) − ( π ‘ 𝑀 ) ) = ( ♯ ‘ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ) )