ltexp2a

Description: Exponent ordering relationship for exponentiation of a fixed real base greater than 1 to integer exponents. (Contributed by NM, 2-Aug-2006) (Revised by Mario Carneiro, 4-Jun-2014)

		Ref	Expression
	Assertion	ltexp2a	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to A^{M} < A^{N}$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to A \in ℝ$
2		0red	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to 0 \in ℝ$
3		1red	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to 1 \in ℝ$
4		0lt1	$⊢ 0 < 1$
5	4	a1i	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to 0 < 1$
6		simprl	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to 1 < A$
7	2 3 1 5 6	lttrd	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to 0 < A$
8	1 7	elrpd	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to A \in ℝ^{+}$
9		simpl2	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to M \in ℤ$
10		rpexpcl	$⊢ (A \in ℝ^{+} \land M \in ℤ) \to A^{M} \in ℝ^{+}$
11	8 9 10	syl2anc	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to A^{M} \in ℝ^{+}$
12	11	rpred	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to A^{M} \in ℝ$
13	12	recnd	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to A^{M} \in ℂ$
14	13	mullidd	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to 1 A^{M} = A^{M}$
15		simprr	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to M < N$
16		simpl3	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to N \in ℤ$
17		znnsub	$⊢ (M \in ℤ \land N \in ℤ) \to (M < N \leftrightarrow N - M \in ℕ)$
18	9 16 17	syl2anc	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to (M < N \leftrightarrow N - M \in ℕ)$
19	15 18	mpbid	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to N - M \in ℕ$
20		expgt1	$⊢ (A \in ℝ \land N - M \in ℕ \land 1 < A) \to 1 < A^{N - M}$
21	1 19 6 20	syl3anc	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to 1 < A^{N - M}$
22	1	recnd	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to A \in ℂ$
23	7	gt0ne0d	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to A \neq 0$
24		expsub	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℤ \land M \in ℤ)) \to A^{N - M} = \frac{A^{N}}{A^{M}}$
25	22 23 16 9 24	syl22anc	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to A^{N - M} = \frac{A^{N}}{A^{M}}$
26	21 25	breqtrd	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to 1 < \frac{A^{N}}{A^{M}}$
27		rpexpcl	$⊢ (A \in ℝ^{+} \land N \in ℤ) \to A^{N} \in ℝ^{+}$
28	8 16 27	syl2anc	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to A^{N} \in ℝ^{+}$
29	28	rpred	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to A^{N} \in ℝ$
30	3 29 11	ltmuldivd	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to (1 A^{M} < A^{N} \leftrightarrow 1 < \frac{A^{N}}{A^{M}})$
31	26 30	mpbird	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to 1 A^{M} < A^{N}$
32	14 31	eqbrtrrd	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land (1 < A \land M < N)) \to A^{M} < A^{N}$

Metamath Proof Explorer

Theorem ltexp2a

Proof