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 ) ... 𝑁 ) ∩ ℙ ) ) )