Theorem cxpaddlelem

Description: Lemma for cxpaddle . (Contributed by Mario Carneiro, 2-Aug-2014)

	Ref	Expression
Hypotheses	cxpaddlelem.1	$$⊢\phi \to A\in ℝ$$
	cxpaddlelem.2	$$⊢\phi \to 0\le A$$
	cxpaddlelem.3	$$⊢\phi \to A\le 1$$
	cxpaddlelem.4	$$⊢\phi \to B\in {ℝ}^{+}$$
	cxpaddlelem.5	$$⊢\phi \to B\le 1$$
Assertion	cxpaddlelem	$$⊢\phi \to A\le A^B$$

Proof

Step	Hyp	Ref	Expression
1		cxpaddlelem.1	$$⊢\phi \to A\in ℝ$$
2		cxpaddlelem.2	$$⊢\phi \to 0\le A$$
3		cxpaddlelem.3	$$⊢\phi \to A\le 1$$
4		cxpaddlelem.4	$$⊢\phi \to B\in {ℝ}^{+}$$
5		cxpaddlelem.5	$$⊢\phi \to B\le 1$$
6		1re	$$⊢1\in ℝ$$
7	4	rpred	$$⊢\phi \to B\in ℝ$$
8		resubcl	$$⊢\left(1\in ℝ\wedge B\in ℝ\right)\to 1-B\in ℝ$$
9	6 7 8	sylancr	$$⊢\phi \to 1-B\in ℝ$$
10	1 2 9	recxpcld	$$⊢\phi \to A^{1-B}\in ℝ$$
11	10	adantr	$$⊢\left(\phi \wedge 0<A\right)\to A^{1-B}\in ℝ$$
12		1red	$$⊢\left(\phi \wedge 0<A\right)\to 1\in ℝ$$
13		recxpcl	$$⊢\left(A\in ℝ\wedge 0\le A\wedge B\in ℝ\right)\to A^B\in ℝ$$
14		cxpge0	$$⊢\left(A\in ℝ\wedge 0\le A\wedge B\in ℝ\right)\to 0\le A^B$$
15	13 14	jca	$$⊢\left(A\in ℝ\wedge 0\le A\wedge B\in ℝ\right)\to \left(A^B\in ℝ\wedge 0\le A^B\right)$$
16	1 2 7 15	syl3anc	$$⊢\phi \to \left(A^B\in ℝ\wedge 0\le A^B\right)$$
17	16	adantr	$$⊢\left(\phi \wedge 0<A\right)\to \left(A^B\in ℝ\wedge 0\le A^B\right)$$
18	3	ad2antrr	$$⊢\left(\left(\phi \wedge 0<A\right)\wedge B<1\right)\to A\le 1$$
19	1	ad2antrr	$$⊢\left(\left(\phi \wedge 0<A\right)\wedge B<1\right)\to A\in ℝ$$
20	2	ad2antrr	$$⊢\left(\left(\phi \wedge 0<A\right)\wedge B<1\right)\to 0\le A$$
21		1red	$$⊢\left(\left(\phi \wedge 0<A\right)\wedge B<1\right)\to 1\in ℝ$$
22		0le1	$$⊢0\le 1$$
23	22	a1i	$$⊢\left(\left(\phi \wedge 0<A\right)\wedge B<1\right)\to 0\le 1$$
24		difrp	$$⊢\left(B\in ℝ\wedge 1\in ℝ\right)\to \left(B<1\leftrightarrow 1-B\in {ℝ}^{+}\right)$$
25	7 6 24	sylancl	$$⊢\phi \to \left(B<1\leftrightarrow 1-B\in {ℝ}^{+}\right)$$
26	25	adantr	$$⊢\left(\phi \wedge 0<A\right)\to \left(B<1\leftrightarrow 1-B\in {ℝ}^{+}\right)$$
27	26	biimpa	$$⊢\left(\left(\phi \wedge 0<A\right)\wedge B<1\right)\to 1-B\in {ℝ}^{+}$$
28	19 20 21 23 27	cxple2d	$$⊢\left(\left(\phi \wedge 0<A\right)\wedge B<1\right)\to \left(A\le 1\leftrightarrow A^{1-B}\le 1^{1-B}\right)$$
29	18 28	mpbid	$$⊢\left(\left(\phi \wedge 0<A\right)\wedge B<1\right)\to A^{1-B}\le 1^{1-B}$$
30	9	recnd	$$⊢\phi \to 1-B\in ℂ$$
31	30	1cxpd	$$⊢\phi \to 1^{1-B}=1$$
32	31	ad2antrr	$$⊢\left(\left(\phi \wedge 0<A\right)\wedge B<1\right)\to 1^{1-B}=1$$
33	29 32	breqtrd	$$⊢\left(\left(\phi \wedge 0<A\right)\wedge B<1\right)\to A^{1-B}\le 1$$
34		simpr	$$⊢\left(\left(\phi \wedge 0<A\right)\wedge B=1\right)\to B=1$$
35	34	oveq2d	$$⊢\left(\left(\phi \wedge 0<A\right)\wedge B=1\right)\to 1-B=1-1$$
36		1m1e0	$$⊢1-1=0$$
37	35 36	eqtrdi	$$⊢\left(\left(\phi \wedge 0<A\right)\wedge B=1\right)\to 1-B=0$$
38	37	oveq2d	$$⊢\left(\left(\phi \wedge 0<A\right)\wedge B=1\right)\to A^{1-B}=A^0$$
39	1	recnd	$$⊢\phi \to A\in ℂ$$
40	39	ad2antrr	$$⊢\left(\left(\phi \wedge 0<A\right)\wedge B=1\right)\to A\in ℂ$$
41	40	cxp0d	$$⊢\left(\left(\phi \wedge 0<A\right)\wedge B=1\right)\to A^0=1$$
42	38 41	eqtrd	$$⊢\left(\left(\phi \wedge 0<A\right)\wedge B=1\right)\to A^{1-B}=1$$
43		1le1	$$⊢1\le 1$$
44	42 43	eqbrtrdi	$$⊢\left(\left(\phi \wedge 0<A\right)\wedge B=1\right)\to A^{1-B}\le 1$$
45		leloe	$$⊢\left(B\in ℝ\wedge 1\in ℝ\right)\to \left(B\le 1\leftrightarrow \left(B<1\vee B=1\right)\right)$$
46	7 6 45	sylancl	$$⊢\phi \to \left(B\le 1\leftrightarrow \left(B<1\vee B=1\right)\right)$$
47	5 46	mpbid	$$⊢\phi \to \left(B<1\vee B=1\right)$$
48	47	adantr	$$⊢\left(\phi \wedge 0<A\right)\to \left(B<1\vee B=1\right)$$
49	33 44 48	mpjaodan	$$⊢\left(\phi \wedge 0<A\right)\to A^{1-B}\le 1$$
50		lemul1a	$$⊢\left(\left(A^{1-B}\in ℝ\wedge 1\in ℝ\wedge \left(A^B\in ℝ\wedge 0\le A^B\right)\right)\wedge A^{1-B}\le 1\right)\to A^{1-B}{A}^B\le 1A^B$$
51	11 12 17 49 50	syl31anc	$$⊢\left(\phi \wedge 0<A\right)\to A^{1-B}{A}^B\le 1A^B$$
52		ax-1cn	$$⊢1\in ℂ$$
53	7	recnd	$$⊢\phi \to B\in ℂ$$
54		npcan	$$⊢\left(1\in ℂ\wedge B\in ℂ\right)\to 1-B+B=1$$
55	52 53 54	sylancr	$$⊢\phi \to 1-B+B=1$$
56	55	adantr	$$⊢\left(\phi \wedge 0<A\right)\to 1-B+B=1$$
57	56	oveq2d	$$⊢\left(\phi \wedge 0<A\right)\to A^{1-B+B}=A^1$$
58	39	adantr	$$⊢\left(\phi \wedge 0<A\right)\to A\in ℂ$$
59	1	anim1i	$$⊢\left(\phi \wedge 0<A\right)\to \left(A\in ℝ\wedge 0<A\right)$$
60		elrp	$$⊢A\in {ℝ}^{+}\leftrightarrow \left(A\in ℝ\wedge 0<A\right)$$
61	59 60	sylibr	$$⊢\left(\phi \wedge 0<A\right)\to A\in {ℝ}^{+}$$
62	61	rpne0d	$$⊢\left(\phi \wedge 0<A\right)\to A\ne 0$$
63	30	adantr	$$⊢\left(\phi \wedge 0<A\right)\to 1-B\in ℂ$$
64	53	adantr	$$⊢\left(\phi \wedge 0<A\right)\to B\in ℂ$$
65	58 62 63 64	cxpaddd	$$⊢\left(\phi \wedge 0<A\right)\to A^{1-B+B}=A^{1-B}{A}^B$$
66	39	cxp1d	$$⊢\phi \to A^1=A$$
67	66	adantr	$$⊢\left(\phi \wedge 0<A\right)\to A^1=A$$
68	57 65 67	3eqtr3d	$$⊢\left(\phi \wedge 0<A\right)\to A^{1-B}{A}^B=A$$
69	39 53	cxpcld	$$⊢\phi \to A^B\in ℂ$$
70	69	mullidd	$$⊢\phi \to 1A^B=A^B$$
71	70	adantr	$$⊢\left(\phi \wedge 0<A\right)\to 1A^B=A^B$$
72	51 68 71	3brtr3d	$$⊢\left(\phi \wedge 0<A\right)\to A\le A^B$$
73	1 2 7	cxpge0d	$$⊢\phi \to 0\le A^B$$
74		breq1	$$⊢0=A\to \left(0\le A^B\leftrightarrow A\le A^B\right)$$
75	73 74	syl5ibcom	$$⊢\phi \to \left(0=A\to A\le A^B\right)$$
76	75	imp	$$⊢\left(\phi \wedge 0=A\right)\to A\le A^B$$
77		0re	$$⊢0\in ℝ$$
78		leloe	$$⊢\left(0\in ℝ\wedge A\in ℝ\right)\to \left(0\le A\leftrightarrow \left(0<A\vee 0=A\right)\right)$$
79	77 1 78	sylancr	$$⊢\phi \to \left(0\le A\leftrightarrow \left(0<A\vee 0=A\right)\right)$$
80	2 79	mpbid	$$⊢\phi \to \left(0<A\vee 0=A\right)$$
81	72 76 80	mpjaodan	$$⊢\phi \to A\le A^B$$