Metamath Proof Explorer

Theorem pire

Description: _pi is a real number. (Contributed by Paul Chapman, 23-Jan-2008)

Ref Expression
Assertion pire 
|- _pi e. RR

Proof

Step Hyp Ref Expression
1 pilem3 
 |-  ( _pi e. ( 2 (,) 4 ) /\ ( sin ` _pi ) = 0 )
2 1 simpli 
 |-  _pi e. ( 2 (,) 4 )
3 elioore 
 |-  ( _pi e. ( 2 (,) 4 ) -> _pi e. RR )
4 2 3 ax-mp 
 |-  _pi e. RR