This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) → 𝑁 < ( 𝑃 ↑ 𝑁 ) )