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