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 )

Metamath Proof Explorer

Theorem pcpre1

Proof