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 |
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 |