leexp2a

Description: Weak ordering relationship for exponentiation. (Contributed by NM, 14-Dec-2005) (Revised by Mario Carneiro, 5-Jun-2014)

		Ref	Expression
	Assertion	leexp2a	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to A^{M} \leq A^{N}$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to A \in ℝ$
2		0red	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to 0 \in ℝ$
3		1red	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to 1 \in ℝ$
4		0lt1	$⊢ 0 < 1$
5	4	a1i	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to 0 < 1$
6		simp2	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to 1 \leq A$
7	2 3 1 5 6	ltletrd	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to 0 < A$
8	1 7	elrpd	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to A \in ℝ^{+}$
9		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
10	9	3ad2ant3	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to M \in ℤ$
11		rpexpcl	$⊢ (A \in ℝ^{+} \land M \in ℤ) \to A^{M} \in ℝ^{+}$
12	8 10 11	syl2anc	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to A^{M} \in ℝ^{+}$
13	12	rpred	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to A^{M} \in ℝ$
14	13	recnd	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to A^{M} \in ℂ$
15	14	mulid2d	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to 1 A^{M} = A^{M}$
16		uznn0sub	$⊢ N \in ℤ_{\geq M} \to N - M \in ℕ_{0}$
17	16	3ad2ant3	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to N - M \in ℕ_{0}$
18		expge1	$⊢ (A \in ℝ \land N - M \in ℕ_{0} \land 1 \leq A) \to 1 \leq A^{N - M}$
19	1 17 6 18	syl3anc	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to 1 \leq A^{N - M}$
20	1	recnd	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to A \in ℂ$
21	7	gt0ne0d	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to A \neq 0$
22		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
23	22	3ad2ant3	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to N \in ℤ$
24		expsub	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℤ \land M \in ℤ)) \to A^{N - M} = \frac{A^{N}}{A^{M}}$
25	20 21 23 10 24	syl22anc	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to A^{N - M} = \frac{A^{N}}{A^{M}}$
26	19 25	breqtrd	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to 1 \leq \frac{A^{N}}{A^{M}}$
27		rpexpcl	$⊢ (A \in ℝ^{+} \land N \in ℤ) \to A^{N} \in ℝ^{+}$
28	8 23 27	syl2anc	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to A^{N} \in ℝ^{+}$
29	28	rpred	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to A^{N} \in ℝ$
30	3 29 12	lemuldivd	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to (1 A^{M} \leq A^{N} \leftrightarrow 1 \leq \frac{A^{N}}{A^{M}})$
31	26 30	mpbird	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to 1 A^{M} \leq A^{N}$
32	15 31	eqbrtrrd	$⊢ (A \in ℝ \land 1 \leq A \land N \in ℤ_{\geq M}) \to A^{M} \leq A^{N}$

Metamath Proof Explorer

Theorem leexp2a

Proof