This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ltexp1d

Description: Elevating to a positive power does not affect inequalities. Similar to ltmul1d for exponentiation of positive reals. (Contributed by Steven Nguyen, 22-Aug-2023)

	Ref	Expression
Hypotheses	ltexp1d.1	$⊢ φ \to A \in ℝ^{+}$
	ltexp1d.2	$⊢ φ \to B \in ℝ^{+}$
	ltexp1d.3	$⊢ φ \to N \in ℕ$
Assertion	ltexp1d	$⊢ φ \to (A < B \leftrightarrow A^{N} < B^{N})$

Proof

Step	Hyp	Ref	Expression
1		ltexp1d.1	$⊢ φ \to A \in ℝ^{+}$
2		ltexp1d.2	$⊢ φ \to B \in ℝ^{+}$
3		ltexp1d.3	$⊢ φ \to N \in ℕ$
4		rpexpmord	$⊢ (N \in ℕ \land A \in ℝ^{+} \land B \in ℝ^{+}) \to (A < B \leftrightarrow A^{N} < B^{N})$
5	3 1 2 4	syl3anc	$⊢ φ \to (A < B \leftrightarrow A^{N} < B^{N})$