Database
REAL AND COMPLEX NUMBERS
Elementary trigonometry
The exponential, sine, and cosine functions
df-e
Next ⟩
df-sin
Metamath Proof Explorer
Ascii
Structured
Definition
df-e
Description:
Define Euler's constant
_e
= 2.71828....
(Contributed by
NM
, 14-Mar-2005)
Ref
Expression
Assertion
df-e
⊢
e = ( exp ‘ 1 )
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
ceu
⊢
e
1
ce
⊢
exp
2
c1
⊢
1
3
2
1
cfv
⊢
( exp ‘ 1 )
4
0
3
wceq
⊢
e = ( exp ‘ 1 )