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	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < A) \to (M \leq N \leftrightarrow A^{M} \leq A^{N})$

Proof

Step	Hyp	Ref	Expression
1		3ancomb	$⊢ (A \in ℝ \land M \in ℤ \land N \in ℤ) \leftrightarrow (A \in ℝ \land N \in ℤ \land M \in ℤ)$
2		ltexp2	$⊢ ((A \in ℝ \land N \in ℤ \land M \in ℤ) \land 1 < A) \to (N < M \leftrightarrow A^{N} < A^{M})$
3	1 2	sylanb	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < A) \to (N < M \leftrightarrow A^{N} < A^{M})$
4	3	notbid	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < A) \to (\neg N < M \leftrightarrow \neg A^{N} < A^{M})$
5		simpl2	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < A) \to M \in ℤ$
6		simpl3	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < A) \to N \in ℤ$
7		zre	$⊢ M \in ℤ \to M \in ℝ$
8		zre	$⊢ N \in ℤ \to N \in ℝ$
9		lenlt	$⊢ (M \in ℝ \land N \in ℝ) \to (M \leq N \leftrightarrow \neg N < M)$
10	7 8 9	syl2an	$⊢ (M \in ℤ \land N \in ℤ) \to (M \leq N \leftrightarrow \neg N < M)$
11	5 6 10	syl2anc	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < A) \to (M \leq N \leftrightarrow \neg N < M)$
12		simpl1	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < A) \to A \in ℝ$
13		0red	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < A) \to 0 \in ℝ$
14		1red	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < A) \to 1 \in ℝ$
15		0lt1	$⊢ 0 < 1$
16	15	a1i	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < A) \to 0 < 1$
17		simpr	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < A) \to 1 < A$
18	13 14 12 16 17	lttrd	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < A) \to 0 < A$
19	18	gt0ne0d	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < A) \to A \neq 0$
20		reexpclz	$⊢ (A \in ℝ \land A \neq 0 \land M \in ℤ) \to A^{M} \in ℝ$
21	12 19 5 20	syl3anc	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < A) \to A^{M} \in ℝ$
22		reexpclz	$⊢ (A \in ℝ \land A \neq 0 \land N \in ℤ) \to A^{N} \in ℝ$
23	12 19 6 22	syl3anc	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < A) \to A^{N} \in ℝ$
24	21 23	lenltd	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < A) \to (A^{M} \leq A^{N} \leftrightarrow \neg A^{N} < A^{M})$
25	4 11 24	3bitr4d	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < A) \to (M \leq N \leftrightarrow A^{M} \leq A^{N})$

Metamath Proof Explorer

Theorem leexp2

Proof