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 ${⊢}\left({A}\in ℝ\wedge 0\le {A}\wedge {B}\in ℝ\right)\to 0\le {{A}}^{{B}}$

Proof

Step Hyp Ref Expression
1 0re ${⊢}0\in ℝ$
2 leloe ${⊢}\left(0\in ℝ\wedge {A}\in ℝ\right)\to \left(0\le {A}↔\left(0<{A}\vee 0={A}\right)\right)$
3 1 2 mpan ${⊢}{A}\in ℝ\to \left(0\le {A}↔\left(0<{A}\vee 0={A}\right)\right)$
4 3 adantr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(0\le {A}↔\left(0<{A}\vee 0={A}\right)\right)$
5 elrp ${⊢}{A}\in {ℝ}^{+}↔\left({A}\in ℝ\wedge 0<{A}\right)$
6 rpcxpcl ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\right)\to {{A}}^{{B}}\in {ℝ}^{+}$
7 6 rpge0d ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\right)\to 0\le {{A}}^{{B}}$
8 7 ex ${⊢}{A}\in {ℝ}^{+}\to \left({B}\in ℝ\to 0\le {{A}}^{{B}}\right)$
9 5 8 sylbir ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \left({B}\in ℝ\to 0\le {{A}}^{{B}}\right)$
10 9 impancom ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(0<{A}\to 0\le {{A}}^{{B}}\right)$
11 0le1 ${⊢}0\le 1$
12 0cn ${⊢}0\in ℂ$
13 cxp0 ${⊢}0\in ℂ\to {0}^{0}=1$
14 12 13 ax-mp ${⊢}{0}^{0}=1$
15 11 14 breqtrri ${⊢}0\le {0}^{0}$
16 simpr ${⊢}\left({B}\in ℝ\wedge {B}=0\right)\to {B}=0$
17 16 oveq2d ${⊢}\left({B}\in ℝ\wedge {B}=0\right)\to {0}^{{B}}={0}^{0}$
18 15 17 breqtrrid ${⊢}\left({B}\in ℝ\wedge {B}=0\right)\to 0\le {0}^{{B}}$
19 0le0 ${⊢}0\le 0$
20 recn ${⊢}{B}\in ℝ\to {B}\in ℂ$
21 0cxp ${⊢}\left({B}\in ℂ\wedge {B}\ne 0\right)\to {0}^{{B}}=0$
22 20 21 sylan ${⊢}\left({B}\in ℝ\wedge {B}\ne 0\right)\to {0}^{{B}}=0$
23 19 22 breqtrrid ${⊢}\left({B}\in ℝ\wedge {B}\ne 0\right)\to 0\le {0}^{{B}}$
24 18 23 pm2.61dane ${⊢}{B}\in ℝ\to 0\le {0}^{{B}}$
25 24 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to 0\le {0}^{{B}}$
26 oveq1 ${⊢}0={A}\to {0}^{{B}}={{A}}^{{B}}$
27 26 breq2d ${⊢}0={A}\to \left(0\le {0}^{{B}}↔0\le {{A}}^{{B}}\right)$
28 25 27 syl5ibcom ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(0={A}\to 0\le {{A}}^{{B}}\right)$
29 10 28 jaod ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left(0<{A}\vee 0={A}\right)\to 0\le {{A}}^{{B}}\right)$
30 4 29 sylbid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(0\le {A}\to 0\le {{A}}^{{B}}\right)$
31 30 3impia ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge 0\le {A}\right)\to 0\le {{A}}^{{B}}$
32 31 3com23 ${⊢}\left({A}\in ℝ\wedge 0\le {A}\wedge {B}\in ℝ\right)\to 0\le {{A}}^{{B}}$