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 ) ) )