Metamath Proof Explorer

Theorem pcdvdsb

Description: P ^ A divides N if and only if A is at most the count of P . (Contributed by Mario Carneiro, 3-Oct-2014)

Ref Expression
Assertion pcdvdsb 
|- ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) -> ( A <_ ( P pCnt N ) <-> ( P ^ A ) || N ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( N = 0 -> ( P pCnt N ) = ( P pCnt 0 ) )
2 1 breq2d 
 |-  ( N = 0 -> ( A <_ ( P pCnt N ) <-> A <_ ( P pCnt 0 ) ) )
3 breq2 
 |-  ( N = 0 -> ( ( P ^ A ) || N <-> ( P ^ A ) || 0 ) )
4 2 3 bibi12d 
 |-  ( N = 0 -> ( ( A <_ ( P pCnt N ) <-> ( P ^ A ) || N ) <-> ( A <_ ( P pCnt 0 ) <-> ( P ^ A ) || 0 ) ) )
5 simpl3 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> A e. NN0 )
6 5 nn0zd 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> A e. ZZ )
7 simpl1 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> P e. Prime )
8 simpl2 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> N e. ZZ )
9 simpr 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> N =/= 0 )
10 pczcl 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P pCnt N ) e. NN0 )
11 7 8 9 10 syl12anc 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( P pCnt N ) e. NN0 )
12 11 nn0zd 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( P pCnt N ) e. ZZ )
13 eluz 
 |-  ( ( A e. ZZ /\ ( P pCnt N ) e. ZZ ) -> ( ( P pCnt N ) e. ( ZZ>= ` A ) <-> A <_ ( P pCnt N ) ) )
14 6 12 13 syl2anc 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( ( P pCnt N ) e. ( ZZ>= ` A ) <-> A <_ ( P pCnt N ) ) )
15 prmnn 
 |-  ( P e. Prime -> P e. NN )
16 7 15 syl 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> P e. NN )
17 16 nnzd 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> P e. ZZ )
18 dvdsexp 
 |-  ( ( P e. ZZ /\ A e. NN0 /\ ( P pCnt N ) e. ( ZZ>= ` A ) ) -> ( P ^ A ) || ( P ^ ( P pCnt N ) ) )
19 18 3expia 
 |-  ( ( P e. ZZ /\ A e. NN0 ) -> ( ( P pCnt N ) e. ( ZZ>= ` A ) -> ( P ^ A ) || ( P ^ ( P pCnt N ) ) ) )
20 17 5 19 syl2anc 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( ( P pCnt N ) e. ( ZZ>= ` A ) -> ( P ^ A ) || ( P ^ ( P pCnt N ) ) ) )
21 14 20 sylbird 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( A <_ ( P pCnt N ) -> ( P ^ A ) || ( P ^ ( P pCnt N ) ) ) )
22 pczdvds 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ ( P pCnt N ) ) || N )
23 7 8 9 22 syl12anc 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( P ^ ( P pCnt N ) ) || N )
24 nnexpcl 
 |-  ( ( P e. NN /\ A e. NN0 ) -> ( P ^ A ) e. NN )
25 15 24 sylan 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> ( P ^ A ) e. NN )
26 25 3adant2 
 |-  ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) -> ( P ^ A ) e. NN )
27 26 nnzd 
 |-  ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) -> ( P ^ A ) e. ZZ )
28 27 adantr 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( P ^ A ) e. ZZ )
29 16 11 nnexpcld 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( P ^ ( P pCnt N ) ) e. NN )
30 29 nnzd 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( P ^ ( P pCnt N ) ) e. ZZ )
31 dvdstr 
 |-  ( ( ( P ^ A ) e. ZZ /\ ( P ^ ( P pCnt N ) ) e. ZZ /\ N e. ZZ ) -> ( ( ( P ^ A ) || ( P ^ ( P pCnt N ) ) /\ ( P ^ ( P pCnt N ) ) || N ) -> ( P ^ A ) || N ) )
32 28 30 8 31 syl3anc 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( ( ( P ^ A ) || ( P ^ ( P pCnt N ) ) /\ ( P ^ ( P pCnt N ) ) || N ) -> ( P ^ A ) || N ) )
33 23 32 mpan2d 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( ( P ^ A ) || ( P ^ ( P pCnt N ) ) -> ( P ^ A ) || N ) )
34 21 33 syld 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( A <_ ( P pCnt N ) -> ( P ^ A ) || N ) )
35 nn0re 
 |-  ( ( P pCnt N ) e. NN0 -> ( P pCnt N ) e. RR )
36 nn0re 
 |-  ( A e. NN0 -> A e. RR )
37 ltnle 
 |-  ( ( ( P pCnt N ) e. RR /\ A e. RR ) -> ( ( P pCnt N ) < A <-> -. A <_ ( P pCnt N ) ) )
38 35 36 37 syl2an 
 |-  ( ( ( P pCnt N ) e. NN0 /\ A e. NN0 ) -> ( ( P pCnt N ) < A <-> -. A <_ ( P pCnt N ) ) )
39 nn0ltp1le 
 |-  ( ( ( P pCnt N ) e. NN0 /\ A e. NN0 ) -> ( ( P pCnt N ) < A <-> ( ( P pCnt N ) + 1 ) <_ A ) )
40 38 39 bitr3d 
 |-  ( ( ( P pCnt N ) e. NN0 /\ A e. NN0 ) -> ( -. A <_ ( P pCnt N ) <-> ( ( P pCnt N ) + 1 ) <_ A ) )
41 11 5 40 syl2anc 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( -. A <_ ( P pCnt N ) <-> ( ( P pCnt N ) + 1 ) <_ A ) )
42 peano2nn0 
 |-  ( ( P pCnt N ) e. NN0 -> ( ( P pCnt N ) + 1 ) e. NN0 )
43 11 42 syl 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( ( P pCnt N ) + 1 ) e. NN0 )
44 43 nn0zd 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( ( P pCnt N ) + 1 ) e. ZZ )
45 eluz 
 |-  ( ( ( ( P pCnt N ) + 1 ) e. ZZ /\ A e. ZZ ) -> ( A e. ( ZZ>= ` ( ( P pCnt N ) + 1 ) ) <-> ( ( P pCnt N ) + 1 ) <_ A ) )
