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≤AN

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-1N
13 2 3 11 12 syl3anc ⊢A∈ℝ∧N∈ℕ0∧0≤A→1+A−1⋅ N≤1+A-1N
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-1N=AN
26 25 3ad2ant1 ⊢A∈ℝ∧N∈ℕ0∧0≤A→1+A-1N=AN
27 13 21 26 3brtr3d ⊢A∈ℝ∧N∈ℕ0∧0≤A→A−1⋅ N+1≤AN