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 ) ≤ ( 𝐴 ↑ 𝑁 ) )