Metamath Proof Explorer


Theorem ltexp1d

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

Ref Expression
Hypotheses ltexp1d.1 ( 𝜑𝐴 ∈ ℝ+ )
ltexp1d.2 ( 𝜑𝐵 ∈ ℝ+ )
ltexp1d.3 ( 𝜑𝑁 ∈ ℕ )
Assertion ltexp1d ( 𝜑 → ( 𝐴 < 𝐵 ↔ ( 𝐴𝑁 ) < ( 𝐵𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 ltexp1d.1 ( 𝜑𝐴 ∈ ℝ+ )
2 ltexp1d.2 ( 𝜑𝐵 ∈ ℝ+ )
3 ltexp1d.3 ( 𝜑𝑁 ∈ ℕ )
4 rpexpmord ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ+𝐵 ∈ ℝ+ ) → ( 𝐴 < 𝐵 ↔ ( 𝐴𝑁 ) < ( 𝐵𝑁 ) ) )
5 3 1 2 4 syl3anc ( 𝜑 → ( 𝐴 < 𝐵 ↔ ( 𝐴𝑁 ) < ( 𝐵𝑁 ) ) )