Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  bernneq Structured version   Visualization version   GIF version

Theorem bernneq 13591
 Description: Bernoulli's inequality, due to Johan Bernoulli (1667-1748). (Contributed by NM, 21-Feb-2005.)
Assertion
Ref Expression
bernneq ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ -1 ≤ 𝐴) → (1 + (𝐴 · 𝑁)) ≤ ((1 + 𝐴)↑𝑁))

Proof of Theorem bernneq
Dummy variables 𝑗 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 7153 . . . . . . 7 (𝑗 = 0 → (𝐴 · 𝑗) = (𝐴 · 0))
21oveq2d 7161 . . . . . 6 (𝑗 = 0 → (1 + (𝐴 · 𝑗)) = (1 + (𝐴 · 0)))
3 oveq2 7153 . . . . . 6 (𝑗 = 0 → ((1 + 𝐴)↑𝑗) = ((1 + 𝐴)↑0))
42, 3breq12d 5065 . . . . 5 (𝑗 = 0 → ((1 + (𝐴 · 𝑗)) ≤ ((1 + 𝐴)↑𝑗) ↔ (1 + (𝐴 · 0)) ≤ ((1 + 𝐴)↑0)))
54imbi2d 344 . . . 4 (𝑗 = 0 → (((𝐴 ∈ ℝ ∧ -1 ≤ 𝐴) → (1 + (𝐴 · 𝑗)) ≤ ((1 + 𝐴)↑𝑗)) ↔ ((𝐴 ∈ ℝ ∧ -1 ≤ 𝐴) → (1 + (𝐴 · 0)) ≤ ((1 + 𝐴)↑0))))
6 oveq2 7153 . . . . . . 7 (𝑗 = 𝑘 → (𝐴 · 𝑗) = (𝐴 · 𝑘))
76oveq2d 7161 . . . . . 6 (𝑗 = 𝑘 → (1 + (𝐴 · 𝑗)) = (1 + (𝐴 · 𝑘)))
8 oveq2 7153 . . . . . 6 (𝑗 = 𝑘 → ((1 + 𝐴)↑𝑗) = ((1 + 𝐴)↑𝑘))
97, 8breq12d 5065 . . . . 5 (𝑗 = 𝑘 → ((1 + (𝐴 · 𝑗)) ≤ ((1 + 𝐴)↑𝑗) ↔ (1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘)))
109imbi2d 344 . . . 4 (𝑗 = 𝑘 → (((𝐴 ∈ ℝ ∧ -1 ≤ 𝐴) → (1 + (𝐴 · 𝑗)) ≤ ((1 + 𝐴)↑𝑗)) ↔ ((𝐴 ∈ ℝ ∧ -1 ≤ 𝐴) → (1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘))))
11 oveq2 7153 . . . . . . 7 (𝑗 = (𝑘 + 1) → (𝐴 · 𝑗) = (𝐴 · (𝑘 + 1)))
1211oveq2d 7161 . . . . . 6 (𝑗 = (𝑘 + 1) → (1 + (𝐴 · 𝑗)) = (1 + (𝐴 · (𝑘 + 1))))
13 oveq2 7153 . . . . . 6 (𝑗 = (𝑘 + 1) → ((1 + 𝐴)↑𝑗) = ((1 + 𝐴)↑(𝑘 + 1)))
1412, 13breq12d 5065 . . . . 5 (𝑗 = (𝑘 + 1) → ((1 + (𝐴 · 𝑗)) ≤ ((1 + 𝐴)↑𝑗) ↔ (1 + (𝐴 · (𝑘 + 1))) ≤ ((1 + 𝐴)↑(𝑘 + 1))))
1514imbi2d 344 . . . 4 (𝑗 = (𝑘 + 1) → (((𝐴 ∈ ℝ ∧ -1 ≤ 𝐴) → (1 + (𝐴 · 𝑗)) ≤ ((1 + 𝐴)↑𝑗)) ↔ ((𝐴 ∈ ℝ ∧ -1 ≤ 𝐴) → (1 + (𝐴 · (𝑘 + 1))) ≤ ((1 + 𝐴)↑(𝑘 + 1)))))
16 oveq2 7153 . . . . . . 7 (𝑗 = 𝑁 → (𝐴 · 𝑗) = (𝐴 · 𝑁))
1716oveq2d 7161 . . . . . 6 (𝑗 = 𝑁 → (1 + (𝐴 · 𝑗)) = (1 + (𝐴 · 𝑁)))
18 oveq2 7153 . . . . . 6 (𝑗 = 𝑁 → ((1 + 𝐴)↑𝑗) = ((1 + 𝐴)↑𝑁))
1917, 18breq12d 5065 . . . . 5 (𝑗 = 𝑁 → ((1 + (𝐴 · 𝑗)) ≤ ((1 + 𝐴)↑𝑗) ↔ (1 + (𝐴 · 𝑁)) ≤ ((1 + 𝐴)↑𝑁)))
2019imbi2d 344 . . . 4 (𝑗 = 𝑁 → (((𝐴 ∈ ℝ ∧ -1 ≤ 𝐴) → (1 + (𝐴 · 𝑗)) ≤ ((1 + 𝐴)↑𝑗)) ↔ ((𝐴 ∈ ℝ ∧ -1 ≤ 𝐴) → (1 + (𝐴 · 𝑁)) ≤ ((1 + 𝐴)↑𝑁))))
21 recn 10619 . . . . . 6 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
22 mul01 10811 . . . . . . . . 9 (𝐴 ∈ ℂ → (𝐴 · 0) = 0)
2322oveq2d 7161 . . . . . . . 8 (𝐴 ∈ ℂ → (1 + (𝐴 · 0)) = (1 + 0))
24 1p0e1 11754 . . . . . . . 8 (1 + 0) = 1
2523, 24syl6eq 2875 . . . . . . 7 (𝐴 ∈ ℂ → (1 + (𝐴 · 0)) = 1)
26 1le1 11260 . . . . . . . 8 1 ≤ 1
27 ax-1cn 10587 . . . . . . . . . 10 1 ∈ ℂ
28 addcl 10611 . . . . . . . . . 10 ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 + 𝐴) ∈ ℂ)
2927, 28mpan 689 . . . . . . . . 9 (𝐴 ∈ ℂ → (1 + 𝐴) ∈ ℂ)
30 exp0 13434 . . . . . . . . 9 ((1 + 𝐴) ∈ ℂ → ((1 + 𝐴)↑0) = 1)
3129, 30syl 17 . . . . . . . 8 (𝐴 ∈ ℂ → ((1 + 𝐴)↑0) = 1)
3226, 31breqtrrid 5090 . . . . . . 7 (𝐴 ∈ ℂ → 1 ≤ ((1 + 𝐴)↑0))
3325, 32eqbrtrd 5074 . . . . . 6 (𝐴 ∈ ℂ → (1 + (𝐴 · 0)) ≤ ((1 + 𝐴)↑0))
3421, 33syl 17 . . . . 5 (𝐴 ∈ ℝ → (1 + (𝐴 · 0)) ≤ ((1 + 𝐴)↑0))
3534adantr 484 . . . 4 ((𝐴 ∈ ℝ ∧ -1 ≤ 𝐴) → (1 + (𝐴 · 0)) ≤ ((1 + 𝐴)↑0))
36 1re 10633 . . . . . . . . . . . . 13 1 ∈ ℝ
37 nn0re 11899 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0𝑘 ∈ ℝ)
38 remulcl 10614 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝐴 · 𝑘) ∈ ℝ)
3937, 38sylan2 595 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → (𝐴 · 𝑘) ∈ ℝ)
40 readdcl 10612 . . . . . . . . . . . . 13 ((1 ∈ ℝ ∧ (𝐴 · 𝑘) ∈ ℝ) → (1 + (𝐴 · 𝑘)) ∈ ℝ)
4136, 39, 40sylancr 590 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → (1 + (𝐴 · 𝑘)) ∈ ℝ)
42 simpl 486 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ ℝ)
43 readdcl 10612 . . . . . . . . . . . 12 (((1 + (𝐴 · 𝑘)) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((1 + (𝐴 · 𝑘)) + 𝐴) ∈ ℝ)
4441, 42, 43syl2anc 587 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((1 + (𝐴 · 𝑘)) + 𝐴) ∈ ℝ)
4544adantr 484 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (-1 ≤ 𝐴 ∧ (1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘))) → ((1 + (𝐴 · 𝑘)) + 𝐴) ∈ ℝ)
46 readdcl 10612 . . . . . . . . . . . . . 14 ((1 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (1 + 𝐴) ∈ ℝ)
4736, 46mpan 689 . . . . . . . . . . . . 13 (𝐴 ∈ ℝ → (1 + 𝐴) ∈ ℝ)
4847adantr 484 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → (1 + 𝐴) ∈ ℝ)
4941, 48remulcld 10663 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((1 + (𝐴 · 𝑘)) · (1 + 𝐴)) ∈ ℝ)
5049adantr 484 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (-1 ≤ 𝐴 ∧ (1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘))) → ((1 + (𝐴 · 𝑘)) · (1 + 𝐴)) ∈ ℝ)
51 reexpcl 13447 . . . . . . . . . . . . 13 (((1 + 𝐴) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((1 + 𝐴)↑𝑘) ∈ ℝ)
5247, 51sylan 583 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((1 + 𝐴)↑𝑘) ∈ ℝ)
5352, 48remulcld 10663 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → (((1 + 𝐴)↑𝑘) · (1 + 𝐴)) ∈ ℝ)
5453adantr 484 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (-1 ≤ 𝐴 ∧ (1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘))) → (((1 + 𝐴)↑𝑘) · (1 + 𝐴)) ∈ ℝ)
55 remulcl 10614 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐴 · 𝐴) ∈ ℝ)
5655anidms 570 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℝ → (𝐴 · 𝐴) ∈ ℝ)
57 msqge0 11153 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℝ → 0 ≤ (𝐴 · 𝐴))
5856, 57jca 515 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℝ → ((𝐴 · 𝐴) ∈ ℝ ∧ 0 ≤ (𝐴 · 𝐴)))
59 nn0ge0 11915 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ0 → 0 ≤ 𝑘)
6037, 59jca 515 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 → (𝑘 ∈ ℝ ∧ 0 ≤ 𝑘))
61 mulge0 11150 . . . . . . . . . . . . . . 15 ((((𝐴 · 𝐴) ∈ ℝ ∧ 0 ≤ (𝐴 · 𝐴)) ∧ (𝑘 ∈ ℝ ∧ 0 ≤ 𝑘)) → 0 ≤ ((𝐴 · 𝐴) · 𝑘))
6258, 60, 61syl2an 598 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → 0 ≤ ((𝐴 · 𝐴) · 𝑘))
6321adantr 484 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ ℂ)
64 nn0cn 11900 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
6564adantl 485 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℂ)
6663, 63, 65mul32d 10842 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((𝐴 · 𝐴) · 𝑘) = ((𝐴 · 𝑘) · 𝐴))
6762, 66breqtrd 5078 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → 0 ≤ ((𝐴 · 𝑘) · 𝐴))
68 simpl 486 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ) → 𝐴 ∈ ℝ)
6938, 68remulcld 10663 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ) → ((𝐴 · 𝑘) · 𝐴) ∈ ℝ)
7037, 69sylan2 595 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((𝐴 · 𝑘) · 𝐴) ∈ ℝ)
7144, 70addge01d 11220 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → (0 ≤ ((𝐴 · 𝑘) · 𝐴) ↔ ((1 + (𝐴 · 𝑘)) + 𝐴) ≤ (((1 + (𝐴 · 𝑘)) + 𝐴) + ((𝐴 · 𝑘) · 𝐴))))
7267, 71mpbid 235 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((1 + (𝐴 · 𝑘)) + 𝐴) ≤ (((1 + (𝐴 · 𝑘)) + 𝐴) + ((𝐴 · 𝑘) · 𝐴)))
73 mulcl 10613 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐴 · 𝑘) ∈ ℂ)
74 addcl 10611 . . . . . . . . . . . . . . . 16 ((1 ∈ ℂ ∧ (𝐴 · 𝑘) ∈ ℂ) → (1 + (𝐴 · 𝑘)) ∈ ℂ)
7527, 73, 74sylancr 590 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (1 + (𝐴 · 𝑘)) ∈ ℂ)
76 simpl 486 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → 𝐴 ∈ ℂ)
7773, 76mulcld 10653 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝐴 · 𝑘) · 𝐴) ∈ ℂ)
7875, 76, 77addassd 10655 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (((1 + (𝐴 · 𝑘)) + 𝐴) + ((𝐴 · 𝑘) · 𝐴)) = ((1 + (𝐴 · 𝑘)) + (𝐴 + ((𝐴 · 𝑘) · 𝐴))))
79 muladd11 10802 . . . . . . . . . . . . . . 15 (((𝐴 · 𝑘) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((1 + (𝐴 · 𝑘)) · (1 + 𝐴)) = ((1 + (𝐴 · 𝑘)) + (𝐴 + ((𝐴 · 𝑘) · 𝐴))))
8073, 76, 79syl2anc 587 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((1 + (𝐴 · 𝑘)) · (1 + 𝐴)) = ((1 + (𝐴 · 𝑘)) + (𝐴 + ((𝐴 · 𝑘) · 𝐴))))
8178, 80eqtr4d 2862 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (((1 + (𝐴 · 𝑘)) + 𝐴) + ((𝐴 · 𝑘) · 𝐴)) = ((1 + (𝐴 · 𝑘)) · (1 + 𝐴)))
8221, 64, 81syl2an 598 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → (((1 + (𝐴 · 𝑘)) + 𝐴) + ((𝐴 · 𝑘) · 𝐴)) = ((1 + (𝐴 · 𝑘)) · (1 + 𝐴)))
8372, 82breqtrd 5078 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((1 + (𝐴 · 𝑘)) + 𝐴) ≤ ((1 + (𝐴 · 𝑘)) · (1 + 𝐴)))
8483adantr 484 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (-1 ≤ 𝐴 ∧ (1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘))) → ((1 + (𝐴 · 𝑘)) + 𝐴) ≤ ((1 + (𝐴 · 𝑘)) · (1 + 𝐴)))
8541adantr 484 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (-1 ≤ 𝐴 ∧ (1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘))) → (1 + (𝐴 · 𝑘)) ∈ ℝ)
8652adantr 484 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (-1 ≤ 𝐴 ∧ (1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘))) → ((1 + 𝐴)↑𝑘) ∈ ℝ)
8748adantr 484 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (-1 ≤ 𝐴 ∧ (1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘))) → (1 + 𝐴) ∈ ℝ)
88 neg1rr 11745 . . . . . . . . . . . . . . 15 -1 ∈ ℝ
89 leadd2 11101 . . . . . . . . . . . . . . 15 ((-1 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (-1 ≤ 𝐴 ↔ (1 + -1) ≤ (1 + 𝐴)))
9088, 36, 89mp3an13 1449 . . . . . . . . . . . . . 14 (𝐴 ∈ ℝ → (-1 ≤ 𝐴 ↔ (1 + -1) ≤ (1 + 𝐴)))
91 1pneg1e0 11749 . . . . . . . . . . . . . . 15 (1 + -1) = 0
9291breq1i 5059 . . . . . . . . . . . . . 14 ((1 + -1) ≤ (1 + 𝐴) ↔ 0 ≤ (1 + 𝐴))
9390, 92syl6bb 290 . . . . . . . . . . . . 13 (𝐴 ∈ ℝ → (-1 ≤ 𝐴 ↔ 0 ≤ (1 + 𝐴)))
9493biimpa 480 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ -1 ≤ 𝐴) → 0 ≤ (1 + 𝐴))
9594ad2ant2r 746 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (-1 ≤ 𝐴 ∧ (1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘))) → 0 ≤ (1 + 𝐴))
96 simprr 772 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (-1 ≤ 𝐴 ∧ (1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘))) → (1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘))
9785, 86, 87, 95, 96lemul1ad 11571 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (-1 ≤ 𝐴 ∧ (1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘))) → ((1 + (𝐴 · 𝑘)) · (1 + 𝐴)) ≤ (((1 + 𝐴)↑𝑘) · (1 + 𝐴)))
9845, 50, 54, 84, 97letrd 10789 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (-1 ≤ 𝐴 ∧ (1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘))) → ((1 + (𝐴 · 𝑘)) + 𝐴) ≤ (((1 + 𝐴)↑𝑘) · (1 + 𝐴)))
99 adddi 10618 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 · (𝑘 + 1)) = ((𝐴 · 𝑘) + (𝐴 · 1)))
10027, 99mp3an3 1447 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐴 · (𝑘 + 1)) = ((𝐴 · 𝑘) + (𝐴 · 1)))
101 mulid1 10631 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
102101adantr 484 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐴 · 1) = 𝐴)
103102oveq2d 7161 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝐴 · 𝑘) + (𝐴 · 1)) = ((𝐴 · 𝑘) + 𝐴))
104100, 103eqtrd 2859 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐴 · (𝑘 + 1)) = ((𝐴 · 𝑘) + 𝐴))
105104oveq2d 7161 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (1 + (𝐴 · (𝑘 + 1))) = (1 + ((𝐴 · 𝑘) + 𝐴)))
106 addass 10616 . . . . . . . . . . . . 13 ((1 ∈ ℂ ∧ (𝐴 · 𝑘) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((1 + (𝐴 · 𝑘)) + 𝐴) = (1 + ((𝐴 · 𝑘) + 𝐴)))
10727, 73, 76, 106mp3an2i 1463 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((1 + (𝐴 · 𝑘)) + 𝐴) = (1 + ((𝐴 · 𝑘) + 𝐴)))
108105, 107eqtr4d 2862 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (1 + (𝐴 · (𝑘 + 1))) = ((1 + (𝐴 · 𝑘)) + 𝐴))
10921, 64, 108syl2an 598 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → (1 + (𝐴 · (𝑘 + 1))) = ((1 + (𝐴 · 𝑘)) + 𝐴))
110109adantr 484 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (-1 ≤ 𝐴 ∧ (1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘))) → (1 + (𝐴 · (𝑘 + 1))) = ((1 + (𝐴 · 𝑘)) + 𝐴))
11127, 21, 28sylancr 590 . . . . . . . . . . 11 (𝐴 ∈ ℝ → (1 + 𝐴) ∈ ℂ)
112 expp1 13437 . . . . . . . . . . 11 (((1 + 𝐴) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((1 + 𝐴)↑(𝑘 + 1)) = (((1 + 𝐴)↑𝑘) · (1 + 𝐴)))
113111, 112sylan 583 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((1 + 𝐴)↑(𝑘 + 1)) = (((1 + 𝐴)↑𝑘) · (1 + 𝐴)))
114113adantr 484 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (-1 ≤ 𝐴 ∧ (1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘))) → ((1 + 𝐴)↑(𝑘 + 1)) = (((1 + 𝐴)↑𝑘) · (1 + 𝐴)))
11598, 110, 1143brtr4d 5084 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (-1 ≤ 𝐴 ∧ (1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘))) → (1 + (𝐴 · (𝑘 + 1))) ≤ ((1 + 𝐴)↑(𝑘 + 1)))
116115exp43 440 . . . . . . 7 (𝐴 ∈ ℝ → (𝑘 ∈ ℕ0 → (-1 ≤ 𝐴 → ((1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘) → (1 + (𝐴 · (𝑘 + 1))) ≤ ((1 + 𝐴)↑(𝑘 + 1))))))
117116com12 32 . . . . . 6 (𝑘 ∈ ℕ0 → (𝐴 ∈ ℝ → (-1 ≤ 𝐴 → ((1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘) → (1 + (𝐴 · (𝑘 + 1))) ≤ ((1 + 𝐴)↑(𝑘 + 1))))))
118117impd 414 . . . . 5 (𝑘 ∈ ℕ0 → ((𝐴 ∈ ℝ ∧ -1 ≤ 𝐴) → ((1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘) → (1 + (𝐴 · (𝑘 + 1))) ≤ ((1 + 𝐴)↑(𝑘 + 1)))))
119118a2d 29 . . . 4 (𝑘 ∈ ℕ0 → (((𝐴 ∈ ℝ ∧ -1 ≤ 𝐴) → (1 + (𝐴 · 𝑘)) ≤ ((1 + 𝐴)↑𝑘)) → ((𝐴 ∈ ℝ ∧ -1 ≤ 𝐴) → (1 + (𝐴 · (𝑘 + 1))) ≤ ((1 + 𝐴)↑(𝑘 + 1)))))
1205, 10, 15, 20, 35, 119nn0ind 12070 . . 3 (𝑁 ∈ ℕ0 → ((𝐴 ∈ ℝ ∧ -1 ≤ 𝐴) → (1 + (𝐴 · 𝑁)) ≤ ((1 + 𝐴)↑𝑁)))
121120expd 419 . 2 (𝑁 ∈ ℕ0 → (𝐴 ∈ ℝ → (-1 ≤ 𝐴 → (1 + (𝐴 · 𝑁)) ≤ ((1 + 𝐴)↑𝑁))))
1221213imp21 1111 1 ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ -1 ≤ 𝐴) → (1 + (𝐴 · 𝑁)) ≤ ((1 + 𝐴)↑𝑁))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2115   class class class wbr 5052  (class class class)co 7145  ℂcc 10527  ℝcr 10528  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534   ≤ cle 10668  -cneg 10863  ℕ0cn0 11890  ↑cexp 13430 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7451  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4276  df-if 4450  df-pw 4523  df-sn 4550  df-pr 4552  df-tp 4554  df-op 4556  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7571  df-2nd 7680  df-wrecs 7937  df-recs 7998  df-rdg 8036  df-er 8279  df-en 8500  df-dom 8501  df-sdom 8502  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11631  df-n0 11891  df-z 11975  df-uz 12237  df-seq 13370  df-exp 13431 This theorem is referenced by:  bernneq2  13592  stoweidlem1  42506  stoweidlem10  42515  stoweidlem42  42547
 Copyright terms: Public domain W3C validator