| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > pire | Structured version Visualization version GIF version | ||
| Description: π is a real number. (Contributed by Paul Chapman, 23-Jan-2008.) |
| Ref | Expression |
|---|---|
| pire | ⊢ π ∈ ℝ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pilem3 26497 | . . 3 ⊢ (π ∈ (2(,)4) ∧ (sin‘π) = 0) | |
| 2 | 1 | simpli 483 | . 2 ⊢ π ∈ (2(,)4) |
| 3 | elioore 13417 | . 2 ⊢ (π ∈ (2(,)4) → π ∈ ℝ) | |
| 4 | 2, 3 | ax-mp 5 | 1 ⊢ π ∈ ℝ |
| Copyright terms: Public domain | W3C validator |