Metamath Proof Explorer

Theorem pcpre1

Description: Value of the prime power pre-function at 1. (Contributed by Mario Carneiro, 23-Feb-2014) (Revised by Mario Carneiro, 26-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 pclem.1 
 |-  A = { n e. NN0 | ( P ^ n ) || N }
2 pclem.2 
 |-  S = sup ( A , RR , < )
3 1z 
 |-  1 e. ZZ
4 eleq1 
 |-  ( N = 1 -> ( N e. ZZ <-> 1 e. ZZ ) )
5 3 4 mpbiri 
 |-  ( N = 1 -> N e. ZZ )
6 ax-1ne0 
 |-  1 =/= 0
7 neeq1 
 |-  ( N = 1 -> ( N =/= 0 <-> 1 =/= 0 ) )
8 6 7 mpbiri 
 |-  ( N = 1 -> N =/= 0 )
9 5 8 jca 
 |-  ( N = 1 -> ( N e. ZZ /\ N =/= 0 ) )
10 1 2 pcprecl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( S e. NN0 /\ ( P ^ S ) || N ) )
11 9 10 sylan2 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> ( S e. NN0 /\ ( P ^ S ) || N ) )
12 11 simprd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> ( P ^ S ) || N )
13 simpr 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> N = 1 )
14 12 13 breqtrd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> ( P ^ S ) || 1 )
15 eluz2nn 
 |-  ( P e. ( ZZ>= ` 2 ) -> P e. NN )
16 15 adantr 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> P e. NN )
17 11 simpld 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> S e. NN0 )
18 16 17 nnexpcld 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> ( P ^ S ) e. NN )
19 18 nnzd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> ( P ^ S ) e. ZZ )
20 1nn 
 |-  1 e. NN
21 dvdsle 
 |-  ( ( ( P ^ S ) e. ZZ /\ 1 e. NN ) -> ( ( P ^ S ) || 1 -> ( P ^ S ) <_ 1 ) )
22 19 20 21 sylancl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> ( ( P ^ S ) || 1 -> ( P ^ S ) <_ 1 ) )
23 14 22 mpd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> ( P ^ S ) <_ 1 )
24 16 nncnd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> P e. CC )
25 24 exp0d 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> ( P ^ 0 ) = 1 )
26 23 25 breqtrrd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> ( P ^ S ) <_ ( P ^ 0 ) )
27 16 nnred 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> P e. RR )
28 17 nn0zd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> S e. ZZ )
29 0zd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> 0 e. ZZ )
30 eluz2gt1 
 |-  ( P e. ( ZZ>= ` 2 ) -> 1 < P )
31 30 adantr 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> 1 < P )
32 27 28 29 31 leexp2d 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> ( S <_ 0 <-> ( P ^ S ) <_ ( P ^ 0 ) ) )
33 26 32 mpbird 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> S <_ 0 )
34 10 simpld 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> S e. NN0 )
35 9 34 sylan2 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> S e. NN0 )
36 nn0le0eq0 
 |-  ( S e. NN0 -> ( S <_ 0 <-> S = 0 ) )
37 35 36 syl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> ( S <_ 0 <-> S = 0 ) )
38 33 37 mpbid 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> S = 0 )