Description: ltmul1d for exponentiation of positive reals. (Contributed by Steven Nguyen, 22-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ltexp1d.1 | |- ( ph -> A e. RR+ ) |
|
ltexp1d.2 | |- ( ph -> B e. RR+ ) |
||
ltexp1d.3 | |- ( ph -> N e. NN ) |
||
Assertion | ltexp1d | |- ( ph -> ( A < B <-> ( A ^ N ) < ( B ^ N ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltexp1d.1 | |- ( ph -> A e. RR+ ) |
|
2 | ltexp1d.2 | |- ( ph -> B e. RR+ ) |
|
3 | ltexp1d.3 | |- ( ph -> N e. NN ) |
|
4 | rpexpmord | |- ( ( N e. NN /\ A e. RR+ /\ B e. RR+ ) -> ( A < B <-> ( A ^ N ) < ( B ^ N ) ) ) |
|
5 | 3 1 2 4 | syl3anc | |- ( ph -> ( A < B <-> ( A ^ N ) < ( B ^ N ) ) ) |