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 + 𝐴 ) ↑ 𝑁 ) )