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

Theorem stoweidlem10 37870
 Description: Lemma for stoweid 37925. 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 9937 . . . 4
3 simp2 1009 . . 3
4 simpr 463 . . . . 5
5 simpl 459 . . . . . 6
6 1red 9658 . . . . . 6
75, 6lenegd 10192 . . . . 5
84, 7mpbid 214 . . . 4
10 bernneq 12398 . . 3
112, 3, 9, 10syl3anc 1268 . 2
12 recn 9629 . . . 4
14 nn0cn 10879 . . . 4
16 1cnd 9659 . . 3
17 mulneg1 10055 . . . . . 6
1817oveq2d 6306 . . . . 5
19183adant3 1028 . . . 4
20 simp3 1010 . . . . 5
21 mulcl 9623 . . . . . 6
22213adant3 1028 . . . . 5
2320, 22negsubd 9992 . . . 4
24 mulcom 9625 . . . . . 6
2524oveq2d 6306 . . . . 5
26253adant3 1028 . . . 4
2719, 23, 263eqtrd 2489 . . 3
2813, 15, 16, 27syl3anc 1268 . 2
29 1cnd 9659 . . . . 5
3029, 12negsubd 9992 . . . 4
3130oveq1d 6305 . . 3