Metamath Proof Explorer

Theorem pcmptdvds

Description: The partial products of the prime power map form a divisibility chain. (Contributed by Mario Carneiro, 12-Mar-2014)

Ref Expression
Hypotheses pcmpt.1 
|- F = ( n e. NN |-> if ( n e. Prime , ( n ^ A ) , 1 ) )
pcmpt.2 
|- ( ph -> A. n e. Prime A e. NN0 )
pcmpt.3 
|- ( ph -> N e. NN )
pcmptdvds.3 
|- ( ph -> M e. ( ZZ>= ` N ) )
Assertion pcmptdvds 
|- ( ph -> ( seq 1 ( x. , F ) ` N ) || ( seq 1 ( x. , F ) ` M ) )

Proof

Step Hyp Ref Expression
1 pcmpt.1 
 |-  F = ( n e. NN |-> if ( n e. Prime , ( n ^ A ) , 1 ) )
2 pcmpt.2 
 |-  ( ph -> A. n e. Prime A e. NN0 )
3 pcmpt.3 
 |-  ( ph -> N e. NN )
4 pcmptdvds.3 
 |-  ( ph -> M e. ( ZZ>= ` N ) )
5 nfv 
 |-  F/ m A e. NN0
6 nfcsb1v 
 |-  F/_ n [_ m / n ]_ A
7 6 nfel1 
 |-  F/ n [_ m / n ]_ A e. NN0
8 csbeq1a 
 |-  ( n = m -> A = [_ m / n ]_ A )
9 8 eleq1d 
 |-  ( n = m -> ( A e. NN0 <-> [_ m / n ]_ A e. NN0 ) )
10 5 7 9 cbvralw 
 |-  ( A. n e. Prime A e. NN0 <-> A. m e. Prime [_ m / n ]_ A e. NN0 )
11 2 10 sylib 
 |-  ( ph -> A. m e. Prime [_ m / n ]_ A e. NN0 )
12 csbeq1 
 |-  ( m = p -> [_ m / n ]_ A = [_ p / n ]_ A )
13 12 eleq1d 
 |-  ( m = p -> ( [_ m / n ]_ A e. NN0 <-> [_ p / n ]_ A e. NN0 ) )
14 13 rspcv 
 |-  ( p e. Prime -> ( A. m e. Prime [_ m / n ]_ A e. NN0 -> [_ p / n ]_ A e. NN0 ) )
15 11 14 mpan9 
 |-  ( ( ph /\ p e. Prime ) -> [_ p / n ]_ A e. NN0 )
16 15 nn0ge0d 
 |-  ( ( ph /\ p e. Prime ) -> 0 <_ [_ p / n ]_ A )
17 0le0 
 |-  0 <_ 0
18 breq2 
 |-  ( [_ p / n ]_ A = if ( ( p <_ M /\ -. p <_ N ) , [_ p / n ]_ A , 0 ) -> ( 0 <_ [_ p / n ]_ A <-> 0 <_ if ( ( p <_ M /\ -. p <_ N ) , [_ p / n ]_ A , 0 ) ) )
19 breq2 
 |-  ( 0 = if ( ( p <_ M /\ -. p <_ N ) , [_ p / n ]_ A , 0 ) -> ( 0 <_ 0 <-> 0 <_ if ( ( p <_ M /\ -. p <_ N ) , [_ p / n ]_ A , 0 ) ) )
20 18 19 ifboth 
 |-  ( ( 0 <_ [_ p / n ]_ A /\ 0 <_ 0 ) -> 0 <_ if ( ( p <_ M /\ -. p <_ N ) , [_ p / n ]_ A , 0 ) )
21 16 17 20 sylancl 
 |-  ( ( ph /\ p e. Prime ) -> 0 <_ if ( ( p <_ M /\ -. p <_ N ) , [_ p / n ]_ A , 0 ) )
22 nfcv 
 |-  F/_ m if ( n e. Prime , ( n ^ A ) , 1 )
23 nfv 
 |-  F/ n m e. Prime
24 nfcv 
 |-  F/_ n m
25 nfcv 
 |-  F/_ n ^
26 24 25 6 nfov 
 |-  F/_ n ( m ^ [_ m / n ]_ A )
27 nfcv 
 |-  F/_ n 1
28 23 26 27 nfif 
 |-  F/_ n if ( m e. Prime , ( m ^ [_ m / n ]_ A ) , 1 )
29 eleq1w 
 |-  ( n = m -> ( n e. Prime <-> m e. Prime ) )
30 id 
 |-  ( n = m -> n = m )
31 30 8 oveq12d 
 |-  ( n = m -> ( n ^ A ) = ( m ^ [_ m / n ]_ A ) )
32 29 31 ifbieq1d 
 |-  ( n = m -> if ( n e. Prime , ( n ^ A ) , 1 ) = if ( m e. Prime , ( m ^ [_ m / n ]_ A ) , 1 ) )
33 22 28 32 cbvmpt 
 |-  ( n e. NN |-> if ( n e. Prime , ( n ^ A ) , 1 ) ) = ( m e. NN |-> if ( m e. Prime , ( m ^ [_ m / n ]_ A ) , 1 ) )
