Theorem bernneq3

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

	Ref	Expression
Assertion	bernneq3	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 < ( 𝑃 ↑ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
2	1	adantl	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
3		peano2re	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 + 1 ) ∈ ℝ )
4	2 3	syl	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ℝ )
5		eluzelre	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ∈ ℝ )
6		reexpcl	⊢ ( ( 𝑃 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑁 ) ∈ ℝ )
7	5 6	sylan	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑁 ) ∈ ℝ )
8	2	ltp1d	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 < ( 𝑁 + 1 ) )
9		uz2m1nn	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑃 − 1 ) ∈ ℕ )
10	9	adantr	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑃 − 1 ) ∈ ℕ )
11	10	nnred	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑃 − 1 ) ∈ ℝ )
12	11 2	remulcld	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑃 − 1 ) · 𝑁 ) ∈ ℝ )
13		peano2re	⊢ ( ( ( 𝑃 − 1 ) · 𝑁 ) ∈ ℝ → ( ( ( 𝑃 − 1 ) · 𝑁 ) + 1 ) ∈ ℝ )
14	12 13	syl	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝑃 − 1 ) · 𝑁 ) + 1 ) ∈ ℝ )
15		1red	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → 1 ∈ ℝ )
16		nn0ge0	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
17	16	adantl	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → 0 ≤ 𝑁 )
18	10	nnge1d	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → 1 ≤ ( 𝑃 − 1 ) )
19	2 11 17 18	lemulge12d	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ≤ ( ( 𝑃 − 1 ) · 𝑁 ) )
20	2 12 15 19	leadd1dd	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ≤ ( ( ( 𝑃 − 1 ) · 𝑁 ) + 1 ) )
21	5	adantr	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑃 ∈ ℝ )
22		simpr	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
23		eluzge2nn0	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ∈ ℕ0 )
24		nn0ge0	⊢ ( 𝑃 ∈ ℕ0 → 0 ≤ 𝑃 )
25	23 24	syl	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 0 ≤ 𝑃 )
26	25	adantr	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → 0 ≤ 𝑃 )
27		bernneq2	⊢ ( ( 𝑃 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝑃 ) → ( ( ( 𝑃 − 1 ) · 𝑁 ) + 1 ) ≤ ( 𝑃 ↑ 𝑁 ) )
28	21 22 26 27	syl3anc	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝑃 − 1 ) · 𝑁 ) + 1 ) ≤ ( 𝑃 ↑ 𝑁 ) )
29	4 14 7 20 28	letrd	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ≤ ( 𝑃 ↑ 𝑁 ) )
30	2 4 7 8 29	ltletrd	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 < ( 𝑃 ↑ 𝑁 ) )