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 mulid1 ( 𝐴 ∈ ℂ → ( 𝐴 · 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 + 𝐴 ) ↑ 𝑁 ) )