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

Metamath Proof Explorer

Theorem bernneq2

Description: Variation of Bernoulli's inequality bernneq . (Contributed by NM, 18-Oct-2007)

Ref Expression
Assertion bernneq2 ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴 ) → ( ( ( 𝐴 − 1 ) · 𝑁 ) + 1 ) ≤ ( 𝐴 ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 peano2rem ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − 1 ) ∈ ℝ )
2 1 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴 ) → ( 𝐴 − 1 ) ∈ ℝ )
3 simp2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴 ) → 𝑁 ∈ ℕ0 )
4 df-neg ⊢ - 1 = ( 0 − 1 )
5 0re ⊢ 0 ∈ ℝ
6 1re ⊢ 1 ∈ ℝ
7 lesub1 ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 0 ≤ 𝐴 ↔ ( 0 − 1 ) ≤ ( 𝐴 − 1 ) ) )
8 5 6 7 mp3an13 ⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 ↔ ( 0 − 1 ) ≤ ( 𝐴 − 1 ) ) )
9 8 biimpa ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 0 − 1 ) ≤ ( 𝐴 − 1 ) )
10 4 9 eqbrtrid ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → - 1 ≤ ( 𝐴 − 1 ) )
11 10 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴 ) → - 1 ≤ ( 𝐴 − 1 ) )
12 bernneq ⊢ ( ( ( 𝐴 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ - 1 ≤ ( 𝐴 − 1 ) ) → ( 1 + ( ( 𝐴 − 1 ) · 𝑁 ) ) ≤ ( ( 1 + ( 𝐴 − 1 ) ) ↑ 𝑁 ) )
13 2 3 11 12 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴 ) → ( 1 + ( ( 𝐴 − 1 ) · 𝑁 ) ) ≤ ( ( 1 + ( 𝐴 − 1 ) ) ↑ 𝑁 ) )
14 ax-1cn ⊢ 1 ∈ ℂ
15 1 recnd ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − 1 ) ∈ ℂ )
16 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
17 mulcl ⊢ ( ( ( 𝐴 − 1 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝐴 − 1 ) · 𝑁 ) ∈ ℂ )
18 15 16 17 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 − 1 ) · 𝑁 ) ∈ ℂ )
19 addcom ⊢ ( ( 1 ∈ ℂ ∧ ( ( 𝐴 − 1 ) · 𝑁 ) ∈ ℂ ) → ( 1 + ( ( 𝐴 − 1 ) · 𝑁 ) ) = ( ( ( 𝐴 − 1 ) · 𝑁 ) + 1 ) )
20 14 18 19 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 1 + ( ( 𝐴 − 1 ) · 𝑁 ) ) = ( ( ( 𝐴 − 1 ) · 𝑁 ) + 1 ) )
21 20 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴 ) → ( 1 + ( ( 𝐴 − 1 ) · 𝑁 ) ) = ( ( ( 𝐴 − 1 ) · 𝑁 ) + 1 ) )
22 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
23 pncan3 ⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 1 + ( 𝐴 − 1 ) ) = 𝐴 )
24 14 22 23 sylancr ⊢ ( 𝐴 ∈ ℝ → ( 1 + ( 𝐴 − 1 ) ) = 𝐴 )
25 24 oveq1d ⊢ ( 𝐴 ∈ ℝ → ( ( 1 + ( 𝐴 − 1 ) ) ↑ 𝑁 ) = ( 𝐴 ↑ 𝑁 ) )
26 25 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴 ) → ( ( 1 + ( 𝐴 − 1 ) ) ↑ 𝑁 ) = ( 𝐴 ↑ 𝑁 ) )
27 13 21 26 3brtr3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴 ) → ( ( ( 𝐴 − 1 ) · 𝑁 ) + 1 ) ≤ ( 𝐴 ↑ 𝑁 ) )