Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Exponents and divisibility
cxpgt0d
Next ⟩
zrtelqelz
Metamath Proof Explorer
Ascii
Unicode
Theorem
cxpgt0d
Description:
A positive real raised to a real power is positive.
(Contributed by
SN
, 6-Apr-2023)
Ref
Expression
Hypotheses
cxpgt0d.1
⊢
φ
→
A
∈
ℝ
+
cxpgt0d.2
⊢
φ
→
N
∈
ℝ
Assertion
cxpgt0d
⊢
φ
→
0
<
A
N
Proof
Step
Hyp
Ref
Expression
1
cxpgt0d.1
⊢
φ
→
A
∈
ℝ
+
2
cxpgt0d.2
⊢
φ
→
N
∈
ℝ
3
1
relogcld
⊢
φ
→
log
⁡
A
∈
ℝ
4
2
3
remulcld
⊢
φ
→
N
⁢
log
⁡
A
∈
ℝ
5
efgt0
⊢
N
⁢
log
⁡
A
∈
ℝ
→
0
<
e
N
⁢
log
⁡
A
6
4
5
syl
⊢
φ
→
0
<
e
N
⁢
log
⁡
A
7
1
rpcnd
⊢
φ
→
A
∈
ℂ
8
1
rpne0d
⊢
φ
→
A
≠
0
9
2
recnd
⊢
φ
→
N
∈
ℂ
10
7
8
9
cxpefd
⊢
φ
→
A
N
=
e
N
⁢
log
⁡
A
11
6
10
breqtrrd
⊢
φ
→
0
<
A
N