34 1 33 eqtri 
 |-  F = ( m e. NN |-> if ( m e. Prime , ( m ^ [_ m / n ]_ A ) , 1 ) )
35 11 adantr 
 |-  ( ( ph /\ p e. Prime ) -> A. m e. Prime [_ m / n ]_ A e. NN0 )
36 3 adantr 
 |-  ( ( ph /\ p e. Prime ) -> N e. NN )
37 simpr 
 |-  ( ( ph /\ p e. Prime ) -> p e. Prime )
38 4 adantr 
 |-  ( ( ph /\ p e. Prime ) -> M e. ( ZZ>= ` N ) )
39 34 35 36 37 12 38 pcmpt2 
 |-  ( ( ph /\ p e. Prime ) -> ( p pCnt ( ( seq 1 ( x. , F ) ` M ) / ( seq 1 ( x. , F ) ` N ) ) ) = if ( ( p <_ M /\ -. p <_ N ) , [_ p / n ]_ A , 0 ) )
40 21 39 breqtrrd 
 |-  ( ( ph /\ p e. Prime ) -> 0 <_ ( p pCnt ( ( seq 1 ( x. , F ) ` M ) / ( seq 1 ( x. , F ) ` N ) ) ) )
41 40 ralrimiva 
 |-  ( ph -> A. p e. Prime 0 <_ ( p pCnt ( ( seq 1 ( x. , F ) ` M ) / ( seq 1 ( x. , F ) ` N ) ) ) )
42 1 2 pcmptcl 
 |-  ( ph -> ( F : NN --> NN /\ seq 1 ( x. , F ) : NN --> NN ) )
43 42 simprd 
 |-  ( ph -> seq 1 ( x. , F ) : NN --> NN )
44 eluznn 
 |-  ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> M e. NN )
45 3 4 44 syl2anc 
 |-  ( ph -> M e. NN )
46 43 45 ffvelrnd 
 |-  ( ph -> ( seq 1 ( x. , F ) ` M ) e. NN )
47 46 nnzd 
 |-  ( ph -> ( seq 1 ( x. , F ) ` M ) e. ZZ )
48 43 3 ffvelrnd 
 |-  ( ph -> ( seq 1 ( x. , F ) ` N ) e. NN )
49 znq 
 |-  ( ( ( seq 1 ( x. , F ) ` M ) e. ZZ /\ ( seq 1 ( x. , F ) ` N ) e. NN ) -> ( ( seq 1 ( x. , F ) ` M ) / ( seq 1 ( x. , F ) ` N ) ) e. QQ )
50 47 48 49 syl2anc 
 |-  ( ph -> ( ( seq 1 ( x. , F ) ` M ) / ( seq 1 ( x. , F ) ` N ) ) e. QQ )
51 pcz 
 |-  ( ( ( seq 1 ( x. , F ) ` M ) / ( seq 1 ( x. , F ) ` N ) ) e. QQ -> ( ( ( seq 1 ( x. , F ) ` M ) / ( seq 1 ( x. , F ) ` N ) ) e. ZZ <-> A. p e. Prime 0 <_ ( p pCnt ( ( seq 1 ( x. , F ) ` M ) / ( seq 1 ( x. , F ) ` N ) ) ) ) )
52 50 51 syl 
 |-  ( ph -> ( ( ( seq 1 ( x. , F ) ` M ) / ( seq 1 ( x. , F ) ` N ) ) e. ZZ <-> A. p e. Prime 0 <_ ( p pCnt ( ( seq 1 ( x. , F ) ` M ) / ( seq 1 ( x. , F ) ` N ) ) ) ) )
53 41 52 mpbird 
 |-  ( ph -> ( ( seq 1 ( x. , F ) ` M ) / ( seq 1 ( x. , F ) ` N ) ) e. ZZ )
54 48 nnzd 
 |-  ( ph -> ( seq 1 ( x. , F ) ` N ) e. ZZ )
55 48 nnne0d 
 |-  ( ph -> ( seq 1 ( x. , F ) ` N ) =/= 0 )
56 dvdsval2 
 |-  ( ( ( seq 1 ( x. , F ) ` N ) e. ZZ /\ ( seq 1 ( x. , F ) ` N ) =/= 0 /\ ( seq 1 ( x. , F ) ` M ) e. ZZ ) -> ( ( seq 1 ( x. , F ) ` N ) || ( seq 1 ( x. , F ) ` M ) <-> ( ( seq 1 ( x. , F ) ` M ) / ( seq 1 ( x. , F ) ` N ) ) e. ZZ ) )
57 54 55 47 56 syl3anc 
 |-  ( ph -> ( ( seq 1 ( x. , F ) ` N ) || ( seq 1 ( x. , F ) ` M ) <-> ( ( seq 1 ( x. , F ) ` M ) / ( seq 1 ( x. , F ) ` N ) ) e. ZZ ) )
58 53 57 mpbird 
 |-  ( ph -> ( seq 1 ( x. , F ) ` N ) || ( seq 1 ( x. , F ) ` M ) )