This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bernneq

Description: Bernoulli's inequality, due to Johan Bernoulli (1667-1748). (Contributed by NM, 21-Feb-2005)

Ref Expression
Assertion bernneq ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ - 1 ≤ 𝐴 ) → ( 1 + ( 𝐴 · 𝑁 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑗 = 0 → ( 𝐴 · 𝑗 ) = ( 𝐴 · 0 ) )
2 1 oveq2d ⊢ ( 𝑗 = 0 → ( 1 + ( 𝐴 · 𝑗 ) ) = ( 1 + ( 𝐴 · 0 ) ) )
3 oveq2 ⊢ ( 𝑗 = 0 → ( ( 1 + 𝐴 ) ↑ 𝑗 ) = ( ( 1 + 𝐴 ) ↑ 0 ) )
4 2 3 breq12d ⊢ ( 𝑗 = 0 → ( ( 1 + ( 𝐴 · 𝑗 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑗 ) ↔ ( 1 + ( 𝐴 · 0 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 0 ) ) )
5 4 imbi2d ⊢ ( 𝑗 = 0 → ( ( ( 𝐴 ∈ ℝ ∧ - 1 ≤ 𝐴 ) → ( 1 + ( 𝐴 · 𝑗 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑗 ) ) ↔ ( ( 𝐴 ∈ ℝ ∧ - 1 ≤ 𝐴 ) → ( 1 + ( 𝐴 · 0 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 0 ) ) ) )
6 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐴 · 𝑗 ) = ( 𝐴 · 𝑘 ) )
7 6 oveq2d ⊢ ( 𝑗 = 𝑘 → ( 1 + ( 𝐴 · 𝑗 ) ) = ( 1 + ( 𝐴 · 𝑘 ) ) )
8 oveq2 ⊢ ( 𝑗 = 𝑘 → ( ( 1 + 𝐴 ) ↑ 𝑗 ) = ( ( 1 + 𝐴 ) ↑ 𝑘 ) )
9 7 8 breq12d ⊢ ( 𝑗 = 𝑘 → ( ( 1 + ( 𝐴 · 𝑗 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑗 ) ↔ ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) ) )
10 9 imbi2d ⊢ ( 𝑗 = 𝑘 → ( ( ( 𝐴 ∈ ℝ ∧ - 1 ≤ 𝐴 ) → ( 1 + ( 𝐴 · 𝑗 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑗 ) ) ↔ ( ( 𝐴 ∈ ℝ ∧ - 1 ≤ 𝐴 ) → ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) ) ) )
11 oveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐴 · 𝑗 ) = ( 𝐴 · ( 𝑘 + 1 ) ) )
12 11 oveq2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 1 + ( 𝐴 · 𝑗 ) ) = ( 1 + ( 𝐴 · ( 𝑘 + 1 ) ) ) )
13 oveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 1 + 𝐴 ) ↑ 𝑗 ) = ( ( 1 + 𝐴 ) ↑ ( 𝑘 + 1 ) ) )
14 12 13 breq12d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 1 + ( 𝐴 · 𝑗 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑗 ) ↔ ( 1 + ( 𝐴 · ( 𝑘 + 1 ) ) ) ≤ ( ( 1 + 𝐴 ) ↑ ( 𝑘 + 1 ) ) ) )
15 14 imbi2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ( 𝐴 ∈ ℝ ∧ - 1 ≤ 𝐴 ) → ( 1 + ( 𝐴 · 𝑗 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑗 ) ) ↔ ( ( 𝐴 ∈ ℝ ∧ - 1 ≤ 𝐴 ) → ( 1 + ( 𝐴 · ( 𝑘 + 1 ) ) ) ≤ ( ( 1 + 𝐴 ) ↑ ( 𝑘 + 1 ) ) ) ) )
16 oveq2 ⊢ ( 𝑗 = 𝑁 → ( 𝐴 · 𝑗 ) = ( 𝐴 · 𝑁 ) )
17 16 oveq2d ⊢ ( 𝑗 = 𝑁 → ( 1 + ( 𝐴 · 𝑗 ) ) = ( 1 + ( 𝐴 · 𝑁 ) ) )
18 oveq2 ⊢ ( 𝑗 = 𝑁 → ( ( 1 + 𝐴 ) ↑ 𝑗 ) = ( ( 1 + 𝐴 ) ↑ 𝑁 ) )
19 17 18 breq12d ⊢ ( 𝑗 = 𝑁 → ( ( 1 + ( 𝐴 · 𝑗 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑗 ) ↔ ( 1 + ( 𝐴 · 𝑁 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑁 ) ) )
20 19 imbi2d ⊢ ( 𝑗 = 𝑁 → ( ( ( 𝐴 ∈ ℝ ∧ - 1 ≤ 𝐴 ) → ( 1 + ( 𝐴 · 𝑗 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑗 ) ) ↔ ( ( 𝐴 ∈ ℝ ∧ - 1 ≤ 𝐴 ) → ( 1 + ( 𝐴 · 𝑁 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑁 ) ) ) )
21 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
22 mul01 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 0 ) = 0 )
23 22 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( 1 + ( 𝐴 · 0 ) ) = ( 1 + 0 ) )
24 1p0e1 ⊢ ( 1 + 0 ) = 1
25 23 24 eqtrdi ⊢ ( 𝐴 ∈ ℂ → ( 1 + ( 𝐴 · 0 ) ) = 1 )
26 1le1 ⊢ 1 ≤ 1
27 ax-1cn ⊢ 1 ∈ ℂ
28 addcl ⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 1 + 𝐴 ) ∈ ℂ )
29 27 28 mpan ⊢ ( 𝐴 ∈ ℂ → ( 1 + 𝐴 ) ∈ ℂ )
30 exp0 ⊢ ( ( 1 + 𝐴 ) ∈ ℂ → ( ( 1 + 𝐴 ) ↑ 0 ) = 1 )
31 29 30 syl ⊢ ( 𝐴 ∈ ℂ → ( ( 1 + 𝐴 ) ↑ 0 ) = 1 )
32 26 31 breqtrrid ⊢ ( 𝐴 ∈ ℂ → 1 ≤ ( ( 1 + 𝐴 ) ↑ 0 ) )
33 25 32 eqbrtrd ⊢ ( 𝐴 ∈ ℂ → ( 1 + ( 𝐴 · 0 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 0 ) )
34 21 33 syl ⊢ ( 𝐴 ∈ ℝ → ( 1 + ( 𝐴 · 0 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 0 ) )
35 34 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ - 1 ≤ 𝐴 ) → ( 1 + ( 𝐴 · 0 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 0 ) )
36 1re ⊢ 1 ∈ ℝ
37 nn0re ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ )
38 remulcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝐴 · 𝑘 ) ∈ ℝ )
39 37 38 sylan2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 · 𝑘 ) ∈ ℝ )
40 readdcl ⊢ ( ( 1 ∈ ℝ ∧ ( 𝐴 · 𝑘 ) ∈ ℝ ) → ( 1 + ( 𝐴 · 𝑘 ) ) ∈ ℝ )
41 36 39 40 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( 1 + ( 𝐴 · 𝑘 ) ) ∈ ℝ )
42 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ℝ )
43 readdcl ⊢ ( ( ( 1 + ( 𝐴 · 𝑘 ) ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 1 + ( 𝐴 · 𝑘 ) ) + 𝐴 ) ∈ ℝ )
44 41 42 43 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 + ( 𝐴 · 𝑘 ) ) + 𝐴 ) ∈ ℝ )
45 44 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) ∧ ( - 1 ≤ 𝐴 ∧ ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) ) ) → ( ( 1 + ( 𝐴 · 𝑘 ) ) + 𝐴 ) ∈ ℝ )
46 readdcl ⊢ ( ( 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 1 + 𝐴 ) ∈ ℝ )
47 36 46 mpan ⊢ ( 𝐴 ∈ ℝ → ( 1 + 𝐴 ) ∈ ℝ )
48 47 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( 1 + 𝐴 ) ∈ ℝ )
49 41 48 remulcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 + ( 𝐴 · 𝑘 ) ) · ( 1 + 𝐴 ) ) ∈ ℝ )
50 49 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) ∧ ( - 1 ≤ 𝐴 ∧ ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) ) ) → ( ( 1 + ( 𝐴 · 𝑘 ) ) · ( 1 + 𝐴 ) ) ∈ ℝ )
51 reexpcl ⊢ ( ( ( 1 + 𝐴 ) ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 + 𝐴 ) ↑ 𝑘 ) ∈ ℝ )
52 47 51 sylan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 + 𝐴 ) ↑ 𝑘 ) ∈ ℝ )
53 52 48 remulcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 1 + 𝐴 ) ↑ 𝑘 ) · ( 1 + 𝐴 ) ) ∈ ℝ )
54 53 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) ∧ ( - 1 ≤ 𝐴 ∧ ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) ) ) → ( ( ( 1 + 𝐴 ) ↑ 𝑘 ) · ( 1 + 𝐴 ) ) ∈ ℝ )
55 remulcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐴 · 𝐴 ) ∈ ℝ )
56 55 anidms ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 𝐴 ) ∈ ℝ )
57 msqge0 ⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( 𝐴 · 𝐴 ) )
58 56 57 jca ⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 · 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 · 𝐴 ) ) )
59 nn0ge0 ⊢ ( 𝑘 ∈ ℕ0 → 0 ≤ 𝑘 )
60 37 59 jca ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 ∈ ℝ ∧ 0 ≤ 𝑘 ) )
61 mulge0 ⊢ ( ( ( ( 𝐴 · 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 · 𝐴 ) ) ∧ ( 𝑘 ∈ ℝ ∧ 0 ≤ 𝑘 ) ) → 0 ≤ ( ( 𝐴 · 𝐴 ) · 𝑘 ) )
62 58 60 61 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → 0 ≤ ( ( 𝐴 · 𝐴 ) · 𝑘 ) )
63 21 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
64 nn0cn ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
65 64 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℂ )
66 63 63 65 mul32d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 · 𝐴 ) · 𝑘 ) = ( ( 𝐴 · 𝑘 ) · 𝐴 ) )
67 62 66 breqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → 0 ≤ ( ( 𝐴 · 𝑘 ) · 𝐴 ) )
68 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → 𝐴 ∈ ℝ )
69 38 68 remulcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( ( 𝐴 · 𝑘 ) · 𝐴 ) ∈ ℝ )
70 37 69 sylan2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 · 𝑘 ) · 𝐴 ) ∈ ℝ )
71 44 70 addge01d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( 0 ≤ ( ( 𝐴 · 𝑘 ) · 𝐴 ) ↔ ( ( 1 + ( 𝐴 · 𝑘 ) ) + 𝐴 ) ≤ ( ( ( 1 + ( 𝐴 · 𝑘 ) ) + 𝐴 ) + ( ( 𝐴 · 𝑘 ) · 𝐴 ) ) ) )
72 67 71 mpbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 + ( 𝐴 · 𝑘 ) ) + 𝐴 ) ≤ ( ( ( 1 + ( 𝐴 · 𝑘 ) ) + 𝐴 ) + ( ( 𝐴 · 𝑘 ) · 𝐴 ) ) )
73 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝐴 · 𝑘 ) ∈ ℂ )
74 addcl ⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 · 𝑘 ) ∈ ℂ ) → ( 1 + ( 𝐴 · 𝑘 ) ) ∈ ℂ )
75 27 73 74 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 1 + ( 𝐴 · 𝑘 ) ) ∈ ℂ )
76 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → 𝐴 ∈ ℂ )
77 73 76 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 𝐴 · 𝑘 ) · 𝐴 ) ∈ ℂ )
78 75 76 77 addassd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( ( 1 + ( 𝐴 · 𝑘 ) ) + 𝐴 ) + ( ( 𝐴 · 𝑘 ) · 𝐴 ) ) = ( ( 1 + ( 𝐴 · 𝑘 ) ) + ( 𝐴 + ( ( 𝐴 · 𝑘 ) · 𝐴 ) ) ) )
79 muladd11 ⊢ ( ( ( 𝐴 · 𝑘 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 1 + ( 𝐴 · 𝑘 ) ) · ( 1 + 𝐴 ) ) = ( ( 1 + ( 𝐴 · 𝑘 ) ) + ( 𝐴 + ( ( 𝐴 · 𝑘 ) · 𝐴 ) ) ) )
80 73 76 79 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 1 + ( 𝐴 · 𝑘 ) ) · ( 1 + 𝐴 ) ) = ( ( 1 + ( 𝐴 · 𝑘 ) ) + ( 𝐴 + ( ( 𝐴 · 𝑘 ) · 𝐴 ) ) ) )
81 78 80 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( ( 1 + ( 𝐴 · 𝑘 ) ) + 𝐴 ) + ( ( 𝐴 · 𝑘 ) · 𝐴 ) ) = ( ( 1 + ( 𝐴 · 𝑘 ) ) · ( 1 + 𝐴 ) ) )
82 21 64 81 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 1 + ( 𝐴 · 𝑘 ) ) + 𝐴 ) + ( ( 𝐴 · 𝑘 ) · 𝐴 ) ) = ( ( 1 + ( 𝐴 · 𝑘 ) ) · ( 1 + 𝐴 ) ) )
83 72 82 breqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 + ( 𝐴 · 𝑘 ) ) + 𝐴 ) ≤ ( ( 1 + ( 𝐴 · 𝑘 ) ) · ( 1 + 𝐴 ) ) )
84 83 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) ∧ ( - 1 ≤ 𝐴 ∧ ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) ) ) → ( ( 1 + ( 𝐴 · 𝑘 ) ) + 𝐴 ) ≤ ( ( 1 + ( 𝐴 · 𝑘 ) ) · ( 1 + 𝐴 ) ) )
85 41 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) ∧ ( - 1 ≤ 𝐴 ∧ ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) ) ) → ( 1 + ( 𝐴 · 𝑘 ) ) ∈ ℝ )
86 52 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) ∧ ( - 1 ≤ 𝐴 ∧ ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) ) ) → ( ( 1 + 𝐴 ) ↑ 𝑘 ) ∈ ℝ )
87 48 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) ∧ ( - 1 ≤ 𝐴 ∧ ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) ) ) → ( 1 + 𝐴 ) ∈ ℝ )
88 neg1rr ⊢ - 1 ∈ ℝ
89 leadd2 ⊢ ( ( - 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ) → ( - 1 ≤ 𝐴 ↔ ( 1 + - 1 ) ≤ ( 1 + 𝐴 ) ) )
90 88 36 89 mp3an13 ⊢ ( 𝐴 ∈ ℝ → ( - 1 ≤ 𝐴 ↔ ( 1 + - 1 ) ≤ ( 1 + 𝐴 ) ) )
91 1pneg1e0 ⊢ ( 1 + - 1 ) = 0
92 91 breq1i ⊢ ( ( 1 + - 1 ) ≤ ( 1 + 𝐴 ) ↔ 0 ≤ ( 1 + 𝐴 ) )
93 90 92 bitrdi ⊢ ( 𝐴 ∈ ℝ → ( - 1 ≤ 𝐴 ↔ 0 ≤ ( 1 + 𝐴 ) ) )
94 93 biimpa ⊢ ( ( 𝐴 ∈ ℝ ∧ - 1 ≤ 𝐴 ) → 0 ≤ ( 1 + 𝐴 ) )
95 94 ad2ant2r ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) ∧ ( - 1 ≤ 𝐴 ∧ ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) ) ) → 0 ≤ ( 1 + 𝐴 ) )
96 simprr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) ∧ ( - 1 ≤ 𝐴 ∧ ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) ) ) → ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) )
97 85 86 87 95 96 lemul1ad ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) ∧ ( - 1 ≤ 𝐴 ∧ ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) ) ) → ( ( 1 + ( 𝐴 · 𝑘 ) ) · ( 1 + 𝐴 ) ) ≤ ( ( ( 1 + 𝐴 ) ↑ 𝑘 ) · ( 1 + 𝐴 ) ) )
98 45 50 54 84 97 letrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) ∧ ( - 1 ≤ 𝐴 ∧ ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) ) ) → ( ( 1 + ( 𝐴 · 𝑘 ) ) + 𝐴 ) ≤ ( ( ( 1 + 𝐴 ) ↑ 𝑘 ) · ( 1 + 𝐴 ) ) )
99 adddi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐴 · ( 𝑘 + 1 ) ) = ( ( 𝐴 · 𝑘 ) + ( 𝐴 · 1 ) ) )
100 27 99 mp3an3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝐴 · ( 𝑘 + 1 ) ) = ( ( 𝐴 · 𝑘 ) + ( 𝐴 · 1 ) ) )
101 mulrid ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 1 ) = 𝐴 )
102 101 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝐴 · 1 ) = 𝐴 )
103 102 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 𝐴 · 𝑘 ) + ( 𝐴 · 1 ) ) = ( ( 𝐴 · 𝑘 ) + 𝐴 ) )
104 100 103 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝐴 · ( 𝑘 + 1 ) ) = ( ( 𝐴 · 𝑘 ) + 𝐴 ) )
105 104 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 1 + ( 𝐴 · ( 𝑘 + 1 ) ) ) = ( 1 + ( ( 𝐴 · 𝑘 ) + 𝐴 ) ) )
106 addass ⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 · 𝑘 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 1 + ( 𝐴 · 𝑘 ) ) + 𝐴 ) = ( 1 + ( ( 𝐴 · 𝑘 ) + 𝐴 ) ) )
107 27 73 76 106 mp3an2i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 1 + ( 𝐴 · 𝑘 ) ) + 𝐴 ) = ( 1 + ( ( 𝐴 · 𝑘 ) + 𝐴 ) ) )
108 105 107 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 1 + ( 𝐴 · ( 𝑘 + 1 ) ) ) = ( ( 1 + ( 𝐴 · 𝑘 ) ) + 𝐴 ) )
109 21 64 108 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( 1 + ( 𝐴 · ( 𝑘 + 1 ) ) ) = ( ( 1 + ( 𝐴 · 𝑘 ) ) + 𝐴 ) )
110 109 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) ∧ ( - 1 ≤ 𝐴 ∧ ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) ) ) → ( 1 + ( 𝐴 · ( 𝑘 + 1 ) ) ) = ( ( 1 + ( 𝐴 · 𝑘 ) ) + 𝐴 ) )
111 27 21 28 sylancr ⊢ ( 𝐴 ∈ ℝ → ( 1 + 𝐴 ) ∈ ℂ )
112 expp1 ⊢ ( ( ( 1 + 𝐴 ) ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 + 𝐴 ) ↑ ( 𝑘 + 1 ) ) = ( ( ( 1 + 𝐴 ) ↑ 𝑘 ) · ( 1 + 𝐴 ) ) )
113 111 112 sylan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 + 𝐴 ) ↑ ( 𝑘 + 1 ) ) = ( ( ( 1 + 𝐴 ) ↑ 𝑘 ) · ( 1 + 𝐴 ) ) )
114 113 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) ∧ ( - 1 ≤ 𝐴 ∧ ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) ) ) → ( ( 1 + 𝐴 ) ↑ ( 𝑘 + 1 ) ) = ( ( ( 1 + 𝐴 ) ↑ 𝑘 ) · ( 1 + 𝐴 ) ) )
115 98 110 114 3brtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) ∧ ( - 1 ≤ 𝐴 ∧ ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) ) ) → ( 1 + ( 𝐴 · ( 𝑘 + 1 ) ) ) ≤ ( ( 1 + 𝐴 ) ↑ ( 𝑘 + 1 ) ) )
116 115 exp43 ⊢ ( 𝐴 ∈ ℝ → ( 𝑘 ∈ ℕ0 → ( - 1 ≤ 𝐴 → ( ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) → ( 1 + ( 𝐴 · ( 𝑘 + 1 ) ) ) ≤ ( ( 1 + 𝐴 ) ↑ ( 𝑘 + 1 ) ) ) ) ) )
117 116 com12 ⊢ ( 𝑘 ∈ ℕ0 → ( 𝐴 ∈ ℝ → ( - 1 ≤ 𝐴 → ( ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) → ( 1 + ( 𝐴 · ( 𝑘 + 1 ) ) ) ≤ ( ( 1 + 𝐴 ) ↑ ( 𝑘 + 1 ) ) ) ) ) )
118 117 impd ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝐴 ∈ ℝ ∧ - 1 ≤ 𝐴 ) → ( ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) → ( 1 + ( 𝐴 · ( 𝑘 + 1 ) ) ) ≤ ( ( 1 + 𝐴 ) ↑ ( 𝑘 + 1 ) ) ) ) )
119 118 a2d ⊢ ( 𝑘 ∈ ℕ0 → ( ( ( 𝐴 ∈ ℝ ∧ - 1 ≤ 𝐴 ) → ( 1 + ( 𝐴 · 𝑘 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑘 ) ) → ( ( 𝐴 ∈ ℝ ∧ - 1 ≤ 𝐴 ) → ( 1 + ( 𝐴 · ( 𝑘 + 1 ) ) ) ≤ ( ( 1 + 𝐴 ) ↑ ( 𝑘 + 1 ) ) ) ) )
120 5 10 15 20 35 119 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝐴 ∈ ℝ ∧ - 1 ≤ 𝐴 ) → ( 1 + ( 𝐴 · 𝑁 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑁 ) ) )
121 120 expd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ∈ ℝ → ( - 1 ≤ 𝐴 → ( 1 + ( 𝐴 · 𝑁 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑁 ) ) ) )
122 121 3imp21 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ - 1 ≤ 𝐴 ) → ( 1 + ( 𝐴 · 𝑁 ) ) ≤ ( ( 1 + 𝐴 ) ↑ 𝑁 ) )