Metamath Proof Explorer

Theorem cxplt2

Description: Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 15-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		cxple2	$⊢ ((B \in ℝ \land 0 \leq B) \land (A \in ℝ \land 0 \leq A) \land C \in ℝ^{+}) \to (B \leq A \leftrightarrow B^{C} \leq A^{C})$
2	1	3com12	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to (B \leq A \leftrightarrow B^{C} \leq A^{C})$
3	2	notbid	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to (\neg B \leq A \leftrightarrow \neg B^{C} \leq A^{C})$
4		simp1l	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to A \in ℝ$
5		simp2l	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to B \in ℝ$
6	4 5	ltnled	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to (A < B \leftrightarrow \neg B \leq A)$
7		simp1r	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to 0 \leq A$
8		rpre	$⊢ C \in ℝ^{+} \to C \in ℝ$
9	8	3ad2ant3	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to C \in ℝ$
10		recxpcl	$⊢ (A \in ℝ \land 0 \leq A \land C \in ℝ) \to A^{C} \in ℝ$
11	4 7 9 10	syl3anc	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to A^{C} \in ℝ$
12		simp2r	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to 0 \leq B$
13		recxpcl	$⊢ (B \in ℝ \land 0 \leq B \land C \in ℝ) \to B^{C} \in ℝ$
14	5 12 9 13	syl3anc	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to B^{C} \in ℝ$
15	11 14	ltnled	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to (A^{C} < B^{C} \leftrightarrow \neg B^{C} \leq A^{C})$
16	3 6 15	3bitr4d	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to (A < B \leftrightarrow A^{C} < B^{C})$