Metamath Proof Explorer


Theorem rpexpmord

Description: Base ordering relationship for exponentiation of positive reals. (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 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ+𝐵 ∈ ℝ+ ) → ( 𝐴 < 𝐵 ↔ ( 𝐴𝑁 ) < ( 𝐵𝑁 ) ) )