Metamath Proof Explorer


Theorem cxpge0d

Description: Nonnegative exponentiation with a real exponent is nonnegative. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Hypotheses recxpcld.1 φA
recxpcld.2 φ0A
recxpcld.3 φB
Assertion cxpge0d φ0AB

Proof

Step Hyp Ref Expression
1 recxpcld.1 φA
2 recxpcld.2 φ0A
3 recxpcld.3 φB
4 cxpge0 A0AB0AB
5 1 2 3 4 syl3anc φ0AB