ltexp2r

Description: The integer powers of a fixed positive real smaller than 1 decrease as the exponent increases. (Contributed by NM, 2-Aug-2006) (Revised by Mario Carneiro, 5-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((A \in ℝ^{+} \land M \in ℤ \land N \in ℤ) \land A < 1) \to A \in ℝ^{+}$
2	1	rpcnd	$⊢ ((A \in ℝ^{+} \land M \in ℤ \land N \in ℤ) \land A < 1) \to A \in ℂ$
3	1	rpne0d	$⊢ ((A \in ℝ^{+} \land M \in ℤ \land N \in ℤ) \land A < 1) \to A \neq 0$
4		simpl2	$⊢ ((A \in ℝ^{+} \land M \in ℤ \land N \in ℤ) \land A < 1) \to M \in ℤ$
5		exprec	$⊢ (A \in ℂ \land A \neq 0 \land M \in ℤ) \to {(\frac{1}{A})}^{M} = \frac{1}{A^{M}}$
6	2 3 4 5	syl3anc	$⊢ ((A \in ℝ^{+} \land M \in ℤ \land N \in ℤ) \land A < 1) \to {(\frac{1}{A})}^{M} = \frac{1}{A^{M}}$
7		simpl3	$⊢ ((A \in ℝ^{+} \land M \in ℤ \land N \in ℤ) \land A < 1) \to N \in ℤ$
8		exprec	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to {(\frac{1}{A})}^{N} = \frac{1}{A^{N}}$
9	2 3 7 8	syl3anc	$⊢ ((A \in ℝ^{+} \land M \in ℤ \land N \in ℤ) \land A < 1) \to {(\frac{1}{A})}^{N} = \frac{1}{A^{N}}$
10	6 9	breq12d	$⊢ ((A \in ℝ^{+} \land M \in ℤ \land N \in ℤ) \land A < 1) \to ({(\frac{1}{A})}^{M} < {(\frac{1}{A})}^{N} \leftrightarrow \frac{1}{A^{M}} < \frac{1}{A^{N}})$
11	1	rprecred	$⊢ ((A \in ℝ^{+} \land M \in ℤ \land N \in ℤ) \land A < 1) \to \frac{1}{A} \in ℝ$
12		simpr	$⊢ ((A \in ℝ^{+} \land M \in ℤ \land N \in ℤ) \land A < 1) \to A < 1$
13	1	reclt1d	$⊢ ((A \in ℝ^{+} \land M \in ℤ \land N \in ℤ) \land A < 1) \to (A < 1 \leftrightarrow 1 < \frac{1}{A})$
14	12 13	mpbid	$⊢ ((A \in ℝ^{+} \land M \in ℤ \land N \in ℤ) \land A < 1) \to 1 < \frac{1}{A}$
15		ltexp2	$⊢ ((\frac{1}{A} \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < \frac{1}{A}) \to (M < N \leftrightarrow {(\frac{1}{A})}^{M} < {(\frac{1}{A})}^{N})$
16	11 4 7 14 15	syl31anc	$⊢ ((A \in ℝ^{+} \land M \in ℤ \land N \in ℤ) \land A < 1) \to (M < N \leftrightarrow {(\frac{1}{A})}^{M} < {(\frac{1}{A})}^{N})$
17		rpexpcl	$⊢ (A \in ℝ^{+} \land N \in ℤ) \to A^{N} \in ℝ^{+}$
18	1 7 17	syl2anc	$⊢ ((A \in ℝ^{+} \land M \in ℤ \land N \in ℤ) \land A < 1) \to A^{N} \in ℝ^{+}$
19		rpexpcl	$⊢ (A \in ℝ^{+} \land M \in ℤ) \to A^{M} \in ℝ^{+}$
20	1 4 19	syl2anc	$⊢ ((A \in ℝ^{+} \land M \in ℤ \land N \in ℤ) \land A < 1) \to A^{M} \in ℝ^{+}$
21	18 20	ltrecd	$⊢ ((A \in ℝ^{+} \land M \in ℤ \land N \in ℤ) \land A < 1) \to (A^{N} < A^{M} \leftrightarrow \frac{1}{A^{M}} < \frac{1}{A^{N}})$
22	10 16 21	3bitr4d	$⊢ ((A \in ℝ^{+} \land M \in ℤ \land N \in ℤ) \land A < 1) \to (M < N \leftrightarrow A^{N} < A^{M})$

Metamath Proof Explorer

Theorem ltexp2r

Proof