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 < 𝐴 ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝐴 ↑ 𝑀 ) ≤ ( 𝐴 ↑ 𝑁 ) ) )