Theorem 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	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 < 𝐵 ↔ ( 𝐴 ↑ 𝑁 ) < ( 𝐵 ↑ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑎 = 𝑏 → ( 𝑎 ↑ 𝑁 ) = ( 𝑏 ↑ 𝑁 ) )
2		oveq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 ↑ 𝑁 ) = ( 𝐴 ↑ 𝑁 ) )
3		oveq1	⊢ ( 𝑎 = 𝐵 → ( 𝑎 ↑ 𝑁 ) = ( 𝐵 ↑ 𝑁 ) )
4		rpssre	⊢ ℝ+ ⊆ ℝ
5		rpre	⊢ ( 𝑎 ∈ ℝ+ → 𝑎 ∈ ℝ )
6		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
7		reexpcl	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑎 ↑ 𝑁 ) ∈ ℝ )
8	5 6 7	syl2anr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑎 ∈ ℝ+ ) → ( 𝑎 ↑ 𝑁 ) ∈ ℝ )
9		simplrl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ 𝑎 < 𝑏 ) → 𝑎 ∈ ℝ+ )
10	9	rpred	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ 𝑎 < 𝑏 ) → 𝑎 ∈ ℝ )
11		simplrr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ 𝑎 < 𝑏 ) → 𝑏 ∈ ℝ+ )
12	11	rpred	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ 𝑎 < 𝑏 ) → 𝑏 ∈ ℝ )
13	9	rpge0d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ 𝑎 < 𝑏 ) → 0 ≤ 𝑎 )
14		simpr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ 𝑎 < 𝑏 ) → 𝑎 < 𝑏 )
15		simpll	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ 𝑎 < 𝑏 ) → 𝑁 ∈ ℕ )
16		expmordi	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 ≤ 𝑎 ∧ 𝑎 < 𝑏 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑎 ↑ 𝑁 ) < ( 𝑏 ↑ 𝑁 ) )
17	10 12 13 14 15 16	syl221anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ 𝑎 < 𝑏 ) → ( 𝑎 ↑ 𝑁 ) < ( 𝑏 ↑ 𝑁 ) )
18	17	ex	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → ( 𝑎 < 𝑏 → ( 𝑎 ↑ 𝑁 ) < ( 𝑏 ↑ 𝑁 ) ) )
19	1 2 3 4 8 18	ltord1	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ) → ( 𝐴 < 𝐵 ↔ ( 𝐴 ↑ 𝑁 ) < ( 𝐵 ↑ 𝑁 ) ) )
20	19	3impb	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 < 𝐵 ↔ ( 𝐴 ↑ 𝑁 ) < ( 𝐵 ↑ 𝑁 ) ) )