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 A + B + 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 +
5 rpre a + a
6 nnnn0 N N 0
7 reexpcl a N 0 a N
8 5 6 7 syl2anr N a + a N
9 simplrl N a + b + a < b a +
10 9 rpred N a + b + a < b a
11 simplrr N a + b + a < b b +
12 11 rpred N a + b + a < b b
13 9 rpge0d N a + b + a < b 0 a
14 simpr N a + b + a < b a < b
15 simpll N a + b + a < b N
16 expmordi a b 0 a a < b N a N < b N
17 10 12 13 14 15 16 syl221anc N a + b + a < b a N < b N
18 17 ex N a + b + a < b a N < b N
19 1 2 3 4 8 18 ltord1 N A + B + A < B A N < B N
20 19 3impb N A + B + A < B A N < B N