Theorem cxpgt0d

Description: A positive real raised to a real power is positive. (Contributed by SN, 6-Apr-2023)

	Ref	Expression
Hypotheses	cxpgt0d.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
	cxpgt0d.2	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
Assertion	cxpgt0d	⊢ ( 𝜑 → 0 < ( 𝐴 ↑𝑐 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		cxpgt0d.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2		cxpgt0d.2	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
3	1	relogcld	⊢ ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℝ )
4	2 3	remulcld	⊢ ( 𝜑 → ( 𝑁 · ( log ‘ 𝐴 ) ) ∈ ℝ )
5		efgt0	⊢ ( ( 𝑁 · ( log ‘ 𝐴 ) ) ∈ ℝ → 0 < ( exp ‘ ( 𝑁 · ( log ‘ 𝐴 ) ) ) )
6	4 5	syl	⊢ ( 𝜑 → 0 < ( exp ‘ ( 𝑁 · ( log ‘ 𝐴 ) ) ) )
7	1	rpcnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
8	1	rpne0d	⊢ ( 𝜑 → 𝐴 ≠ 0 )
9	2	recnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
10	7 8 9	cxpefd	⊢ ( 𝜑 → ( 𝐴 ↑𝑐 𝑁 ) = ( exp ‘ ( 𝑁 · ( log ‘ 𝐴 ) ) ) )
11	6 10	breqtrrd	⊢ ( 𝜑 → 0 < ( 𝐴 ↑𝑐 𝑁 ) )