Metamath Proof Explorer

Theorem pc0

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

Ref Expression
Assertion pc0 
|- ( P e. Prime -> ( P pCnt 0 ) = +oo )

Proof

Step Hyp Ref Expression
1 0z 
 |-  0 e. ZZ
2 zq 
 |-  ( 0 e. ZZ -> 0 e. QQ )
3 1 2 ax-mp 
 |-  0 e. QQ
4 iftrue 
 |-  ( r = 0 -> 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 , < ) ) ) ) ) = +oo )
5 4 adantl 
 |-  ( ( p = P /\ r = 0 ) -> 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 , < ) ) ) ) ) = +oo )
6 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 , < ) ) ) ) ) )
7 pnfex 
 |-  +oo e. _V
8 5 6 7 ovmpoa 
 |-  ( ( P e. Prime /\ 0 e. QQ ) -> ( P pCnt 0 ) = +oo )
9 3 8 mpan2 
 |-  ( P e. Prime -> ( P pCnt 0 ) = +oo )