Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ≤ ( ( 𝐴 ↑𝑐 𝐶 ) + ( 𝐵 ↑𝑐 𝐶 ) ) )