| Intuitionistic Logic Explorer | 
      
      
      < Previous  
      Next >
      
       Nearby theorems  | 
  ||
| Mirrors > Home > ILE Home > Th. List > df-e | Unicode version | ||
| Description: Define Euler's constant
 | 
| Ref | Expression | 
|---|---|
| df-e | 
 | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | ceu 11808 | 
. 2
 | |
| 2 | c1 7880 | 
. . 3
 | |
| 3 | ce 11807 | 
. . 3
 | |
| 4 | 2, 3 | cfv 5258 | 
. 2
 | 
| 5 | 1, 4 | wceq 1364 | 
1
 | 
| Colors of variables: wff set class | 
| This definition is referenced by: esum 11827 ere 11835 ege2le3 11836 efzval 11848 reeff1oleme 15008 loge 15103 logdivlti 15117 | 
| Copyright terms: Public domain | W3C validator |