Theorem cxpaddle

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

	Ref	Expression
Hypotheses	cxpaddle.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	cxpaddle.2	⊢ ( 𝜑 → 0 ≤ 𝐴 )
	cxpaddle.3	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	cxpaddle.4	⊢ ( 𝜑 → 0 ≤ 𝐵 )
	cxpaddle.5	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
	cxpaddle.6	⊢ ( 𝜑 → 𝐶 ≤ 1 )
Assertion	cxpaddle	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ≤ ( ( 𝐴 ↑𝑐 𝐶 ) + ( 𝐵 ↑𝑐 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cxpaddle.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		cxpaddle.2	⊢ ( 𝜑 → 0 ≤ 𝐴 )
3		cxpaddle.3	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4		cxpaddle.4	⊢ ( 𝜑 → 0 ≤ 𝐵 )
5		cxpaddle.5	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
6		cxpaddle.6	⊢ ( 𝜑 → 𝐶 ≤ 1 )
7	1 3	readdcld	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℝ )
8	1 3 2 4	addge0d	⊢ ( 𝜑 → 0 ≤ ( 𝐴 + 𝐵 ) )
9	5	rpred	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
10	7 8 9	recxpcld	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ∈ ℝ )
11	10	adantr	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ∈ ℝ )
12	11	recnd	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ∈ ℂ )
13	12	mullidd	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( 1 · ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ) = ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) )
14	1	adantr	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → 𝐴 ∈ ℝ )
15	7	anim1i	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐴 + 𝐵 ) ) )
16		elrp	⊢ ( ( 𝐴 + 𝐵 ) ∈ ℝ+ ↔ ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐴 + 𝐵 ) ) )
17	15 16	sylibr	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( 𝐴 + 𝐵 ) ∈ ℝ+ )
18	14 17	rerpdivcld	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( 𝐴 / ( 𝐴 + 𝐵 ) ) ∈ ℝ )
19	3	adantr	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → 𝐵 ∈ ℝ )
20	19 17	rerpdivcld	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( 𝐵 / ( 𝐴 + 𝐵 ) ) ∈ ℝ )
21	2	adantr	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → 0 ≤ 𝐴 )
22	7	adantr	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
23		simpr	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → 0 < ( 𝐴 + 𝐵 ) )
24		divge0	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐴 + 𝐵 ) ) ) → 0 ≤ ( 𝐴 / ( 𝐴 + 𝐵 ) ) )
25	14 21 22 23 24	syl22anc	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → 0 ≤ ( 𝐴 / ( 𝐴 + 𝐵 ) ) )
26	9	adantr	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → 𝐶 ∈ ℝ )
27	18 25 26	recxpcld	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( 𝐴 / ( 𝐴 + 𝐵 ) ) ↑𝑐 𝐶 ) ∈ ℝ )
28	4	adantr	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → 0 ≤ 𝐵 )
29		divge0	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐴 + 𝐵 ) ) ) → 0 ≤ ( 𝐵 / ( 𝐴 + 𝐵 ) ) )
30	19 28 22 23 29	syl22anc	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → 0 ≤ ( 𝐵 / ( 𝐴 + 𝐵 ) ) )
31	20 30 26	recxpcld	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( 𝐵 / ( 𝐴 + 𝐵 ) ) ↑𝑐 𝐶 ) ∈ ℝ )
32	1 3	addge01d	⊢ ( 𝜑 → ( 0 ≤ 𝐵 ↔ 𝐴 ≤ ( 𝐴 + 𝐵 ) ) )
33	4 32	mpbid	⊢ ( 𝜑 → 𝐴 ≤ ( 𝐴 + 𝐵 ) )
34	33	adantr	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → 𝐴 ≤ ( 𝐴 + 𝐵 ) )
35	22	recnd	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
36	35	mulridd	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( 𝐴 + 𝐵 ) · 1 ) = ( 𝐴 + 𝐵 ) )
37	34 36	breqtrrd	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → 𝐴 ≤ ( ( 𝐴 + 𝐵 ) · 1 ) )
38		1red	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → 1 ∈ ℝ )
39		ledivmul	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐴 + 𝐵 ) ) ) → ( ( 𝐴 / ( 𝐴 + 𝐵 ) ) ≤ 1 ↔ 𝐴 ≤ ( ( 𝐴 + 𝐵 ) · 1 ) ) )
40	14 38 22 23 39	syl112anc	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( 𝐴 / ( 𝐴 + 𝐵 ) ) ≤ 1 ↔ 𝐴 ≤ ( ( 𝐴 + 𝐵 ) · 1 ) ) )
41	37 40	mpbird	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( 𝐴 / ( 𝐴 + 𝐵 ) ) ≤ 1 )
42	5	adantr	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → 𝐶 ∈ ℝ+ )
43	6	adantr	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → 𝐶 ≤ 1 )
44	18 25 41 42 43	cxpaddlelem	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( 𝐴 / ( 𝐴 + 𝐵 ) ) ≤ ( ( 𝐴 / ( 𝐴 + 𝐵 ) ) ↑𝑐 𝐶 ) )
45	3 1	addge02d	⊢ ( 𝜑 → ( 0 ≤ 𝐴 ↔ 𝐵 ≤ ( 𝐴 + 𝐵 ) ) )
46	2 45	mpbid	⊢ ( 𝜑 → 𝐵 ≤ ( 𝐴 + 𝐵 ) )
47	46	adantr	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → 𝐵 ≤ ( 𝐴 + 𝐵 ) )
48	47 36	breqtrrd	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → 𝐵 ≤ ( ( 𝐴 + 𝐵 ) · 1 ) )
49		ledivmul	⊢ ( ( 𝐵 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐴 + 𝐵 ) ) ) → ( ( 𝐵 / ( 𝐴 + 𝐵 ) ) ≤ 1 ↔ 𝐵 ≤ ( ( 𝐴 + 𝐵 ) · 1 ) ) )
50	19 38 22 23 49	syl112anc	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( 𝐵 / ( 𝐴 + 𝐵 ) ) ≤ 1 ↔ 𝐵 ≤ ( ( 𝐴 + 𝐵 ) · 1 ) ) )
51	48 50	mpbird	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( 𝐵 / ( 𝐴 + 𝐵 ) ) ≤ 1 )
52	20 30 51 42 43	cxpaddlelem	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( 𝐵 / ( 𝐴 + 𝐵 ) ) ≤ ( ( 𝐵 / ( 𝐴 + 𝐵 ) ) ↑𝑐 𝐶 ) )
53	18 20 27 31 44 52	le2addd	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( 𝐴 / ( 𝐴 + 𝐵 ) ) + ( 𝐵 / ( 𝐴 + 𝐵 ) ) ) ≤ ( ( ( 𝐴 / ( 𝐴 + 𝐵 ) ) ↑𝑐 𝐶 ) + ( ( 𝐵 / ( 𝐴 + 𝐵 ) ) ↑𝑐 𝐶 ) ) )
54	14	recnd	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → 𝐴 ∈ ℂ )
55	19	recnd	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → 𝐵 ∈ ℂ )
56	17	rpne0d	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( 𝐴 + 𝐵 ) ≠ 0 )
57	54 55 35 56	divdird	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( 𝐴 + 𝐵 ) / ( 𝐴 + 𝐵 ) ) = ( ( 𝐴 / ( 𝐴 + 𝐵 ) ) + ( 𝐵 / ( 𝐴 + 𝐵 ) ) ) )
58	35 56	dividd	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( 𝐴 + 𝐵 ) / ( 𝐴 + 𝐵 ) ) = 1 )
59	57 58	eqtr3d	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( 𝐴 / ( 𝐴 + 𝐵 ) ) + ( 𝐵 / ( 𝐴 + 𝐵 ) ) ) = 1 )
60	9	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
61	60	adantr	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → 𝐶 ∈ ℂ )
62	14 21 17 61	divcxpd	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( 𝐴 / ( 𝐴 + 𝐵 ) ) ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) / ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ) )
63	19 28 17 61	divcxpd	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( 𝐵 / ( 𝐴 + 𝐵 ) ) ↑𝑐 𝐶 ) = ( ( 𝐵 ↑𝑐 𝐶 ) / ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ) )
64	62 63	oveq12d	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( ( 𝐴 / ( 𝐴 + 𝐵 ) ) ↑𝑐 𝐶 ) + ( ( 𝐵 / ( 𝐴 + 𝐵 ) ) ↑𝑐 𝐶 ) ) = ( ( ( 𝐴 ↑𝑐 𝐶 ) / ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ) + ( ( 𝐵 ↑𝑐 𝐶 ) / ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ) ) )
65	1 2 9	recxpcld	⊢ ( 𝜑 → ( 𝐴 ↑𝑐 𝐶 ) ∈ ℝ )
66	65	recnd	⊢ ( 𝜑 → ( 𝐴 ↑𝑐 𝐶 ) ∈ ℂ )
67	66	adantr	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( 𝐴 ↑𝑐 𝐶 ) ∈ ℂ )
68	3 4 9	recxpcld	⊢ ( 𝜑 → ( 𝐵 ↑𝑐 𝐶 ) ∈ ℝ )
69	68	recnd	⊢ ( 𝜑 → ( 𝐵 ↑𝑐 𝐶 ) ∈ ℂ )
70	69	adantr	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( 𝐵 ↑𝑐 𝐶 ) ∈ ℂ )
71	17 26	rpcxpcld	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ∈ ℝ+ )
72	71	rpne0d	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ≠ 0 )
73	67 70 12 72	divdird	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( ( 𝐴 ↑𝑐 𝐶 ) + ( 𝐵 ↑𝑐 𝐶 ) ) / ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ) = ( ( ( 𝐴 ↑𝑐 𝐶 ) / ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ) + ( ( 𝐵 ↑𝑐 𝐶 ) / ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ) ) )
74	64 73	eqtr4d	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( ( 𝐴 / ( 𝐴 + 𝐵 ) ) ↑𝑐 𝐶 ) + ( ( 𝐵 / ( 𝐴 + 𝐵 ) ) ↑𝑐 𝐶 ) ) = ( ( ( 𝐴 ↑𝑐 𝐶 ) + ( 𝐵 ↑𝑐 𝐶 ) ) / ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ) )
75	53 59 74	3brtr3d	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → 1 ≤ ( ( ( 𝐴 ↑𝑐 𝐶 ) + ( 𝐵 ↑𝑐 𝐶 ) ) / ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ) )
76	65 68	readdcld	⊢ ( 𝜑 → ( ( 𝐴 ↑𝑐 𝐶 ) + ( 𝐵 ↑𝑐 𝐶 ) ) ∈ ℝ )
77	76	adantr	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( 𝐴 ↑𝑐 𝐶 ) + ( 𝐵 ↑𝑐 𝐶 ) ) ∈ ℝ )
78	38 77 71	lemuldivd	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( 1 · ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ) ≤ ( ( 𝐴 ↑𝑐 𝐶 ) + ( 𝐵 ↑𝑐 𝐶 ) ) ↔ 1 ≤ ( ( ( 𝐴 ↑𝑐 𝐶 ) + ( 𝐵 ↑𝑐 𝐶 ) ) / ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ) ) )
79	75 78	mpbird	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( 1 · ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ) ≤ ( ( 𝐴 ↑𝑐 𝐶 ) + ( 𝐵 ↑𝑐 𝐶 ) ) )
80	13 79	eqbrtrrd	⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 + 𝐵 ) ) → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ≤ ( ( 𝐴 ↑𝑐 𝐶 ) + ( 𝐵 ↑𝑐 𝐶 ) ) )
81	5	rpne0d	⊢ ( 𝜑 → 𝐶 ≠ 0 )
82	60 81	0cxpd	⊢ ( 𝜑 → ( 0 ↑𝑐 𝐶 ) = 0 )
83	1 2 9	cxpge0d	⊢ ( 𝜑 → 0 ≤ ( 𝐴 ↑𝑐 𝐶 ) )
84	3 4 9	cxpge0d	⊢ ( 𝜑 → 0 ≤ ( 𝐵 ↑𝑐 𝐶 ) )
85	65 68 83 84	addge0d	⊢ ( 𝜑 → 0 ≤ ( ( 𝐴 ↑𝑐 𝐶 ) + ( 𝐵 ↑𝑐 𝐶 ) ) )
86	82 85	eqbrtrd	⊢ ( 𝜑 → ( 0 ↑𝑐 𝐶 ) ≤ ( ( 𝐴 ↑𝑐 𝐶 ) + ( 𝐵 ↑𝑐 𝐶 ) ) )
87		oveq1	⊢ ( 0 = ( 𝐴 + 𝐵 ) → ( 0 ↑𝑐 𝐶 ) = ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) )
88	87	breq1d	⊢ ( 0 = ( 𝐴 + 𝐵 ) → ( ( 0 ↑𝑐 𝐶 ) ≤ ( ( 𝐴 ↑𝑐 𝐶 ) + ( 𝐵 ↑𝑐 𝐶 ) ) ↔ ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ≤ ( ( 𝐴 ↑𝑐 𝐶 ) + ( 𝐵 ↑𝑐 𝐶 ) ) ) )
89	86 88	syl5ibcom	⊢ ( 𝜑 → ( 0 = ( 𝐴 + 𝐵 ) → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ≤ ( ( 𝐴 ↑𝑐 𝐶 ) + ( 𝐵 ↑𝑐 𝐶 ) ) ) )
90	89	imp	⊢ ( ( 𝜑 ∧ 0 = ( 𝐴 + 𝐵 ) ) → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ≤ ( ( 𝐴 ↑𝑐 𝐶 ) + ( 𝐵 ↑𝑐 𝐶 ) ) )
91		0re	⊢ 0 ∈ ℝ
92		leloe	⊢ ( ( 0 ∈ ℝ ∧ ( 𝐴 + 𝐵 ) ∈ ℝ ) → ( 0 ≤ ( 𝐴 + 𝐵 ) ↔ ( 0 < ( 𝐴 + 𝐵 ) ∨ 0 = ( 𝐴 + 𝐵 ) ) ) )
93	91 7 92	sylancr	⊢ ( 𝜑 → ( 0 ≤ ( 𝐴 + 𝐵 ) ↔ ( 0 < ( 𝐴 + 𝐵 ) ∨ 0 = ( 𝐴 + 𝐵 ) ) ) )
94	8 93	mpbid	⊢ ( 𝜑 → ( 0 < ( 𝐴 + 𝐵 ) ∨ 0 = ( 𝐴 + 𝐵 ) ) )
95	80 90 94	mpjaodan	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ≤ ( ( 𝐴 ↑𝑐 𝐶 ) + ( 𝐵 ↑𝑐 𝐶 ) ) )