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 ) ) |