cxplt

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

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

Proof

Step	Hyp	Ref	Expression
1		simprl	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to B \in ℝ$
2		rplogcl	$⊢ (A \in ℝ \land 1 < A) \to \log A \in ℝ^{+}$
3	2	adantr	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to \log A \in ℝ^{+}$
4	3	rpred	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to \log A \in ℝ$
5	1 4	remulcld	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to B \log A \in ℝ$
6		simprr	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to C \in ℝ$
7	6 4	remulcld	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to C \log A \in ℝ$
8		eflt	$⊢ (B \log A \in ℝ \land C \log A \in ℝ) \to (B \log A < C \log A \leftrightarrow e^{B \log A} < e^{C \log A})$
9	5 7 8	syl2anc	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to (B \log A < C \log A \leftrightarrow e^{B \log A} < e^{C \log A})$
10	1 6 3	ltmul1d	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to (B < C \leftrightarrow B \log A < C \log A)$
11		simpll	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to A \in ℝ$
12	11	recnd	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to A \in ℂ$
13		0red	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to 0 \in ℝ$
14		1red	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to 1 \in ℝ$
15		0lt1	$⊢ 0 < 1$
16	15	a1i	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to 0 < 1$
17		simplr	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to 1 < A$
18	13 14 11 16 17	lttrd	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to 0 < A$
19	18	gt0ne0d	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to A \neq 0$
20	1	recnd	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to B \in ℂ$
21		cxpef	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℂ) \to A^{B} = e^{B \log A}$
22	12 19 20 21	syl3anc	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to A^{B} = e^{B \log A}$
23	6	recnd	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to C \in ℂ$
24		cxpef	$⊢ (A \in ℂ \land A \neq 0 \land C \in ℂ) \to A^{C} = e^{C \log A}$
25	12 19 23 24	syl3anc	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to A^{C} = e^{C \log A}$
26	22 25	breq12d	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to (A^{B} < A^{C} \leftrightarrow e^{B \log A} < e^{C \log A})$
27	9 10 26	3bitr4d	$⊢ ((A \in ℝ \land 1 < A) \land (B \in ℝ \land C \in ℝ)) \to (B < C \leftrightarrow A^{B} < A^{C})$

Metamath Proof Explorer

Theorem cxplt

Proof