46 44 6 45 syl2anc 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( A e. ( ZZ>= ` ( ( P pCnt N ) + 1 ) ) <-> ( ( P pCnt N ) + 1 ) <_ A ) )
47 dvdsexp 
 |-  ( ( P e. ZZ /\ ( ( P pCnt N ) + 1 ) e. NN0 /\ A e. ( ZZ>= ` ( ( P pCnt N ) + 1 ) ) ) -> ( P ^ ( ( P pCnt N ) + 1 ) ) || ( P ^ A ) )
48 47 3expia 
 |-  ( ( P e. ZZ /\ ( ( P pCnt N ) + 1 ) e. NN0 ) -> ( A e. ( ZZ>= ` ( ( P pCnt N ) + 1 ) ) -> ( P ^ ( ( P pCnt N ) + 1 ) ) || ( P ^ A ) ) )
49 17 43 48 syl2anc 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( A e. ( ZZ>= ` ( ( P pCnt N ) + 1 ) ) -> ( P ^ ( ( P pCnt N ) + 1 ) ) || ( P ^ A ) ) )
50 46 49 sylbird 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( ( ( P pCnt N ) + 1 ) <_ A -> ( P ^ ( ( P pCnt N ) + 1 ) ) || ( P ^ A ) ) )
51 pczndvds 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. ( P ^ ( ( P pCnt N ) + 1 ) ) || N )
52 7 8 9 51 syl12anc 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> -. ( P ^ ( ( P pCnt N ) + 1 ) ) || N )
53 16 43 nnexpcld 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( P ^ ( ( P pCnt N ) + 1 ) ) e. NN )
54 53 nnzd 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( P ^ ( ( P pCnt N ) + 1 ) ) e. ZZ )
55 dvdstr 
 |-  ( ( ( P ^ ( ( P pCnt N ) + 1 ) ) e. ZZ /\ ( P ^ A ) e. ZZ /\ N e. ZZ ) -> ( ( ( P ^ ( ( P pCnt N ) + 1 ) ) || ( P ^ A ) /\ ( P ^ A ) || N ) -> ( P ^ ( ( P pCnt N ) + 1 ) ) || N ) )
56 54 28 8 55 syl3anc 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( ( ( P ^ ( ( P pCnt N ) + 1 ) ) || ( P ^ A ) /\ ( P ^ A ) || N ) -> ( P ^ ( ( P pCnt N ) + 1 ) ) || N ) )
57 52 56 mtod 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> -. ( ( P ^ ( ( P pCnt N ) + 1 ) ) || ( P ^ A ) /\ ( P ^ A ) || N ) )
58 imnan 
 |-  ( ( ( P ^ ( ( P pCnt N ) + 1 ) ) || ( P ^ A ) -> -. ( P ^ A ) || N ) <-> -. ( ( P ^ ( ( P pCnt N ) + 1 ) ) || ( P ^ A ) /\ ( P ^ A ) || N ) )
59 57 58 sylibr 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( ( P ^ ( ( P pCnt N ) + 1 ) ) || ( P ^ A ) -> -. ( P ^ A ) || N ) )
60 50 59 syld 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( ( ( P pCnt N ) + 1 ) <_ A -> -. ( P ^ A ) || N ) )
61 41 60 sylbid 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( -. A <_ ( P pCnt N ) -> -. ( P ^ A ) || N ) )
62 34 61 impcon4bid 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) /\ N =/= 0 ) -> ( A <_ ( P pCnt N ) <-> ( P ^ A ) || N ) )
63 36 3ad2ant3 
 |-  ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) -> A e. RR )
64 63 rexrd 
 |-  ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) -> A e. RR* )
65 pnfge 
 |-  ( A e. RR* -> A <_ +oo )
66 64 65 syl 
 |-  ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) -> A <_ +oo )
67 pc0 
 |-  ( P e. Prime -> ( P pCnt 0 ) = +oo )
68 67 3ad2ant1 
 |-  ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) -> ( P pCnt 0 ) = +oo )
69 66 68 breqtrrd 
 |-  ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) -> A <_ ( P pCnt 0 ) )
70 dvds0 
 |-  ( ( P ^ A ) e. ZZ -> ( P ^ A ) || 0 )
71 27 70 syl 
 |-  ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) -> ( P ^ A ) || 0 )
72 69 71 2thd 
 |-  ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) -> ( A <_ ( P pCnt 0 ) <-> ( P ^ A ) || 0 ) )
73 4 62 72 pm2.61ne 
 |-  ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) -> ( A <_ ( P pCnt N ) <-> ( P ^ A ) || N ) )