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 ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ≤ 1 ) → ( 1 − ( 𝑁 · 𝐴 ) ) ≤ ( ( 1 − 𝐴 ) ↑ 𝑁 ) )

Proof

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