This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pcprendvds2

Description: Non-divisibility property of the prime power pre-function. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Hypotheses pclem.1 
|- A = { n e. NN0 | ( P ^ n ) || N }
pclem.2 
|- S = sup ( A , RR , < )
Assertion pcprendvds2 
|- ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. P || ( N / ( P ^ S ) ) )

Proof

Step Hyp Ref Expression
1 pclem.1 
 |-  A = { n e. NN0 | ( P ^ n ) || N }
2 pclem.2 
 |-  S = sup ( A , RR , < )
3 1 2 pcprendvds 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. ( P ^ ( S + 1 ) ) || N )
4 eluz2nn 
 |-  ( P e. ( ZZ>= ` 2 ) -> P e. NN )
5 4 adantr 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> P e. NN )
6 5 nnzd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> P e. ZZ )
7 1 2 pcprecl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( S e. NN0 /\ ( P ^ S ) || N ) )
8 7 simprd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ S ) || N )
9 7 simpld 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> S e. NN0 )
10 5 9 nnexpcld 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ S ) e. NN )
11 10 nnzd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ S ) e. ZZ )
12 10 nnne0d 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ S ) =/= 0 )
13 simprl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> N e. ZZ )
14 dvdsval2 
 |-  ( ( ( P ^ S ) e. ZZ /\ ( P ^ S ) =/= 0 /\ N e. ZZ ) -> ( ( P ^ S ) || N <-> ( N / ( P ^ S ) ) e. ZZ ) )
15 11 12 13 14 syl3anc 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( P ^ S ) || N <-> ( N / ( P ^ S ) ) e. ZZ ) )
16 8 15 mpbid 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( N / ( P ^ S ) ) e. ZZ )
17 dvdscmul 
 |-  ( ( P e. ZZ /\ ( N / ( P ^ S ) ) e. ZZ /\ ( P ^ S ) e. ZZ ) -> ( P || ( N / ( P ^ S ) ) -> ( ( P ^ S ) x. P ) || ( ( P ^ S ) x. ( N / ( P ^ S ) ) ) ) )
18 6 16 11 17 syl3anc 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P || ( N / ( P ^ S ) ) -> ( ( P ^ S ) x. P ) || ( ( P ^ S ) x. ( N / ( P ^ S ) ) ) ) )
19 5 nncnd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> P e. CC )
20 19 9 expp1d 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ ( S + 1 ) ) = ( ( P ^ S ) x. P ) )
21 20 eqcomd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( P ^ S ) x. P ) = ( P ^ ( S + 1 ) ) )
22 zcn 
 |-  ( N e. ZZ -> N e. CC )
23 22 ad2antrl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> N e. CC )
24 10 nncnd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ S ) e. CC )
25 23 24 12 divcan2d 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( P ^ S ) x. ( N / ( P ^ S ) ) ) = N )
26 21 25 breq12d 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( ( P ^ S ) x. P ) || ( ( P ^ S ) x. ( N / ( P ^ S ) ) ) <-> ( P ^ ( S + 1 ) ) || N ) )
27 18 26 sylibd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P || ( N / ( P ^ S ) ) -> ( P ^ ( S + 1 ) ) || N ) )
28 3 27 mtod 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. P || ( N / ( P ^ S ) ) )