This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bernneq2

Description: Variation of Bernoulli's inequality bernneq . (Contributed by NM, 18-Oct-2007)

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

Proof

Step Hyp Ref Expression
1 peano2rem 
 |-  ( A e. RR -> ( A - 1 ) e. RR )
2 1 3ad2ant1 
 |-  ( ( A e. RR /\ N e. NN0 /\ 0 <_ A ) -> ( A - 1 ) e. RR )
3 simp2 
 |-  ( ( A e. RR /\ N e. NN0 /\ 0 <_ A ) -> N e. NN0 )
4 df-neg 
 |-  -u 1 = ( 0 - 1 )
5 0re 
 |-  0 e. RR
6 1re 
 |-  1 e. RR
7 lesub1 
 |-  ( ( 0 e. RR /\ A e. RR /\ 1 e. RR ) -> ( 0 <_ A <-> ( 0 - 1 ) <_ ( A - 1 ) ) )
8 5 6 7 mp3an13 
 |-  ( A e. RR -> ( 0 <_ A <-> ( 0 - 1 ) <_ ( A - 1 ) ) )
9 8 biimpa 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( 0 - 1 ) <_ ( A - 1 ) )
10 4 9 eqbrtrid 
 |-  ( ( A e. RR /\ 0 <_ A ) -> -u 1 <_ ( A - 1 ) )
11 10 3adant2 
 |-  ( ( A e. RR /\ N e. NN0 /\ 0 <_ A ) -> -u 1 <_ ( A - 1 ) )
12 bernneq 
 |-  ( ( ( A - 1 ) e. RR /\ N e. NN0 /\ -u 1 <_ ( A - 1 ) ) -> ( 1 + ( ( A - 1 ) x. N ) ) <_ ( ( 1 + ( A - 1 ) ) ^ N ) )
13 2 3 11 12 syl3anc 
 |-  ( ( A e. RR /\ N e. NN0 /\ 0 <_ A ) -> ( 1 + ( ( A - 1 ) x. N ) ) <_ ( ( 1 + ( A - 1 ) ) ^ N ) )
14 ax-1cn 
 |-  1 e. CC
15 1 recnd 
 |-  ( A e. RR -> ( A - 1 ) e. CC )
16 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
17 mulcl 
 |-  ( ( ( A - 1 ) e. CC /\ N e. CC ) -> ( ( A - 1 ) x. N ) e. CC )
18 15 16 17 syl2an 
 |-  ( ( A e. RR /\ N e. NN0 ) -> ( ( A - 1 ) x. N ) e. CC )
19 addcom 
 |-  ( ( 1 e. CC /\ ( ( A - 1 ) x. N ) e. CC ) -> ( 1 + ( ( A - 1 ) x. N ) ) = ( ( ( A - 1 ) x. N ) + 1 ) )
20 14 18 19 sylancr 
 |-  ( ( A e. RR /\ N e. NN0 ) -> ( 1 + ( ( A - 1 ) x. N ) ) = ( ( ( A - 1 ) x. N ) + 1 ) )
21 20 3adant3 
 |-  ( ( A e. RR /\ N e. NN0 /\ 0 <_ A ) -> ( 1 + ( ( A - 1 ) x. N ) ) = ( ( ( A - 1 ) x. N ) + 1 ) )
22 recn 
 |-  ( A e. RR -> A e. CC )
23 pncan3 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( 1 + ( A - 1 ) ) = A )
24 14 22 23 sylancr 
 |-  ( A e. RR -> ( 1 + ( A - 1 ) ) = A )
25 24 oveq1d 
 |-  ( A e. RR -> ( ( 1 + ( A - 1 ) ) ^ N ) = ( A ^ N ) )
26 25 3ad2ant1 
 |-  ( ( A e. RR /\ N e. NN0 /\ 0 <_ A ) -> ( ( 1 + ( A - 1 ) ) ^ N ) = ( A ^ N ) )
27 13 21 26 3brtr3d 
 |-  ( ( A e. RR /\ N e. NN0 /\ 0 <_ A ) -> ( ( ( A - 1 ) x. N ) + 1 ) <_ ( A ^ N ) )