Theorem bernneq 6652

Description: Bernoulli's inequality, due to Johan Bernoulli (1667-1748).

Assertion

Ref	Expression
bernneq	|- ((A e. RR /\ N e. NN0 /\ -u1 <_ A) -> (1 + (A x. N)) <_ ((1 + A)^N))

Proof of Theorem bernneq

Step	Hyp	Ref	Expression
1		opreq2 3969	. . . . . . . 8 |- (j = 0 -> (A x. j) = (A x. 0))
2	1	opreq2d 3976	. . . . . . 7 |- (j = 0 -> (1 + (A x. j)) = (1 + (A x. 0)))
3		opreq2 3969	. . . . . . 7 |- (j = 0 -> ((1 + A)^j) = ((1 + A)^0))
4	2, 3	breq12d 2631	. . . . . 6 |- (j = 0 -> ((1 + (A x. j)) <_ ((1 + A)^j) <-> (1 + (A x. 0)) <_ ((1 + A)^0)))
5	4	imbi2d 612	. . . . 5 |- (j = 0 -> (((A e. RR /\ -u1 <_ A) -> (1 + (A x. j)) <_ ((1 + A)^j)) <-> ((A e. RR /\ -u1 <_ A) -> (1 + (A x. 0)) <_ ((1 + A)^0))))
6		opreq2 3969	. . . . . . . 8 |- (j = k -> (A x. j) = (A x. k))
7	6	opreq2d 3976	. . . . . . 7 |- (j = k -> (1 + (A x. j)) = (1 + (A x. k)))
8		opreq2 3969	. . . . . . 7 |- (j = k -> ((1 + A)^j) = ((1 + A)^k))
9	7, 8	breq12d 2631	. . . . . 6 |- (j = k -> ((1 + (A x. j)) <_ ((1 + A)^j) <-> (1 + (A x. k)) <_ ((1 + A)^k)))
10	9	imbi2d 612	. . . . 5 |- (j = k -> (((A e. RR /\ -u1 <_ A) -> (1 + (A x. j)) <_ ((1 + A)^j)) <-> ((A e. RR /\ -u1 <_ A) -> (1 + (A x. k)) <_ ((1 + A)^k))))
11		opreq2 3969	. . . . . . . 8 |- (j = (k + 1) -> (A x. j) = (A x. (k + 1)))
12	11	opreq2d 3976	. . . . . . 7 |- (j = (k + 1) -> (1 + (A x. j)) = (1 + (A x. (k + 1))))
13		opreq2 3969	. . . . . . 7 |- (j = (k + 1) -> ((1 + A)^j) = ((1 + A)^(k + 1)))
14	12, 13	breq12d 2631	. . . . . 6 |- (j = (k + 1) -> ((1 + (A x. j)) <_ ((1 + A)^j) <-> (1 + (A x. (k + 1))) <_ ((1 + A)^(k + 1))))
15	14	imbi2d 612	. . . . 5 |- (j = (k + 1) -> (((A e. RR /\ -u1 <_ A) -> (1 + (A x. j)) <_ ((1 + A)^j)) <-> ((A e. RR /\ -u1 <_ A) -> (1 + (A x. (k + 1))) <_ ((1 + A)^(k + 1)))))
16		opreq2 3969	. . . . . . . 8 |- (j = N -> (A x. j) = (A x. N))
17	16	opreq2d 3976	. . . . . . 7 |- (j = N -> (1 + (A x. j)) = (1 + (A x. N)))
18		opreq2 3969	. . . . . . 7 |- (j = N -> ((1 + A)^j) = ((1 + A)^N))
19	17, 18	breq12d 2631	. . . . . 6 |- (j = N -> ((1 + (A x. j)) <_ ((1 + A)^j) <-> (1 + (A x. N)) <_ ((1 + A)^N)))
20	19	imbi2d 612	. . . . 5 |- (j = N -> (((A e. RR /\ -u1 <_ A) -> (1 + (A x. j)) <_ ((1 + A)^j)) <-> ((A e. RR /\ -u1 <_ A) -> (1 + (A x. N)) <_ ((1 + A)^N))))
21		recnt 5313	. . . . . . 7 |- (A e. RR -> A e. CC)
22		mul01t 5443	. . . . . . . . . 10 |- (A e. CC -> (A x. 0) = 0)
23	22	opreq2d 3976	. . . . . . . . 9 |- (A e. CC -> (1 + (A x. 0)) = (1 + 0))
24		ax1cn 5269	. . . . . . . . . 10 |- 1 e. CC
25	24	addid1 5330	. . . . . . . . 9 |- (1 + 0) = 1
26	23, 25	syl6eq 1523	. . . . . . . 8 |- (A e. CC -> (1 + (A x. 0)) = 1)
27		axaddcl 5271	. . . . . . . . . . 11 |- ((1 e. CC /\ A e. CC) -> (1 + A) e. CC)
28	24, 27	mpan 695	. . . . . . . . . 10 |- (A e. CC -> (1 + A) e. CC)
29		exp0t 6571	. . . . . . . . . 10 |- ((1 + A) e. CC -> ((1 + A)^0) = 1)
30	28, 29	syl 10	. . . . . . . . 9 |- (A e. CC -> ((1 + A)^0) = 1)
31		1re 5435	. . . . . . . . . 10 |- 1 e. RR
32	31	leid 5610	. . . . . . . . 9 |- 1 <_ 1
33	30, 32	syl5breqr 2651	. . . . . . . 8 |- (A e. CC -> 1 <_ ((1 + A)^0))
34	26, 33	eqbrtrd 2635	. . . . . . 7 |- (A e. CC -> (1 + (A x. 0)) <_ ((1 + A)^0))
35	21, 34	syl 10	. . . . . 6 |- (A e. RR -> (1 + (A x. 0)) <_ ((1 + A)^0))
36	35	adantr 389	. . . . 5 |- ((A e. RR /\ -u1 <_ A) -> (1 + (A x. 0)) <_ ((1 + A)^0))
37		axaddrcl 5272	. . . . . . . . . . . . 13 |- (((1 + (A x. k)) e. RR /\ A e. RR) -> ((1 + (A x. k)) + A) e. RR)
38		axmulrcl 5274	. . . . . . . . . . . . . . 15 |- ((A e. RR /\ k e. RR) -> (A x. k) e. RR)
39		nn0ret 6108	. . . . . . . . . . . . . . 15 |- (k e. NN0 -> k e. RR)
40	38, 39	sylan2 451	. . . . . . . . . . . . . 14 |- ((A e. RR /\ k e. NN0) -> (A x. k) e. RR)
41		axaddrcl 5272	. . . . . . . . . . . . . . 15 |- ((1 e. RR /\ (A x. k) e. RR) -> (1 + (A x. k)) e. RR)
42	31, 41	mpan 695	. . . . . . . . . . . . . 14 |- ((A x. k) e. RR -> (1 + (A x. k)) e. RR)
43	40, 42	syl 10	. . . . . . . . . . . . 13 |- ((A e. RR /\ k e. NN0) -> (1 + (A x. k)) e. RR)
44		pm3.26 319	. . . . . . . . . . . . 13 |- ((A e. RR /\ k e. NN0) -> A e. RR)
45	37, 43, 44	sylanc 471	. . . . . . . . . . . 12 |- ((A e. RR /\ k e. NN0) -> ((1 + (A x. k)) + A) e. RR)
46	45	adantr 389	. . . . . . . . . . 11 |- (((A e. RR /\ k e. NN0) /\ (-u1 <_ A /\ (1 + (A x. k)) <_ ((1 + A)^k))) -> ((1 + (A x. k)) + A) e. RR)
47		axmulrcl 5274	. . . . . . . . . . . . 13 |- (((1 + (A x. k)) e. RR /\ (1 + A) e. RR) -> ((1 + (A x. k)) x. (1 + A)) e. RR)
48		axaddrcl 5272	. . . . . . . . . . . . . . 15 |- ((1 e. RR /\ A e. RR) -> (1 + A) e. RR)
49	31, 48	mpan 695	. . . . . . . . . . . . . 14 |- (A e. RR -> (1 + A) e. RR)
50	49	adantr 389	. . . . . . . . . . . . 13 |- ((A e. RR /\ k e. NN0) -> (1 + A) e. RR)
51	47, 43, 50	sylanc 471	. . . . . . . . . . . 12 |- ((A e. RR /\ k e. NN0) -> ((1 + (A x. k)) x. (1 + A)) e. RR)
52	51	adantr 389	. . . . . . . . . . 11 |- (((A e. RR /\ k e. NN0) /\ (-u1 <_ A /\ (1 + (A x. k)) <_ ((1 + A)^k))) -> ((1 + (A x. k)) x. (1 + A)) e. RR)
53		axmulrcl 5274	. . . . . . . . . . . . 13 |- ((((1 + A)^k) e. RR /\ (1 + A) e. RR) -> (((1 + A)^k) x. (1 + A)) e. RR)
54		reexpclt 6580	. . . . . . . . . . . . . 14 |- (((1 + A) e. RR /\ k e. NN0) -> ((1 + A)^k) e. RR)
55	54, 49	sylan 448	. . . . . . . . . . . . 13 |- ((A e. RR /\ k e. NN0) -> ((1 + A)^k) e. RR)
56	53, 55, 50	sylanc 471	. . . . . . . . . . . 12 |- ((A e. RR /\ k e. NN0) -> (((1 + A)^k) x. (1 + A)) e. RR)
57	56	adantr 389	. . . . . . . . . . 11 |- (((A e. RR /\ k e. NN0) /\ (-u1 <_ A /\ (1 + (A x. k)) <_ ((1 + A)^k))) -> (((1 + A)^k) x. (1 + A)) e. RR)
58		mulge0t 5679	. . . . . . . . . . . . . . . 16 |- ((((A x. A) e. RR /\ k e. RR) /\ (0 <_ (A x. A) /\ 0 <_ k)) -> 0 <_ ((A x. A) x. k))
59		axmulrcl 5274	. . . . . . . . . . . . . . . . . 18 |- ((A e. RR /\ A e. RR) -> (A x. A) e. RR)
60	59	anidms 434	. . . . . . . . . . . . . . . . 17 |- (A e. RR -> (A x. A) e. RR)
61	60, 39	anim12i 333	. . . . . . . . . . . . . . . 16 |- ((A e. RR /\ k e. NN0) -> ((A x. A) e. RR /\ k e. RR))
62		msqge0t 5616	. . . . . . . . . . . . . . . . 17 |- (A e. RR -> 0 <_ (A x. A))
63		nn0ge0t 6117	. . . . . . . . . . . . . . . . 17 |- (k e. NN0 -> 0 <_ k)
64	62, 63	anim12i 333	. . . . . . . . . . . . . . . 16 |- ((A e. RR /\ k e. NN0) -> (0 <_ (A x. A) /\ 0 <_ k))
65	58, 61, 64	sylanc 471	. . . . . . . . . . . . . . 15 |- ((A e. RR /\ k e. NN0) -> 0 <_ ((A x. A) x. k))
66		mul23t 5419	. . . . . . . . . . . . . . . 16 |- ((A e. CC /\ A e. CC /\ k e. CC) -> ((A x. A) x. k) = ((A x. k) x. A))
67	21	adantr 389	. . . . . . . . . . . . . . . 16 |- ((A e. RR /\ k e. NN0) -> A e. CC)
68