cxple2

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

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

Proof

Step	Hyp	Ref	Expression
1		simpl1l	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \to A \in ℝ$
2		simpr	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \to 0 < A$
3	1 2	elrpd	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \to A \in ℝ^{+}$
4	3	adantr	$⊢ ((((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \land 0 < B) \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	5	ad2antrr	$⊢ ((((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \land 0 < B) \to B \in ℝ$
7		simpr	$⊢ ((((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \land 0 < B) \to 0 < B$
8	6 7	elrpd	$⊢ ((((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \land 0 < B) \to B \in ℝ^{+}$
9		simp3	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to C \in ℝ^{+}$
10	9	ad2antrr	$⊢ ((((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \land 0 < B) \to C \in ℝ^{+}$
11		simp3	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to C \in ℝ^{+}$
12	11	rpred	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to C \in ℝ$
13		relogcl	$⊢ A \in ℝ^{+} \to \log A \in ℝ$
14	13	3ad2ant1	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to \log A \in ℝ$
15	12 14	remulcld	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to C \log A \in ℝ$
16		relogcl	$⊢ B \in ℝ^{+} \to \log B \in ℝ$
17	16	3ad2ant2	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to \log B \in ℝ$
18	12 17	remulcld	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to C \log B \in ℝ$
19		efle	$⊢ (C \log A \in ℝ \land C \log B \in ℝ) \to (C \log A \leq C \log B \leftrightarrow e^{C \log A} \leq e^{C \log B})$
20	15 18 19	syl2anc	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to (C \log A \leq C \log B \leftrightarrow e^{C \log A} \leq e^{C \log B})$
21		efle	$⊢ (\log A \in ℝ \land \log B \in ℝ) \to (\log A \leq \log B \leftrightarrow e^{\log A} \leq e^{\log B})$
22	14 17 21	syl2anc	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to (\log A \leq \log B \leftrightarrow e^{\log A} \leq e^{\log B})$
23	14 17 11	lemul2d	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to (\log A \leq \log B \leftrightarrow C \log A \leq C \log B)$
24		reeflog	$⊢ A \in ℝ^{+} \to e^{\log A} = A$
25	24	3ad2ant1	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to e^{\log A} = A$
26		reeflog	$⊢ B \in ℝ^{+} \to e^{\log B} = B$
27	26	3ad2ant2	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to e^{\log B} = B$
28	25 27	breq12d	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to (e^{\log A} \leq e^{\log B} \leftrightarrow A \leq B)$
29	22 23 28	3bitr3rd	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to (A \leq B \leftrightarrow C \log A \leq C \log B)$
30		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
31	30	3ad2ant1	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to A \in ℝ$
32	31	recnd	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to A \in ℂ$
33		rpne0	$⊢ A \in ℝ^{+} \to A \neq 0$
34	33	3ad2ant1	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to A \neq 0$
35	12	recnd	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to C \in ℂ$
36		cxpef	$⊢ (A \in ℂ \land A \neq 0 \land C \in ℂ) \to A^{C} = e^{C \log A}$
37	32 34 35 36	syl3anc	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to A^{C} = e^{C \log A}$
38		rpre	$⊢ B \in ℝ^{+} \to B \in ℝ$
39	38	3ad2ant2	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to B \in ℝ$
40	39	recnd	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to B \in ℂ$
41		rpne0	$⊢ B \in ℝ^{+} \to B \neq 0$
42	41	3ad2ant2	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to B \neq 0$
43		cxpef	$⊢ (B \in ℂ \land B \neq 0 \land C \in ℂ) \to B^{C} = e^{C \log B}$
44	40 42 35 43	syl3anc	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to B^{C} = e^{C \log B}$
45	37 44	breq12d	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to (A^{C} \leq B^{C} \leftrightarrow e^{C \log A} \leq e^{C \log B})$
46	20 29 45	3bitr4d	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ^{+}) \to (A \leq B \leftrightarrow A^{C} \leq B^{C})$
47	4 8 10 46	syl3anc	$⊢ ((((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \land 0 < B) \to (A \leq B \leftrightarrow A^{C} \leq B^{C})$
48		0re	$⊢ 0 \in ℝ$
49		simp1l	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to A \in ℝ$
50		ltnle	$⊢ (0 \in ℝ \land A \in ℝ) \to (0 < A \leftrightarrow \neg A \leq 0)$
51	48 49 50	sylancr	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to (0 < A \leftrightarrow \neg A \leq 0)$
52	51	biimpa	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \to \neg A \leq 0$
53	9	rpred	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to C \in ℝ$
54	53	adantr	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \to C \in ℝ$
55		rpcxpcl	$⊢ (A \in ℝ^{+} \land C \in ℝ) \to A^{C} \in ℝ^{+}$
56	3 54 55	syl2anc	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \to A^{C} \in ℝ^{+}$
57		rpgt0	$⊢ A^{C} \in ℝ^{+} \to 0 < A^{C}$
58		rpre	$⊢ A^{C} \in ℝ^{+} \to A^{C} \in ℝ$
59		ltnle	$⊢ (0 \in ℝ \land A^{C} \in ℝ) \to (0 < A^{C} \leftrightarrow \neg A^{C} \leq 0)$
60	48 58 59	sylancr	$⊢ A^{C} \in ℝ^{+} \to (0 < A^{C} \leftrightarrow \neg A^{C} \leq 0)$
61	57 60	mpbid	$⊢ A^{C} \in ℝ^{+} \to \neg A^{C} \leq 0$
62	56 61	syl	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \to \neg A^{C} \leq 0$
63	53	recnd	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to C \in ℂ$
64	9	rpne0d	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to C \neq 0$
65		0cxp	$⊢ (C \in ℂ \land C \neq 0) \to 0^{C} = 0$
66	63 64 65	syl2anc	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to 0^{C} = 0$
67	66	adantr	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \to 0^{C} = 0$
68	67	breq2d	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \to (A^{C} \leq 0^{C} \leftrightarrow A^{C} \leq 0)$
69	62 68	mtbird	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \to \neg A^{C} \leq 0^{C}$
70	52 69	2falsed	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \to (A \leq 0 \leftrightarrow A^{C} \leq 0^{C})$
71		breq2	$⊢ 0 = B \to (A \leq 0 \leftrightarrow A \leq B)$
72		oveq1	$⊢ 0 = B \to 0^{C} = B^{C}$
73	72	breq2d	$⊢ 0 = B \to (A^{C} \leq 0^{C} \leftrightarrow A^{C} \leq B^{C})$
74	71 73	bibi12d	$⊢ 0 = B \to ((A \leq 0 \leftrightarrow A^{C} \leq 0^{C}) \leftrightarrow (A \leq B \leftrightarrow A^{C} \leq B^{C}))$
75	70 74	syl5ibcom	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \to (0 = B \to (A \leq B \leftrightarrow A^{C} \leq B^{C}))$
76	75	imp	$⊢ ((((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \land 0 = B) \to (A \leq B \leftrightarrow A^{C} \leq B^{C})$
77		simp2r	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to 0 \leq B$
78		leloe	$⊢ (0 \in ℝ \land B \in ℝ) \to (0 \leq B \leftrightarrow (0 < B \lor 0 = B))$
79	48 5 78	sylancr	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to (0 \leq B \leftrightarrow (0 < B \lor 0 = B))$
80	77 79	mpbid	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to (0 < B \lor 0 = B)$
81	80	adantr	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \to (0 < B \lor 0 = B)$
82	47 76 81	mpjaodan	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 < A) \to (A \leq B \leftrightarrow A^{C} \leq B^{C})$
83		simpr	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 = A) \to 0 = A$
84		simpl2r	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 = A) \to 0 \leq B$
85	83 84	eqbrtrrd	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 = A) \to A \leq B$
86	66	adantr	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 = A) \to 0^{C} = 0$
87	83	oveq1d	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 = A) \to 0^{C} = A^{C}$
88	86 87	eqtr3d	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 = A) \to 0 = A^{C}$
89		simpl2l	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 = A) \to B \in ℝ$
90	53	adantr	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 = A) \to C \in ℝ$
91		cxpge0	$⊢ (B \in ℝ \land 0 \leq B \land C \in ℝ) \to 0 \leq B^{C}$
92	89 84 90 91	syl3anc	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 = A) \to 0 \leq B^{C}$
93	88 92	eqbrtrrd	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 = A) \to A^{C} \leq B^{C}$
94	85 93	2thd	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \land 0 = A) \to (A \leq B \leftrightarrow A^{C} \leq B^{C})$
95		simp1r	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to 0 \leq A$
96		leloe	$⊢ (0 \in ℝ \land A \in ℝ) \to (0 \leq A \leftrightarrow (0 < A \lor 0 = A))$
97	48 49 96	sylancr	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to (0 \leq A \leftrightarrow (0 < A \lor 0 = A))$
98	95 97	mpbid	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to (0 < A \lor 0 = A)$
99	82 94 98	mpjaodan	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℝ^{+}) \to (A \leq B \leftrightarrow A^{C} \leq B^{C})$

Metamath Proof Explorer

Theorem cxple2

Proof