Metamath Proof Explorer

Theorem negpitopissre

Description: The interval ( -upi (,] pi ) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Assertion negpitopissre 
|- ( -u _pi (,] _pi ) C_ RR

Proof

Step Hyp Ref Expression
1 pire 
 |-  _pi e. RR
2 1 renegcli 
 |-  -u _pi e. RR
3 2 rexri 
 |-  -u _pi e. RR*
4 iocssre 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR ) -> ( -u _pi (,] _pi ) C_ RR )
5 3 1 4 mp2an 
 |-  ( -u _pi (,] _pi ) C_ RR