Metamath Proof Explorer

Theorem pczndvds2

Description: The remainder after dividing out all factors of P is not divisible by P . (Contributed by Mario Carneiro, 9-Sep-2014)

Ref Expression
Assertion pczndvds2 
|- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. P || ( N / ( P ^ ( P pCnt N ) ) ) )

Proof

Step Hyp Ref Expression
1 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
2 eqid 
 |-  { n e. NN0 | ( P ^ n ) || N } = { n e. NN0 | ( P ^ n ) || N }
3 eqid 
 |-  sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < )
4 2 3 pcprendvds2 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. P || ( N / ( P ^ sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < ) ) ) )
5 1 4 sylan 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. P || ( N / ( P ^ sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < ) ) ) )
6 3 pczpre 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P pCnt N ) = sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < ) )
7 6 oveq2d 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ ( P pCnt N ) ) = ( P ^ sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < ) ) )
8 7 oveq2d 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( N / ( P ^ ( P pCnt N ) ) ) = ( N / ( P ^ sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < ) ) ) )
9 8 breq2d 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P || ( N / ( P ^ ( P pCnt N ) ) ) <-> P || ( N / ( P ^ sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < ) ) ) ) )
10 5 9 mtbird 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. P || ( N / ( P ^ ( P pCnt N ) ) ) )