Metamath Proof Explorer

Theorem cxpaddle

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

Ref Expression
Hypotheses cxpaddle.1 
|- ( ph -> A e. RR )
cxpaddle.2 
|- ( ph -> 0 <_ A )
cxpaddle.3 
|- ( ph -> B e. RR )
cxpaddle.4 
|- ( ph -> 0 <_ B )
cxpaddle.5 
|- ( ph -> C e. RR+ )
cxpaddle.6 
|- ( ph -> C <_ 1 )
Assertion cxpaddle 
|- ( ph -> ( ( A + B ) ^c C ) <_ ( ( A ^c C ) + ( B ^c C ) ) )

Proof

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