Metamath Proof Explorer

Theorem pczpre

Description: Connect the prime count pre-function to the actual prime count function, when restricted to the integers. (Contributed by Mario Carneiro, 23-Feb-2014) (Proof shortened by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypothesis pczpre.1 
|- S = sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < )
Assertion pczpre 
|- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P pCnt N ) = S )

Proof

Step Hyp Ref Expression
1 pczpre.1 
 |-  S = sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < )
2 zq 
 |-  ( N e. ZZ -> N e. QQ )
3 eqid 
 |-  sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < )
4 eqid 
 |-  sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < )
5 3 4 pcval 
 |-  ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> ( P pCnt N ) = ( iota z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) ) )
6 2 5 sylanr1 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P pCnt N ) = ( iota z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) ) )
7 simprl 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> N e. ZZ )
8 7 zcnd 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> N e. CC )
9 8 div1d 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( N / 1 ) = N )
10 9 eqcomd 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> N = ( N / 1 ) )
11 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
12 eqid 
 |-  1 = 1
13 eqid 
 |-  { n e. NN0 | ( P ^ n ) || 1 } = { n e. NN0 | ( P ^ n ) || 1 }
14 eqid 
 |-  sup ( { n e. NN0 | ( P ^ n ) || 1 } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || 1 } , RR , < )
15 13 14 pcpre1 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ 1 = 1 ) -> sup ( { n e. NN0 | ( P ^ n ) || 1 } , RR , < ) = 0 )
16 11 12 15 sylancl 
 |-  ( P e. Prime -> sup ( { n e. NN0 | ( P ^ n ) || 1 } , RR , < ) = 0 )
17 16 adantr 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> sup ( { n e. NN0 | ( P ^ n ) || 1 } , RR , < ) = 0 )
18 17 oveq2d 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( S - sup ( { n e. NN0 | ( P ^ n ) || 1 } , RR , < ) ) = ( S - 0 ) )
19 eqid 
 |-  { n e. NN0 | ( P ^ n ) || N } = { n e. NN0 | ( P ^ n ) || N }
20 19 1 pcprecl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( S e. NN0 /\ ( P ^ S ) || N ) )
21 11 20 sylan 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( S e. NN0 /\ ( P ^ S ) || N ) )
22 21 simpld 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> S e. NN0 )
23 22 nn0cnd 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> S e. CC )
24 23 subid1d 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( S - 0 ) = S )
25 18 24 eqtr2d 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> S = ( S - sup ( { n e. NN0 | ( P ^ n ) || 1 } , RR , < ) ) )
26 1nn 
 |-  1 e. NN
27 oveq1 
 |-  ( x = N -> ( x / y ) = ( N / y ) )
28 27 eqeq2d 
 |-  ( x = N -> ( N = ( x / y ) <-> N = ( N / y ) ) )
29 breq2 
 |-  ( x = N -> ( ( P ^ n ) || x <-> ( P ^ n ) || N ) )
30 29 rabbidv 
 |-  ( x = N -> { n e. NN0 | ( P ^ n ) || x } = { n e. NN0 | ( P ^ n ) || N } )
31 30 supeq1d 
 |-  ( x = N -> sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < ) )
32 31 1 eqtr4di 
 |-  ( x = N -> sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) = S )
33 32 oveq1d 
 |-  ( x = N -> ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) = ( S - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) )
34 33 eqeq2d 
 |-  ( x = N -> ( S = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) <-> S = ( S - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) )
35 28 34 anbi12d 
 |-  ( x = N -> ( ( N = ( x / y ) /\ S = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) <-> ( N = ( N / y ) /\ S = ( S - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) ) )
36 oveq2 
 |-  ( y = 1 -> ( N / y ) = ( N / 1 ) )
37 36 eqeq2d 
 |-  ( y = 1 -> ( N = ( N / y ) <-> N = ( N / 1 ) ) )
38 breq2 
 |-  ( y = 1 -> ( ( P ^ n ) || y <-> ( P ^ n ) || 1 ) )
39 38 rabbidv 
 |-  ( y = 1 -> { n e. NN0 | ( P ^ n ) || y } = { n e. NN0 | ( P ^ n ) || 1 } )
40 39 supeq1d 
 |-  ( y = 1 -> sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || 1 } , RR , < ) )
41 40 oveq2d 
 |-  ( y = 1 -> ( S - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) = ( S - sup ( { n e. NN0 | ( P ^ n ) || 1 } , RR , < ) ) )
42 41 eqeq2d 
 |-  ( y = 1 -> ( S = ( S - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) <-> S = ( S - sup ( { n e. NN0 | ( P ^ n ) || 1 } , RR , < ) ) ) )
43 37 42 anbi12d 
 |-  ( y = 1 -> ( ( N = ( N / y ) /\ S = ( S - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) <-> ( N = ( N / 1 ) /\ S = ( S - sup ( { n e. NN0 | ( P ^ n ) || 1 } , RR , < ) ) ) ) )
44 35 43 rspc2ev 
 |-  ( ( N e. ZZ /\ 1 e. NN /\ ( N = ( N / 1 ) /\ S = ( S - sup ( { n e. NN0 | ( P ^ n ) || 1 } , RR , < ) ) ) ) -> E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ S = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) )
45 26 44 mp3an2 
 |-  ( ( N e. ZZ /\ ( N = ( N / 1 ) /\ S = ( S - sup ( { n e. NN0 | ( P ^ n ) || 1 } , RR , < ) ) ) ) -> E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ S = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) )
46 7 10 25 45 syl12anc 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ S = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) )
47 ltso 
 |-  < Or RR
48 47 supex 
 |-  sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < ) e. _V
49 1 48 eqeltri 
 |-  S e. _V
50 3 4 pceu 
 |-  ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> E! z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) )
51 2 50 sylanr1 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> E! z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) )
52 eqeq1 
 |-  ( z = S -> ( z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) <-> S = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) )
53 52 anbi2d 
 |-  ( z = S -> ( ( N = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) <-> ( N = ( x / y ) /\ S = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) ) )
54 53 2rexbidv 
 |-  ( z = S -> ( E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) <-> E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ S = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) ) )
55 54 iota2 
 |-  ( ( S e. _V /\ E! z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) ) -> ( E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ S = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) <-> ( iota z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) ) = S ) )
56 49 51 55 sylancr 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ S = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) <-> ( iota z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) ) = S ) )
57 46 56 mpbid 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( iota z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) ) = S )
58 6 57 eqtrd 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P pCnt N ) = S )