Metamath Proof Explorer

Theorem stoweidlem10

Description: Lemma for stoweid . This lemma is used by Lemma 1 in BrosowskiDeutsh p. 90, this lemma is an application of Bernoulli's inequality. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Assertion stoweidlem10 ⊢ A ∈ ℝ ∧ N ∈ ℕ 0 ∧ A ≤ 1 → 1 − N ⁢ A ≤ 1 − A N

Proof

Step Hyp Ref Expression
1 renegcl ⊢ A ∈ ℝ → − A ∈ ℝ
2 1 3ad2ant1 ⊢ A ∈ ℝ ∧ N ∈ ℕ 0 ∧ A ≤ 1 → − A ∈ ℝ
3 simp2 ⊢ A ∈ ℝ ∧ N ∈ ℕ 0 ∧ A ≤ 1 → N ∈ ℕ 0
4 simpr ⊢ A ∈ ℝ ∧ A ≤ 1 → A ≤ 1
5 simpl ⊢ A ∈ ℝ ∧ A ≤ 1 → A ∈ ℝ
6 1red ⊢ A ∈ ℝ ∧ A ≤ 1 → 1 ∈ ℝ
7 5 6 lenegd ⊢ A ∈ ℝ ∧ A ≤ 1 → A ≤ 1 ↔ − 1 ≤ − A
8 4 7 mpbid ⊢ A ∈ ℝ ∧ A ≤ 1 → − 1 ≤ − A
9 8 3adant2 ⊢ A ∈ ℝ ∧ N ∈ ℕ 0 ∧ A ≤ 1 → − 1 ≤ − A
10 bernneq ⊢ − A ∈ ℝ ∧ N ∈ ℕ 0 ∧ − 1 ≤ − A → 1 + − A ⋅ N ≤ 1 + − A N
11 2 3 9 10 syl3anc ⊢ A ∈ ℝ ∧ N ∈ ℕ 0 ∧ A ≤ 1 → 1 + − A ⋅ N ≤ 1 + − A N
12 recn ⊢ A ∈ ℝ → A ∈ ℂ
13 12 3ad2ant1 ⊢ A ∈ ℝ ∧ N ∈ ℕ 0 ∧ A ≤ 1 → A ∈ ℂ
14 nn0cn ⊢ N ∈ ℕ 0 → N ∈ ℂ
15 14 3ad2ant2 ⊢ A ∈ ℝ ∧ N ∈ ℕ 0 ∧ A ≤ 1 → N ∈ ℂ
16 1cnd ⊢ A ∈ ℝ ∧ N ∈ ℕ 0 ∧ A ≤ 1 → 1 ∈ ℂ
17 mulneg1 ⊢ A ∈ ℂ ∧ N ∈ ℂ → − A ⋅ N = − A ⋅ N
18 17 oveq2d ⊢ A ∈ ℂ ∧ N ∈ ℂ → 1 + − A ⋅ N = 1 + − A ⋅ N
19 18 3adant3 ⊢ A ∈ ℂ ∧ N ∈ ℂ ∧ 1 ∈ ℂ → 1 + − A ⋅ N = 1 + − A ⋅ N
20 simp3 ⊢ A ∈ ℂ ∧ N ∈ ℂ ∧ 1 ∈ ℂ → 1 ∈ ℂ
21 mulcl ⊢ A ∈ ℂ ∧ N ∈ ℂ → A ⋅ N ∈ ℂ
22 21 3adant3 ⊢ A ∈ ℂ ∧ N ∈ ℂ ∧ 1 ∈ ℂ → A ⋅ N ∈ ℂ
23 20 22 negsubd ⊢ A ∈ ℂ ∧ N ∈ ℂ ∧ 1 ∈ ℂ → 1 + − A ⋅ N = 1 − A ⋅ N
24 mulcom ⊢ A ∈ ℂ ∧ N ∈ ℂ → A ⋅ N = N ⁢ A
25 24 oveq2d ⊢ A ∈ ℂ ∧ N ∈ ℂ → 1 − A ⋅ N = 1 − N ⁢ A
26 25 3adant3 ⊢ A ∈ ℂ ∧ N ∈ ℂ ∧ 1 ∈ ℂ → 1 − A ⋅ N = 1 − N ⁢ A
27 19 23 26 3eqtrd ⊢ A ∈ ℂ ∧ N ∈ ℂ ∧ 1 ∈ ℂ → 1 + − A ⋅ N = 1 − N ⁢ A
28 13 15 16 27 syl3anc ⊢ A ∈ ℝ ∧ N ∈ ℕ 0 ∧ A ≤ 1 → 1 + − A ⋅ N = 1 − N ⁢ A
29 1cnd ⊢ A ∈ ℝ → 1 ∈ ℂ
30 29 12 negsubd ⊢ A ∈ ℝ → 1 + − A = 1 − A
31 30 oveq1d ⊢ A ∈ ℝ → 1 + − A N = 1 − A N
32 31 3ad2ant1 ⊢ A ∈ ℝ ∧ N ∈ ℕ 0 ∧ A ≤ 1 → 1 + − A N = 1 − A N
33 11 28 32 3brtr3d ⊢ A ∈ ℝ ∧ N ∈ ℕ 0 ∧ A ≤ 1 → 1 − N ⁢ A ≤ 1 − A N