Description: Define the constant pi, _pi = 3.14159..., which is the smallest positive number whose sine is zero. Definition of _pi in Gleason p. 311. (Contributed by Paul Chapman, 23-Jan-2008) (Revised by AV, 14-Sep-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-pi | |- _pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cpi | |- _pi |
|
| 1 | crp | |- RR+ |
|
| 2 | csin | |- sin |
|
| 3 | 2 | ccnv | |- `' sin |
| 4 | cc0 | |- 0 |
|
| 5 | 4 | csn | |- { 0 } |
| 6 | 3 5 | cima | |- ( `' sin " { 0 } ) |
| 7 | 1 6 | cin | |- ( RR+ i^i ( `' sin " { 0 } ) ) |
| 8 | cr | |- RR |
|
| 9 | clt | |- < |
|
| 10 | 7 8 9 | cinf | |- inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) |
| 11 | 0 10 | wceq | |- _pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) |