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

Metamath Proof Explorer

Theorem leexp2

Description: Ordering law for exponentiation of a fixed real base greater than 1 to integer exponents. (Contributed by Mario Carneiro, 26-Apr-2016)

Ref Expression
Assertion leexp2 ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝐴 ↑ 𝑀 ) ≤ ( 𝐴 ↑ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 3ancomb ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ↔ ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) )
2 ltexp2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( 𝑁 < 𝑀 ↔ ( 𝐴 ↑ 𝑁 ) < ( 𝐴 ↑ 𝑀 ) ) )
3 1 2 sylanb ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( 𝑁 < 𝑀 ↔ ( 𝐴 ↑ 𝑁 ) < ( 𝐴 ↑ 𝑀 ) ) )
4 3 notbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( ¬ 𝑁 < 𝑀 ↔ ¬ ( 𝐴 ↑ 𝑁 ) < ( 𝐴 ↑ 𝑀 ) ) )
5 simpl2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → 𝑀 ∈ ℤ )
6 simpl3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → 𝑁 ∈ ℤ )
7 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
8 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
9 lenlt ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑀 ) )
10 7 8 9 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑀 ) )
11 5 6 10 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( 𝑀 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑀 ) )
12 simpl1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ )
13 0red ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → 0 ∈ ℝ )
14 1red ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → 1 ∈ ℝ )
15 0lt1 ⊢ 0 < 1
16 15 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → 0 < 1 )
17 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → 1 < 𝐴 )
18 13 14 12 16 17 lttrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → 0 < 𝐴 )
19 18 gt0ne0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → 𝐴 ≠ 0 )
20 reexpclz ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ∧ 𝑀 ∈ ℤ ) → ( 𝐴 ↑ 𝑀 ) ∈ ℝ )
21 12 19 5 20 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( 𝐴 ↑ 𝑀 ) ∈ ℝ )
22 reexpclz ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℝ )
23 12 19 6 22 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℝ )
24 21 23 lenltd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( ( 𝐴 ↑ 𝑀 ) ≤ ( 𝐴 ↑ 𝑁 ) ↔ ¬ ( 𝐴 ↑ 𝑁 ) < ( 𝐴 ↑ 𝑀 ) ) )
25 4 11 24 3bitr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝐴 ↑ 𝑀 ) ≤ ( 𝐴 ↑ 𝑁 ) ) )