Metamath Proof Explorer

Theorem bernneq2

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

Ref Expression
Assertion bernneq2 ⊢ A ∈ ℝ ∧ N ∈ ℕ 0 ∧ 0 ≤ A → A − 1 ⋅ N + 1 ≤ A N

Proof

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