Metamath Proof Explorer

Theorem pcval

Description: The value of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014) (Revised by Mario Carneiro, 3-Oct-2014)

Ref Expression
Hypotheses pcval.1 
|- S = sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < )
pcval.2 
|- T = sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < )
Assertion 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 = ( S - T ) ) ) )

Proof

Step Hyp Ref Expression
1 pcval.1 
 |-  S = sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < )
2 pcval.2 
 |-  T = sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < )
3 simpr 
 |-  ( ( p = P /\ r = N ) -> r = N )
4 3 eqeq1d 
 |-  ( ( p = P /\ r = N ) -> ( r = 0 <-> N = 0 ) )
5 eqeq1 
 |-  ( r = N -> ( r = ( x / y ) <-> N = ( x / y ) ) )
6 oveq1 
 |-  ( p = P -> ( p ^ n ) = ( P ^ n ) )
7 6 breq1d 
 |-  ( p = P -> ( ( p ^ n ) || x <-> ( P ^ n ) || x ) )
8 7 rabbidv 
 |-  ( p = P -> { n e. NN0 | ( p ^ n ) || x } = { n e. NN0 | ( P ^ n ) || x } )
9 8 supeq1d 
 |-  ( p = P -> sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) )
10 9 1 eqtr4di 
 |-  ( p = P -> sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) = S )
11 6 breq1d 
 |-  ( p = P -> ( ( p ^ n ) || y <-> ( P ^ n ) || y ) )
12 11 rabbidv 
 |-  ( p = P -> { n e. NN0 | ( p ^ n ) || y } = { n e. NN0 | ( P ^ n ) || y } )
13 12 supeq1d 
 |-  ( p = P -> sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) )
14 13 2 eqtr4di 
 |-  ( p = P -> sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) = T )
15 10 14 oveq12d 
 |-  ( p = P -> ( sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) ) = ( S - T ) )
16 15 eqeq2d 
 |-  ( p = P -> ( z = ( sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) ) <-> z = ( S - T ) ) )
17 5 16 bi2anan9r 
 |-  ( ( p = P /\ r = N ) -> ( ( r = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) ) ) <-> ( N = ( x / y ) /\ z = ( S - T ) ) ) )
18 17 2rexbidv 
 |-  ( ( p = P /\ r = N ) -> ( E. x e. ZZ E. y e. NN ( r = ( 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 ) /\ z = ( S - T ) ) ) )
19 18 iotabidv 
 |-  ( ( p = P /\ r = N ) -> ( iota z E. x e. ZZ E. y e. NN ( r = ( x / y ) /\ z = ( 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 = ( S - T ) ) ) )
20 4 19 ifbieq2d 
 |-  ( ( p = P /\ r = N ) -> if ( r = 0 , +oo , ( iota z E. x e. ZZ E. y e. NN ( r = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) ) ) ) ) = if ( N = 0 , +oo , ( iota z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) ) ) )
21 df-pc 
 |-  pCnt = ( p e. Prime , r e. QQ |-> if ( r = 0 , +oo , ( iota z E. x e. ZZ E. y e. NN ( r = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) ) ) ) ) )
22 pnfex 
 |-  +oo e. _V
23 iotaex 
 |-  ( iota z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) ) e. _V
24 22 23 ifex 
 |-  if ( N = 0 , +oo , ( iota z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) ) ) e. _V
25 20 21 24 ovmpoa 
 |-  ( ( P e. Prime /\ N e. QQ ) -> ( P pCnt N ) = if ( N = 0 , +oo , ( iota z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) ) ) )
26 ifnefalse 
 |-  ( N =/= 0 -> if ( N = 0 , +oo , ( iota z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) ) ) = ( iota z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) ) )
27 25 26 sylan9eq 
 |-  ( ( ( 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 = ( S - T ) ) ) )
28 27 anasss 
 |-  ( ( 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 = ( S - T ) ) ) )