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 
|- ( N e. ( ZZ>= ` M ) -> ( ( ppi ` N ) - ( ppi ` M ) ) = ( # ` ( ( ( M + 1 ) ... N ) i^i Prime ) ) )

Proof

Step Hyp Ref Expression
1 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
2 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
3 2z 
 |-  2 e. ZZ
4 ifcl 
 |-  ( ( M e. ZZ /\ 2 e. ZZ ) -> if ( M <_ 2 , M , 2 ) e. ZZ )
5 2 3 4 sylancl 
 |-  ( N e. ( ZZ>= ` M ) -> if ( M <_ 2 , M , 2 ) e. ZZ )
6 3 a1i 
 |-  ( N e. ( ZZ>= ` M ) -> 2 e. ZZ )
7 2 zred 
 |-  ( N e. ( ZZ>= ` M ) -> M e. RR )
8 2re 
 |-  2 e. RR
9 min2 
 |-  ( ( M e. RR /\ 2 e. RR ) -> if ( M <_ 2 , M , 2 ) <_ 2 )
10 7 8 9 sylancl 
 |-  ( N e. ( ZZ>= ` M ) -> if ( M <_ 2 , M , 2 ) <_ 2 )
11 eluz2 
 |-  ( 2 e. ( ZZ>= ` if ( M <_ 2 , M , 2 ) ) <-> ( if ( M <_ 2 , M , 2 ) e. ZZ /\ 2 e. ZZ /\ if ( M <_ 2 , M , 2 ) <_ 2 ) )
12 5 6 10 11 syl3anbrc 
 |-  ( N e. ( ZZ>= ` M ) -> 2 e. ( ZZ>= ` if ( M <_ 2 , M , 2 ) ) )
13 ppival2g 
 |-  ( ( N e. ZZ /\ 2 e. ( ZZ>= ` if ( M <_ 2 , M , 2 ) ) ) -> ( ppi ` N ) = ( # ` ( ( if ( M <_ 2 , M , 2 ) ... N ) i^i Prime ) ) )
14 1 12 13 syl2anc 
 |-  ( N e. ( ZZ>= ` M ) -> ( ppi ` N ) = ( # ` ( ( if ( M <_ 2 , M , 2 ) ... N ) i^i Prime ) ) )
15 min1 
 |-  ( ( M e. RR /\ 2 e. RR ) -> if ( M <_ 2 , M , 2 ) <_ M )
16 7 8 15 sylancl 
 |-  ( N e. ( ZZ>= ` M ) -> if ( M <_ 2 , M , 2 ) <_ M )
17 eluz2 
 |-  ( M e. ( ZZ>= ` if ( M <_ 2 , M , 2 ) ) <-> ( if ( M <_ 2 , M , 2 ) e. ZZ /\ M e. ZZ /\ if ( M <_ 2 , M , 2 ) <_ M ) )
18 5 2 16 17 syl3anbrc 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( ZZ>= ` if ( M <_ 2 , M , 2 ) ) )
19 id 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( ZZ>= ` M ) )
20 elfzuzb 
 |-  ( M e. ( if ( M <_ 2 , M , 2 ) ... N ) <-> ( M e. ( ZZ>= ` if ( M <_ 2 , M , 2 ) ) /\ N e. ( ZZ>= ` M ) ) )
21 18 19 20 sylanbrc 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( if ( M <_ 2 , M , 2 ) ... N ) )
22 fzsplit 
 |-  ( M e. ( if ( M <_ 2 , M , 2 ) ... N ) -> ( if ( M <_ 2 , M , 2 ) ... N ) = ( ( if ( M <_ 2 , M , 2 ) ... M ) u. ( ( M + 1 ) ... N ) ) )
23 21 22 syl 
 |-  ( N e. ( ZZ>= ` M ) -> ( if ( M <_ 2 , M , 2 ) ... N ) = ( ( if ( M <_ 2 , M , 2 ) ... M ) u. ( ( M + 1 ) ... N ) ) )
24 23 ineq1d 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( if ( M <_ 2 , M , 2 ) ... N ) i^i Prime ) = ( ( ( if ( M <_ 2 , M , 2 ) ... M ) u. ( ( M + 1 ) ... N ) ) i^i Prime ) )
25 indir 
 |-  ( ( ( if ( M <_ 2 , M , 2 ) ... M ) u. ( ( M + 1 ) ... N ) ) i^i Prime ) = ( ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) u. ( ( ( M + 1 ) ... N ) i^i Prime ) )
26 24 25 eqtrdi 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( if ( M <_ 2 , M , 2 ) ... N ) i^i Prime ) = ( ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) u. ( ( ( M + 1 ) ... N ) i^i Prime ) ) )
27 26 fveq2d 
 |-  ( N e. ( ZZ>= ` M ) -> ( # ` ( ( if ( M <_ 2 , M , 2 ) ... N ) i^i Prime ) ) = ( # ` ( ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) u. ( ( ( M + 1 ) ... N ) i^i Prime ) ) ) )
28 fzfi 
 |-  ( if ( M <_ 2 , M , 2 ) ... M ) e. Fin
29 inss1 
 |-  ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) C_ ( if ( M <_ 2 , M , 2 ) ... M )
30 ssfi 
 |-  ( ( ( if ( M <_ 2 , M , 2 ) ... M ) e. Fin /\ ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) C_ ( if ( M <_ 2 , M , 2 ) ... M ) ) -> ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) e. Fin )
