Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem10 Unicode version

Theorem stoweidlem10 27861
 Description: Lemma for stoweid 27914. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90, this lemma is an application of Bernoulli's inequality. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Assertion
Ref Expression
stoweidlem10

Proof of Theorem stoweidlem10
StepHypRef Expression
1 renegcl 9126 . . . . 5
213ad2ant1 976 . . . 4
3 simp2 956 . . . 4
4 simpr 447 . . . . . 6
5 simpl 443 . . . . . . . 8
6 1re 8853 . . . . . . . . 9
76a1i 10 . . . . . . . 8
85, 7jca 518 . . . . . . 7
9 leneg 9293 . . . . . . 7
108, 9syl 15 . . . . . 6
114, 10mpbid 201 . . . . 5
12113adant2 974 . . . 4
132, 3, 123jca 1132 . . 3
14 bernneq 11243 . . 3
1513, 14syl 15 . 2
16 recn 8843 . . . . 5
17163ad2ant1 976 . . . 4
18 nn0cn 9991 . . . . 5
19183ad2ant2 977 . . . 4
20 ax-1cn 8811 . . . . 5
2120a1i 10 . . . 4
2217, 19, 213jca 1132 . . 3
23 mulneg1 9232 . . . . . 6
2423oveq2d 5890 . . . . 5
25243adant3 975 . . . 4
26 simp3 957 . . . . . 6
27 3simpa 952 . . . . . . 7
28 mulcl 8837 . . . . . . 7
2927, 28syl 15 . . . . . 6
3026, 29jca 518 . . . . 5
31 negsub 9111 . . . . 5
3230, 31syl 15 . . . 4
33 mulcom 8839 . . . . . 6
3433oveq2d 5890 . . . . 5
35343adant3 975 . . . 4
3625, 32, 353eqtrd 2332 . . 3
3722, 36syl 15 . 2
3820a1i 10 . . . . . 6
3938, 16jca 518 . . . . 5
40 negsub 9111 . . . . 5
4139, 40syl 15 . . . 4
4241oveq1d 5889 . . 3