Description: Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | recxpcld.1 | |- ( ph -> A e. RR ) |
|
| recxpcld.2 | |- ( ph -> 0 <_ A ) |
||
| recxpcld.3 | |- ( ph -> B e. RR ) |
||
| cxple2ad.4 | |- ( ph -> C e. RR ) |
||
| cxple2ad.5 | |- ( ph -> 0 <_ C ) |
||
| cxple2ad.6 | |- ( ph -> A <_ B ) |
||
| Assertion | cxple2ad | |- ( ph -> ( A ^c C ) <_ ( B ^c C ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | recxpcld.1 | |- ( ph -> A e. RR ) |
|
| 2 | recxpcld.2 | |- ( ph -> 0 <_ A ) |
|
| 3 | recxpcld.3 | |- ( ph -> B e. RR ) |
|
| 4 | cxple2ad.4 | |- ( ph -> C e. RR ) |
|
| 5 | cxple2ad.5 | |- ( ph -> 0 <_ C ) |
|
| 6 | cxple2ad.6 | |- ( ph -> A <_ B ) |
|
| 7 | cxple2a | |- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) -> ( A ^c C ) <_ ( B ^c C ) ) |
|
| 8 | 1 3 4 2 5 6 7 | syl321anc | |- ( ph -> ( A ^c C ) <_ ( B ^c C ) ) |