cxplt3

Description: Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-May-2016)

		Ref	Expression
	Assertion	cxplt3	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to (B < C \leftrightarrow A^{C} < A^{B})$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to A \in ℝ^{+}$
2		simprl	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to B \in ℝ$
3	2	recnd	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to B \in ℂ$
4		cxprec	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to {(\frac{1}{A})}^{B} = \frac{1}{A^{B}}$
5	1 3 4	syl2anc	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to {(\frac{1}{A})}^{B} = \frac{1}{A^{B}}$
6		simprr	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to C \in ℝ$
7	6	recnd	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to C \in ℂ$
8		cxprec	$⊢ (A \in ℝ^{+} \land C \in ℂ) \to {(\frac{1}{A})}^{C} = \frac{1}{A^{C}}$
9	1 7 8	syl2anc	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to {(\frac{1}{A})}^{C} = \frac{1}{A^{C}}$
10	5 9	breq12d	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to ({(\frac{1}{A})}^{B} < {(\frac{1}{A})}^{C} \leftrightarrow \frac{1}{A^{B}} < \frac{1}{A^{C}})$
11	1	rprecred	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to \frac{1}{A} \in ℝ$
12		simplr	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to A < 1$
13	1	reclt1d	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to (A < 1 \leftrightarrow 1 < \frac{1}{A})$
14	12 13	mpbid	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to 1 < \frac{1}{A}$
15		cxplt	$⊢ ((\frac{1}{A} \in ℝ \land 1 < \frac{1}{A}) \land (B \in ℝ \land C \in ℝ)) \to (B < C \leftrightarrow {(\frac{1}{A})}^{B} < {(\frac{1}{A})}^{C})$
16	11 14 2 6 15	syl22anc	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to (B < C \leftrightarrow {(\frac{1}{A})}^{B} < {(\frac{1}{A})}^{C})$
17		rpcxpcl	$⊢ (A \in ℝ^{+} \land C \in ℝ) \to A^{C} \in ℝ^{+}$
18	17	ad2ant2rl	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to A^{C} \in ℝ^{+}$
19		rpcxpcl	$⊢ (A \in ℝ^{+} \land B \in ℝ) \to A^{B} \in ℝ^{+}$
20	19	ad2ant2r	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to A^{B} \in ℝ^{+}$
21	18 20	ltrecd	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to (A^{C} < A^{B} \leftrightarrow \frac{1}{A^{B}} < \frac{1}{A^{C}})$
22	10 16 21	3bitr4d	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to (B < C \leftrightarrow A^{C} < A^{B})$

Metamath Proof Explorer

Theorem cxplt3

Proof