Metamath Proof Explorer

Theorem rpexpmord

Description: Base ordering relationship for exponentiation of positive reals to a fixed positive integer exponent. (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 ) ) )