HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-e 7299
Description: Define Euler's constant 2.71828....
Assertion
Ref Expression
df-e |- e = (exp` 1)

Detailed syntax breakdown of Definition df-e
StepHypRef Expression
1 ceu 7294 . 2 class e
2 c1 5235 . . 3 class 1
3 ce 7293 . . 3 class exp
42, 3cfv 3182 . 2 class (exp`
1)
51, 4wceq 956 1 wff e = (exp` 1)
Colors of variables: wff set class
This definition is referenced by:  eval 7309  ere 7330  efnn0valt 7373  eirrlem5 7393  loge 8767
Copyright terms: Public domain