Metamath Proof Explorer

Theorem cxpge0

Description: Nonnegative exponentiation with a real exponent is nonnegative. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion cxpge0 
|- ( ( A e. RR /\ 0 <_ A /\ B e. RR ) -> 0 <_ ( A ^c B ) )

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 leloe 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) )
3 1 2 mpan 
 |-  ( A e. RR -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) )
4 3 adantr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) )
5 elrp 
 |-  ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
6 rpcxpcl 
 |-  ( ( A e. RR+ /\ B e. RR ) -> ( A ^c B ) e. RR+ )
7 6 rpge0d 
 |-  ( ( A e. RR+ /\ B e. RR ) -> 0 <_ ( A ^c B ) )
8 7 ex 
 |-  ( A e. RR+ -> ( B e. RR -> 0 <_ ( A ^c B ) ) )
9 5 8 sylbir 
 |-  ( ( A e. RR /\ 0 < A ) -> ( B e. RR -> 0 <_ ( A ^c B ) ) )
10 9 impancom 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 < A -> 0 <_ ( A ^c B ) ) )
11 0le1 
 |-  0 <_ 1
12 0cn 
 |-  0 e. CC
13 cxp0 
 |-  ( 0 e. CC -> ( 0 ^c 0 ) = 1 )
14 12 13 ax-mp 
 |-  ( 0 ^c 0 ) = 1
15 11 14 breqtrri 
 |-  0 <_ ( 0 ^c 0 )
16 simpr 
 |-  ( ( B e. RR /\ B = 0 ) -> B = 0 )
17 16 oveq2d 
 |-  ( ( B e. RR /\ B = 0 ) -> ( 0 ^c B ) = ( 0 ^c 0 ) )
18 15 17 breqtrrid 
 |-  ( ( B e. RR /\ B = 0 ) -> 0 <_ ( 0 ^c B ) )
19 0le0 
 |-  0 <_ 0
20 recn 
 |-  ( B e. RR -> B e. CC )
21 0cxp 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( 0 ^c B ) = 0 )
22 20 21 sylan 
 |-  ( ( B e. RR /\ B =/= 0 ) -> ( 0 ^c B ) = 0 )
23 19 22 breqtrrid 
 |-  ( ( B e. RR /\ B =/= 0 ) -> 0 <_ ( 0 ^c B ) )
24 18 23 pm2.61dane 
 |-  ( B e. RR -> 0 <_ ( 0 ^c B ) )
25 24 adantl 
 |-  ( ( A e. RR /\ B e. RR ) -> 0 <_ ( 0 ^c B ) )
26 oveq1 
 |-  ( 0 = A -> ( 0 ^c B ) = ( A ^c B ) )
27 26 breq2d 
 |-  ( 0 = A -> ( 0 <_ ( 0 ^c B ) <-> 0 <_ ( A ^c B ) ) )
28 25 27 syl5ibcom 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 = A -> 0 <_ ( A ^c B ) ) )
29 10 28 jaod 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 < A \/ 0 = A ) -> 0 <_ ( A ^c B ) ) )
30 4 29 sylbid 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 <_ A -> 0 <_ ( A ^c B ) ) )
31 30 3impia 
 |-  ( ( A e. RR /\ B e. RR /\ 0 <_ A ) -> 0 <_ ( A ^c B ) )
32 31 3com23 
 |-  ( ( A e. RR /\ 0 <_ A /\ B e. RR ) -> 0 <_ ( A ^c B ) )