rpexpmord

Description: Base ordering relationship for exponentiation of positive reals to a fixed positive integer exponent. (Contributed by Stefan O'Rear, 16-Oct-2014)

		Ref	Expression
	Assertion	rpexpmord	$⊢ (N \in ℕ \land A \in ℝ^{+} \land B \in ℝ^{+}) \to (A < B \leftrightarrow A^{N} < B^{N})$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ a = b \to a^{N} = b^{N}$
2		oveq1	$⊢ a = A \to a^{N} = A^{N}$
3		oveq1	$⊢ a = B \to a^{N} = B^{N}$
4		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
5		rpre	$⊢ a \in ℝ^{+} \to a \in ℝ$
6		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
7		reexpcl	$⊢ (a \in ℝ \land N \in ℕ_{0}) \to a^{N} \in ℝ$
8	5 6 7	syl2anr	$⊢ (N \in ℕ \land a \in ℝ^{+}) \to a^{N} \in ℝ$
9		simplrl	$⊢ ((N \in ℕ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land a < b) \to a \in ℝ^{+}$
10	9	rpred	$⊢ ((N \in ℕ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land a < b) \to a \in ℝ$
11		simplrr	$⊢ ((N \in ℕ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land a < b) \to b \in ℝ^{+}$
12	11	rpred	$⊢ ((N \in ℕ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land a < b) \to b \in ℝ$
13	9	rpge0d	$⊢ ((N \in ℕ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land a < b) \to 0 \leq a$
14		simpr	$⊢ ((N \in ℕ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land a < b) \to a < b$
15		simpll	$⊢ ((N \in ℕ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land a < b) \to N \in ℕ$
16		expmordi	$⊢ ((a \in ℝ \land b \in ℝ) \land (0 \leq a \land a < b) \land N \in ℕ) \to a^{N} < b^{N}$
17	10 12 13 14 15 16	syl221anc	$⊢ ((N \in ℕ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land a < b) \to a^{N} < b^{N}$
18	17	ex	$⊢ (N \in ℕ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \to (a < b \to a^{N} < b^{N})$
19	1 2 3 4 8 18	ltord1	$⊢ (N \in ℕ \land (A \in ℝ^{+} \land B \in ℝ^{+})) \to (A < B \leftrightarrow A^{N} < B^{N})$
20	19	3impb	$⊢ (N \in ℕ \land A \in ℝ^{+} \land B \in ℝ^{+}) \to (A < B \leftrightarrow A^{N} < B^{N})$

Metamath Proof Explorer

Theorem rpexpmord

Proof