Metamath Proof Explorer

Theorem stoweidlem10

Description: Lemma for stoweid . 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)

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

Proof

Step Hyp Ref Expression
1 renegcl 
 |-  ( A e. RR -> -u A e. RR )
2 1 3ad2ant1 
 |-  ( ( A e. RR /\ N e. NN0 /\ A <_ 1 ) -> -u A e. RR )
3 simp2 
 |-  ( ( A e. RR /\ N e. NN0 /\ A <_ 1 ) -> N e. NN0 )
4 simpr 
 |-  ( ( A e. RR /\ A <_ 1 ) -> A <_ 1 )
5 simpl 
 |-  ( ( A e. RR /\ A <_ 1 ) -> A e. RR )
6 1red 
 |-  ( ( A e. RR /\ A <_ 1 ) -> 1 e. RR )
7 5 6 lenegd 
 |-  ( ( A e. RR /\ A <_ 1 ) -> ( A <_ 1 <-> -u 1 <_ -u A ) )
8 4 7 mpbid 
 |-  ( ( A e. RR /\ A <_ 1 ) -> -u 1 <_ -u A )
9 8 3adant2 
 |-  ( ( A e. RR /\ N e. NN0 /\ A <_ 1 ) -> -u 1 <_ -u A )
10 bernneq 
 |-  ( ( -u A e. RR /\ N e. NN0 /\ -u 1 <_ -u A ) -> ( 1 + ( -u A x. N ) ) <_ ( ( 1 + -u A ) ^ N ) )
11 2 3 9 10 syl3anc 
 |-  ( ( A e. RR /\ N e. NN0 /\ A <_ 1 ) -> ( 1 + ( -u A x. N ) ) <_ ( ( 1 + -u A ) ^ N ) )
12 recn 
 |-  ( A e. RR -> A e. CC )
13 12 3ad2ant1 
 |-  ( ( A e. RR /\ N e. NN0 /\ A <_ 1 ) -> A e. CC )
14 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
15 14 3ad2ant2 
 |-  ( ( A e. RR /\ N e. NN0 /\ A <_ 1 ) -> N e. CC )
16 1cnd 
 |-  ( ( A e. RR /\ N e. NN0 /\ A <_ 1 ) -> 1 e. CC )
17 mulneg1 
 |-  ( ( A e. CC /\ N e. CC ) -> ( -u A x. N ) = -u ( A x. N ) )
18 17 oveq2d 
 |-  ( ( A e. CC /\ N e. CC ) -> ( 1 + ( -u A x. N ) ) = ( 1 + -u ( A x. N ) ) )
19 18 3adant3 
 |-  ( ( A e. CC /\ N e. CC /\ 1 e. CC ) -> ( 1 + ( -u A x. N ) ) = ( 1 + -u ( A x. N ) ) )
20 simp3 
 |-  ( ( A e. CC /\ N e. CC /\ 1 e. CC ) -> 1 e. CC )
21 mulcl 
 |-  ( ( A e. CC /\ N e. CC ) -> ( A x. N ) e. CC )
22 21 3adant3 
 |-  ( ( A e. CC /\ N e. CC /\ 1 e. CC ) -> ( A x. N ) e. CC )
23 20 22 negsubd 
 |-  ( ( A e. CC /\ N e. CC /\ 1 e. CC ) -> ( 1 + -u ( A x. N ) ) = ( 1 - ( A x. N ) ) )
24 mulcom 
 |-  ( ( A e. CC /\ N e. CC ) -> ( A x. N ) = ( N x. A ) )
25 24 oveq2d 
 |-  ( ( A e. CC /\ N e. CC ) -> ( 1 - ( A x. N ) ) = ( 1 - ( N x. A ) ) )
26 25 3adant3 
 |-  ( ( A e. CC /\ N e. CC /\ 1 e. CC ) -> ( 1 - ( A x. N ) ) = ( 1 - ( N x. A ) ) )
27 19 23 26 3eqtrd 
 |-  ( ( A e. CC /\ N e. CC /\ 1 e. CC ) -> ( 1 + ( -u A x. N ) ) = ( 1 - ( N x. A ) ) )
28 13 15 16 27 syl3anc 
 |-  ( ( A e. RR /\ N e. NN0 /\ A <_ 1 ) -> ( 1 + ( -u A x. N ) ) = ( 1 - ( N x. A ) ) )
29 1cnd 
 |-  ( A e. RR -> 1 e. CC )
30 29 12 negsubd 
 |-  ( A e. RR -> ( 1 + -u A ) = ( 1 - A ) )
31 30 oveq1d 
 |-  ( A e. RR -> ( ( 1 + -u A ) ^ N ) = ( ( 1 - A ) ^ N ) )
32 31 3ad2ant1 
 |-  ( ( A e. RR /\ N e. NN0 /\ A <_ 1 ) -> ( ( 1 + -u A ) ^ N ) = ( ( 1 - A ) ^ N ) )
33 11 28 32 3brtr3d 
 |-  ( ( A e. RR /\ N e. NN0 /\ A <_ 1 ) -> ( 1 - ( N x. A ) ) <_ ( ( 1 - A ) ^ N ) )