Metamath Proof Explorer

Theorem cxple3

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

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

Proof

Step	Hyp	Ref	Expression
1		cxplt3	$⊢ ((A \in ℝ^{+} \land A < 1) \land (C \in ℝ \land B \in ℝ)) \to (C < B \leftrightarrow A^{B} < A^{C})$
2	1	ancom2s	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to (C < B \leftrightarrow A^{B} < A^{C})$
3	2	notbid	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to (\neg C < B \leftrightarrow \neg A^{B} < A^{C})$
4		lenlt	$⊢ (B \in ℝ \land C \in ℝ) \to (B \leq C \leftrightarrow \neg C < B)$
5	4	adantl	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to (B \leq C \leftrightarrow \neg C < B)$
6		rpcxpcl	$⊢ (A \in ℝ^{+} \land C \in ℝ) \to A^{C} \in ℝ^{+}$
7	6	ad2ant2rl	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to A^{C} \in ℝ^{+}$
8		rpcxpcl	$⊢ (A \in ℝ^{+} \land B \in ℝ) \to A^{B} \in ℝ^{+}$
9	8	ad2ant2r	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to A^{B} \in ℝ^{+}$
10		rpre	$⊢ A^{C} \in ℝ^{+} \to A^{C} \in ℝ$
11		rpre	$⊢ A^{B} \in ℝ^{+} \to A^{B} \in ℝ$
12		lenlt	$⊢ (A^{C} \in ℝ \land A^{B} \in ℝ) \to (A^{C} \leq A^{B} \leftrightarrow \neg A^{B} < A^{C})$
13	10 11 12	syl2an	$⊢ (A^{C} \in ℝ^{+} \land A^{B} \in ℝ^{+}) \to (A^{C} \leq A^{B} \leftrightarrow \neg A^{B} < A^{C})$
14	7 9 13	syl2anc	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to (A^{C} \leq A^{B} \leftrightarrow \neg A^{B} < A^{C})$
15	3 5 14	3bitr4d	$⊢ ((A \in ℝ^{+} \land A < 1) \land (B \in ℝ \land C \in ℝ)) \to (B \leq C \leftrightarrow A^{C} \leq A^{B})$