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