Metamath Proof Explorer


Theorem leexp2

Description: Ordering law for exponentiation. (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 < 𝐴 ) → ( 𝑀𝑁 ↔ ( 𝐴𝑀 ) ≤ ( 𝐴𝑁 ) ) )