31 28 29 30 mp2an 
 |-  ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) e. Fin
32 fzfi 
 |-  ( ( M + 1 ) ... N ) e. Fin
33 inss1 
 |-  ( ( ( M + 1 ) ... N ) i^i Prime ) C_ ( ( M + 1 ) ... N )
34 ssfi 
 |-  ( ( ( ( M + 1 ) ... N ) e. Fin /\ ( ( ( M + 1 ) ... N ) i^i Prime ) C_ ( ( M + 1 ) ... N ) ) -> ( ( ( M + 1 ) ... N ) i^i Prime ) e. Fin )
35 32 33 34 mp2an 
 |-  ( ( ( M + 1 ) ... N ) i^i Prime ) e. Fin
36 7 ltp1d 
 |-  ( N e. ( ZZ>= ` M ) -> M < ( M + 1 ) )
37 fzdisj 
 |-  ( M < ( M + 1 ) -> ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i ( ( M + 1 ) ... N ) ) = (/) )
38 36 37 syl 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i ( ( M + 1 ) ... N ) ) = (/) )
39 38 ineq1d 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i ( ( M + 1 ) ... N ) ) i^i Prime ) = ( (/) i^i Prime ) )
40 inindir 
 |-  ( ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i ( ( M + 1 ) ... N ) ) i^i Prime ) = ( ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) i^i ( ( ( M + 1 ) ... N ) i^i Prime ) )
41 0in 
 |-  ( (/) i^i Prime ) = (/)
42 39 40 41 3eqtr3g 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) i^i ( ( ( M + 1 ) ... N ) i^i Prime ) ) = (/) )
43 hashun 
 |-  ( ( ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) e. Fin /\ ( ( ( M + 1 ) ... N ) i^i Prime ) e. Fin /\ ( ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) i^i ( ( ( M + 1 ) ... N ) i^i Prime ) ) = (/) ) -> ( # ` ( ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) u. ( ( ( M + 1 ) ... N ) i^i Prime ) ) ) = ( ( # ` ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) ) + ( # ` ( ( ( M + 1 ) ... N ) i^i Prime ) ) ) )
44 31 35 42 43 mp3an12i 
 |-  ( N e. ( ZZ>= ` M ) -> ( # ` ( ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) u. ( ( ( M + 1 ) ... N ) i^i Prime ) ) ) = ( ( # ` ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) ) + ( # ` ( ( ( M + 1 ) ... N ) i^i Prime ) ) ) )
45 14 27 44 3eqtrd 
 |-  ( N e. ( ZZ>= ` M ) -> ( ppi ` N ) = ( ( # ` ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) ) + ( # ` ( ( ( M + 1 ) ... N ) i^i Prime ) ) ) )
46 ppival2g 
 |-  ( ( M e. ZZ /\ 2 e. ( ZZ>= ` if ( M <_ 2 , M , 2 ) ) ) -> ( ppi ` M ) = ( # ` ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) ) )
47 2 12 46 syl2anc 
 |-  ( N e. ( ZZ>= ` M ) -> ( ppi ` M ) = ( # ` ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) ) )
48 45 47 oveq12d 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( ppi ` N ) - ( ppi ` M ) ) = ( ( ( # ` ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) ) + ( # ` ( ( ( M + 1 ) ... N ) i^i Prime ) ) ) - ( # ` ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) ) ) )
49 hashcl 
 |-  ( ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) e. Fin -> ( # ` ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) ) e. NN0 )
50 31 49 ax-mp 
 |-  ( # ` ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) ) e. NN0
51 50 nn0cni 
 |-  ( # ` ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) ) e. CC
52 hashcl 
 |-  ( ( ( ( M + 1 ) ... N ) i^i Prime ) e. Fin -> ( # ` ( ( ( M + 1 ) ... N ) i^i Prime ) ) e. NN0 )
53 35 52 ax-mp 
 |-  ( # ` ( ( ( M + 1 ) ... N ) i^i Prime ) ) e. NN0
54 53 nn0cni 
 |-  ( # ` ( ( ( M + 1 ) ... N ) i^i Prime ) ) e. CC
55 pncan2 
 |-  ( ( ( # ` ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) ) e. CC /\ ( # ` ( ( ( M + 1 ) ... N ) i^i Prime ) ) e. CC ) -> ( ( ( # ` ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) ) + ( # ` ( ( ( M + 1 ) ... N ) i^i Prime ) ) ) - ( # ` ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) ) ) = ( # ` ( ( ( M + 1 ) ... N ) i^i Prime ) ) )
56 51 54 55 mp2an 
 |-  ( ( ( # ` ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) ) + ( # ` ( ( ( M + 1 ) ... N ) i^i Prime ) ) ) - ( # ` ( ( if ( M <_ 2 , M , 2 ) ... M ) i^i Prime ) ) ) = ( # ` ( ( ( M + 1 ) ... N ) i^i Prime ) )
57 48 56 eqtrdi 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( ppi ` N ) - ( ppi ` M ) ) = ( # ` ( ( ( M + 1 ) ... N ) i^i Prime ) ) )