Theorem bernneq3

Description: A corollary of bernneq . (Contributed by Mario Carneiro, 11-Mar-2014)

	Ref	Expression
Assertion	bernneq3	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to N<P^N$$

Proof

Step	Hyp	Ref	Expression
1		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
2	1	adantl	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to N\in ℝ$$
3		peano2re	$$⊢N\in ℝ\to N+1\in ℝ$$
4	2 3	syl	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to N+1\in ℝ$$
5		eluzelre	$$⊢P\in {\mathbb{Z}}_{\ge 2}\to P\in ℝ$$
6		reexpcl	$$⊢\left(P\in ℝ\wedge N\in {\mathbb{N}}_0\right)\to P^N\in ℝ$$
7	5 6	sylan	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to P^N\in ℝ$$
8	2	ltp1d	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to N<N+1$$
9		uz2m1nn	$$⊢P\in {\mathbb{Z}}_{\ge 2}\to P-1\in \mathbb{N}$$
10	9	adantr	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to P-1\in \mathbb{N}$$
11	10	nnred	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to P-1\in ℝ$$
12	11 2	remulcld	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to \left(P-1\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
13		peano2re	$$⊢\left(P-1\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ\to \left(P-1\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\in ℝ$$
14	12 13	syl	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to \left(P-1\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\in ℝ$$
15		1red	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to 1\in ℝ$$
16		nn0ge0	$$⊢N\in {\mathbb{N}}_0\to 0\le N$$
17	16	adantl	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to 0\le N$$
18	10	nnge1d	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to 1\le P-1$$
19	2 11 17 18	lemulge12d	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to N\le \left(P-1\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
20	2 12 15 19	leadd1dd	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to N+1\le \left(P-1\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1$$
21	5	adantr	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to P\in ℝ$$
22		simpr	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to N\in {\mathbb{N}}_0$$
23		eluzge2nn0	$$⊢P\in {\mathbb{Z}}_{\ge 2}\to P\in {\mathbb{N}}_0$$
24		nn0ge0	$$⊢P\in {\mathbb{N}}_0\to 0\le P$$
25	23 24	syl	$$⊢P\in {\mathbb{Z}}_{\ge 2}\to 0\le P$$
26	25	adantr	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to 0\le P$$
27		bernneq2	$$⊢\left(P\in ℝ\wedge N\in {\mathbb{N}}_0\wedge 0\le P\right)\to \left(P-1\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\le P^N$$
28	21 22 26 27	syl3anc	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to \left(P-1\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\le P^N$$
29	4 14 7 20 28	letrd	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to N+1\le P^N$$
30	2 4 7 8 29	ltletrd	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to N<P^N$$