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 N 0 1 A 1 + A N 1 + A N

Proof

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