bernneq

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

		Ref	Expression
	Assertion	bernneq	$⊢ (A \in ℝ \land N \in ℕ_{0} \land - 1 \leq A) \to 1 + A \cdot N \leq {(1 + A)}^{N}$

Proof

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

Metamath Proof Explorer

Theorem bernneq

Proof