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 
|- ( ( A e. RR /\ N e. NN0 /\ -u 1 <_ A ) -> ( 1 + ( A x. N ) ) <_ ( ( 1 + A ) ^ N ) )

Proof

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