Metamath Proof Explorer

Theorem pcfaclem

Description: Lemma for pcfac . (Contributed by Mario Carneiro, 20-May-2014)

Ref Expression
Assertion pcfaclem 
|- ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> ( |_ ` ( N / ( P ^ M ) ) ) = 0 )

Proof

Step Hyp Ref Expression
1 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
2 1 3ad2ant1 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> 0 <_ N )
3 nn0re 
 |-  ( N e. NN0 -> N e. RR )
4 3 3ad2ant1 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> N e. RR )
5 prmnn 
 |-  ( P e. Prime -> P e. NN )
6 5 3ad2ant3 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> P e. NN )
7 eluznn0 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) ) -> M e. NN0 )
8 7 3adant3 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> M e. NN0 )
9 6 8 nnexpcld 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> ( P ^ M ) e. NN )
10 9 nnred 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> ( P ^ M ) e. RR )
11 9 nngt0d 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> 0 < ( P ^ M ) )
12 ge0div 
 |-  ( ( N e. RR /\ ( P ^ M ) e. RR /\ 0 < ( P ^ M ) ) -> ( 0 <_ N <-> 0 <_ ( N / ( P ^ M ) ) ) )
13 4 10 11 12 syl3anc 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> ( 0 <_ N <-> 0 <_ ( N / ( P ^ M ) ) ) )
14 2 13 mpbid 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> 0 <_ ( N / ( P ^ M ) ) )
15 8 nn0red 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> M e. RR )
16 eluzle 
 |-  ( M e. ( ZZ>= ` N ) -> N <_ M )
17 16 3ad2ant2 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> N <_ M )
18 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
19 18 3ad2ant3 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> P e. ( ZZ>= ` 2 ) )
20 bernneq3 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ M e. NN0 ) -> M < ( P ^ M ) )
21 19 8 20 syl2anc 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> M < ( P ^ M ) )
22 4 15 10 17 21 lelttrd 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> N < ( P ^ M ) )
23 9 nncnd 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> ( P ^ M ) e. CC )
24 23 mulid1d 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> ( ( P ^ M ) x. 1 ) = ( P ^ M ) )
25 22 24 breqtrrd 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> N < ( ( P ^ M ) x. 1 ) )
26 1red 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> 1 e. RR )
27 ltdivmul 
 |-  ( ( N e. RR /\ 1 e. RR /\ ( ( P ^ M ) e. RR /\ 0 < ( P ^ M ) ) ) -> ( ( N / ( P ^ M ) ) < 1 <-> N < ( ( P ^ M ) x. 1 ) ) )
28 4 26 10 11 27 syl112anc 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> ( ( N / ( P ^ M ) ) < 1 <-> N < ( ( P ^ M ) x. 1 ) ) )
29 25 28 mpbird 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> ( N / ( P ^ M ) ) < 1 )
30 0p1e1 
 |-  ( 0 + 1 ) = 1
31 29 30 breqtrrdi 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> ( N / ( P ^ M ) ) < ( 0 + 1 ) )
32 4 9 nndivred 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> ( N / ( P ^ M ) ) e. RR )
33 0z 
 |-  0 e. ZZ
34 flbi 
 |-  ( ( ( N / ( P ^ M ) ) e. RR /\ 0 e. ZZ ) -> ( ( |_ ` ( N / ( P ^ M ) ) ) = 0 <-> ( 0 <_ ( N / ( P ^ M ) ) /\ ( N / ( P ^ M ) ) < ( 0 + 1 ) ) ) )
35 32 33 34 sylancl 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> ( ( |_ ` ( N / ( P ^ M ) ) ) = 0 <-> ( 0 <_ ( N / ( P ^ M ) ) /\ ( N / ( P ^ M ) ) < ( 0 + 1 ) ) ) )
36 14 31 35 mpbir2and 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> ( |_ ` ( N / ( P ^ M ) ) ) = 0 )