Metamath Proof Explorer


Theorem ltexp1d

Description: ltmul1d for exponentiation of positive reals. (Contributed by Steven Nguyen, 22-Aug-2023)

Ref Expression
Hypotheses ltexp1d.1 φ A +
ltexp1d.2 φ B +
ltexp1d.3 φ N
Assertion ltexp1d φ A < B A N < B N

Proof

Step Hyp Ref Expression
1 ltexp1d.1 φ A +
2 ltexp1d.2 φ B +
3 ltexp1d.3 φ N
4 rpexpmord N A + B + A < B A N < B N
5 3 1 2 4 syl3anc φ A < B A N < B N