Metamath Proof Explorer


Theorem rpexpmord

Description: Base ordering relationship for exponentiation of positive reals. (Contributed by Stefan O'Rear, 16-Oct-2014)

Ref Expression
Assertion rpexpmord
|- ( ( N e. NN /\ A e. RR+ /\ B e. RR+ ) -> ( A < B <-> ( A ^ N ) < ( B ^ N ) ) )

Proof

Step Hyp Ref Expression
1 oveq1
 |-  ( a = b -> ( a ^ N ) = ( b ^ N ) )
2 oveq1
 |-  ( a = A -> ( a ^ N ) = ( A ^ N ) )
3 oveq1
 |-  ( a = B -> ( a ^ N ) = ( B ^ N ) )
4 rpssre
 |-  RR+ C_ RR
5 rpre
 |-  ( a e. RR+ -> a e. RR )
6 nnnn0
 |-  ( N e. NN -> N e. NN0 )
7 reexpcl
 |-  ( ( a e. RR /\ N e. NN0 ) -> ( a ^ N ) e. RR )
8 5 6 7 syl2anr
 |-  ( ( N e. NN /\ a e. RR+ ) -> ( a ^ N ) e. RR )
9 simplrl
 |-  ( ( ( N e. NN /\ ( a e. RR+ /\ b e. RR+ ) ) /\ a < b ) -> a e. RR+ )
10 9 rpred
 |-  ( ( ( N e. NN /\ ( a e. RR+ /\ b e. RR+ ) ) /\ a < b ) -> a e. RR )
11 simplrr
 |-  ( ( ( N e. NN /\ ( a e. RR+ /\ b e. RR+ ) ) /\ a < b ) -> b e. RR+ )
12 11 rpred
 |-  ( ( ( N e. NN /\ ( a e. RR+ /\ b e. RR+ ) ) /\ a < b ) -> b e. RR )
13 9 rpge0d
 |-  ( ( ( N e. NN /\ ( a e. RR+ /\ b e. RR+ ) ) /\ a < b ) -> 0 <_ a )
14 simpr
 |-  ( ( ( N e. NN /\ ( a e. RR+ /\ b e. RR+ ) ) /\ a < b ) -> a < b )
15 simpll
 |-  ( ( ( N e. NN /\ ( a e. RR+ /\ b e. RR+ ) ) /\ a < b ) -> N e. NN )
16 expmordi
 |-  ( ( ( a e. RR /\ b e. RR ) /\ ( 0 <_ a /\ a < b ) /\ N e. NN ) -> ( a ^ N ) < ( b ^ N ) )
17 10 12 13 14 15 16 syl221anc
 |-  ( ( ( N e. NN /\ ( a e. RR+ /\ b e. RR+ ) ) /\ a < b ) -> ( a ^ N ) < ( b ^ N ) )
18 17 ex
 |-  ( ( N e. NN /\ ( a e. RR+ /\ b e. RR+ ) ) -> ( a < b -> ( a ^ N ) < ( b ^ N ) ) )
19 1 2 3 4 8 18 ltord1
 |-  ( ( N e. NN /\ ( A e. RR+ /\ B e. RR+ ) ) -> ( A < B <-> ( A ^ N ) < ( B ^ N ) ) )
20 19 3impb
 |-  ( ( N e. NN /\ A e. RR+ /\ B e. RR+ ) -> ( A < B <-> ( A ^ N ) < ( B ^ N ) ) )