Theorem cxpge0

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

	Ref	Expression
Assertion	cxpge0	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) → 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		0re	⊢ 0 ∈ ℝ
2		leloe	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 ≤ 𝐴 ↔ ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) )
3	1 2	mpan	⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 ↔ ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) )
4	3	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 ≤ 𝐴 ↔ ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) )
5		elrp	⊢ ( 𝐴 ∈ ℝ+ ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
6		rpcxpcl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℝ+ )
7	6	rpge0d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) )
8	7	ex	⊢ ( 𝐴 ∈ ℝ+ → ( 𝐵 ∈ ℝ → 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) ) )
9	5 8	sylbir	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 𝐵 ∈ ℝ → 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) ) )
10	9	impancom	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 < 𝐴 → 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) ) )
11		0le1	⊢ 0 ≤ 1
12		0cn	⊢ 0 ∈ ℂ
13		cxp0	⊢ ( 0 ∈ ℂ → ( 0 ↑𝑐 0 ) = 1 )
14	12 13	ax-mp	⊢ ( 0 ↑𝑐 0 ) = 1
15	11 14	breqtrri	⊢ 0 ≤ ( 0 ↑𝑐 0 )
16		simpr	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 = 0 ) → 𝐵 = 0 )
17	16	oveq2d	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 = 0 ) → ( 0 ↑𝑐 𝐵 ) = ( 0 ↑𝑐 0 ) )
18	15 17	breqtrrid	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 = 0 ) → 0 ≤ ( 0 ↑𝑐 𝐵 ) )
19		0le0	⊢ 0 ≤ 0
20		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
21		0cxp	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 0 ↑𝑐 𝐵 ) = 0 )
22	20 21	sylan	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 0 ↑𝑐 𝐵 ) = 0 )
23	19 22	breqtrrid	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → 0 ≤ ( 0 ↑𝑐 𝐵 ) )
24	18 23	pm2.61dane	⊢ ( 𝐵 ∈ ℝ → 0 ≤ ( 0 ↑𝑐 𝐵 ) )
25	24	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 0 ≤ ( 0 ↑𝑐 𝐵 ) )
26		oveq1	⊢ ( 0 = 𝐴 → ( 0 ↑𝑐 𝐵 ) = ( 𝐴 ↑𝑐 𝐵 ) )
27	26	breq2d	⊢ ( 0 = 𝐴 → ( 0 ≤ ( 0 ↑𝑐 𝐵 ) ↔ 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) ) )
28	25 27	syl5ibcom	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 = 𝐴 → 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) ) )
29	10 28	jaod	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 < 𝐴 ∨ 0 = 𝐴 ) → 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) ) )
30	4 29	sylbid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 ≤ 𝐴 → 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) ) )
31	30	3impia	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) )
32	31	3com23	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) → 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) )