# Metamath Proof Explorer

## Theorem xrdifh

Description: Class difference of a half-open interval in the extended reals. (Contributed by Thierry Arnoux, 1-Aug-2017)

Ref Expression
Hypothesis xrdifh.1 ${⊢}{A}\in {ℝ}^{*}$
Assertion xrdifh ${⊢}{ℝ}^{*}\setminus \left[{A},\mathrm{+\infty }\right]=\left[\mathrm{-\infty },{A}\right)$

### Proof

Step Hyp Ref Expression
1 xrdifh.1 ${⊢}{A}\in {ℝ}^{*}$
2 biortn ${⊢}{x}\in {ℝ}^{*}\to \left(\left(¬{A}\le {x}\vee ¬{x}\le \mathrm{+\infty }\right)↔\left(¬{x}\in {ℝ}^{*}\vee \left(¬{A}\le {x}\vee ¬{x}\le \mathrm{+\infty }\right)\right)\right)$
3 pnfge ${⊢}{x}\in {ℝ}^{*}\to {x}\le \mathrm{+\infty }$
4 3 notnotd ${⊢}{x}\in {ℝ}^{*}\to ¬¬{x}\le \mathrm{+\infty }$
5 biorf ${⊢}¬¬{x}\le \mathrm{+\infty }\to \left(¬{A}\le {x}↔\left(¬{x}\le \mathrm{+\infty }\vee ¬{A}\le {x}\right)\right)$
6 4 5 syl ${⊢}{x}\in {ℝ}^{*}\to \left(¬{A}\le {x}↔\left(¬{x}\le \mathrm{+\infty }\vee ¬{A}\le {x}\right)\right)$
7 orcom ${⊢}\left(¬{A}\le {x}\vee ¬{x}\le \mathrm{+\infty }\right)↔\left(¬{x}\le \mathrm{+\infty }\vee ¬{A}\le {x}\right)$
8 6 7 syl6bbr ${⊢}{x}\in {ℝ}^{*}\to \left(¬{A}\le {x}↔\left(¬{A}\le {x}\vee ¬{x}\le \mathrm{+\infty }\right)\right)$
9 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
10 elicc1 ${⊢}\left({A}\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left({x}\in \left[{A},\mathrm{+\infty }\right]↔\left({x}\in {ℝ}^{*}\wedge {A}\le {x}\wedge {x}\le \mathrm{+\infty }\right)\right)$
11 1 9 10 mp2an ${⊢}{x}\in \left[{A},\mathrm{+\infty }\right]↔\left({x}\in {ℝ}^{*}\wedge {A}\le {x}\wedge {x}\le \mathrm{+\infty }\right)$
12 11 notbii ${⊢}¬{x}\in \left[{A},\mathrm{+\infty }\right]↔¬\left({x}\in {ℝ}^{*}\wedge {A}\le {x}\wedge {x}\le \mathrm{+\infty }\right)$
13 3ianor ${⊢}¬\left({x}\in {ℝ}^{*}\wedge {A}\le {x}\wedge {x}\le \mathrm{+\infty }\right)↔\left(¬{x}\in {ℝ}^{*}\vee ¬{A}\le {x}\vee ¬{x}\le \mathrm{+\infty }\right)$
14 3orass ${⊢}\left(¬{x}\in {ℝ}^{*}\vee ¬{A}\le {x}\vee ¬{x}\le \mathrm{+\infty }\right)↔\left(¬{x}\in {ℝ}^{*}\vee \left(¬{A}\le {x}\vee ¬{x}\le \mathrm{+\infty }\right)\right)$
15 12 13 14 3bitri ${⊢}¬{x}\in \left[{A},\mathrm{+\infty }\right]↔\left(¬{x}\in {ℝ}^{*}\vee \left(¬{A}\le {x}\vee ¬{x}\le \mathrm{+\infty }\right)\right)$
16 15 a1i ${⊢}{x}\in {ℝ}^{*}\to \left(¬{x}\in \left[{A},\mathrm{+\infty }\right]↔\left(¬{x}\in {ℝ}^{*}\vee \left(¬{A}\le {x}\vee ¬{x}\le \mathrm{+\infty }\right)\right)\right)$
17 2 8 16 3bitr4rd ${⊢}{x}\in {ℝ}^{*}\to \left(¬{x}\in \left[{A},\mathrm{+\infty }\right]↔¬{A}\le {x}\right)$
18 xrltnle ${⊢}\left({x}\in {ℝ}^{*}\wedge {A}\in {ℝ}^{*}\right)\to \left({x}<{A}↔¬{A}\le {x}\right)$
19 1 18 mpan2 ${⊢}{x}\in {ℝ}^{*}\to \left({x}<{A}↔¬{A}\le {x}\right)$
20 17 19 bitr4d ${⊢}{x}\in {ℝ}^{*}\to \left(¬{x}\in \left[{A},\mathrm{+\infty }\right]↔{x}<{A}\right)$
21 20 pm5.32i ${⊢}\left({x}\in {ℝ}^{*}\wedge ¬{x}\in \left[{A},\mathrm{+\infty }\right]\right)↔\left({x}\in {ℝ}^{*}\wedge {x}<{A}\right)$
22 eldif ${⊢}{x}\in \left({ℝ}^{*}\setminus \left[{A},\mathrm{+\infty }\right]\right)↔\left({x}\in {ℝ}^{*}\wedge ¬{x}\in \left[{A},\mathrm{+\infty }\right]\right)$
23 3anass ${⊢}\left({x}\in {ℝ}^{*}\wedge \mathrm{-\infty }\le {x}\wedge {x}<{A}\right)↔\left({x}\in {ℝ}^{*}\wedge \left(\mathrm{-\infty }\le {x}\wedge {x}<{A}\right)\right)$
24 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
25 elico1 ${⊢}\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge {A}\in {ℝ}^{*}\right)\to \left({x}\in \left[\mathrm{-\infty },{A}\right)↔\left({x}\in {ℝ}^{*}\wedge \mathrm{-\infty }\le {x}\wedge {x}<{A}\right)\right)$
26 24 1 25 mp2an ${⊢}{x}\in \left[\mathrm{-\infty },{A}\right)↔\left({x}\in {ℝ}^{*}\wedge \mathrm{-\infty }\le {x}\wedge {x}<{A}\right)$
27 mnfle ${⊢}{x}\in {ℝ}^{*}\to \mathrm{-\infty }\le {x}$
28 27 biantrurd ${⊢}{x}\in {ℝ}^{*}\to \left({x}<{A}↔\left(\mathrm{-\infty }\le {x}\wedge {x}<{A}\right)\right)$
29 28 pm5.32i ${⊢}\left({x}\in {ℝ}^{*}\wedge {x}<{A}\right)↔\left({x}\in {ℝ}^{*}\wedge \left(\mathrm{-\infty }\le {x}\wedge {x}<{A}\right)\right)$
30 23 26 29 3bitr4i ${⊢}{x}\in \left[\mathrm{-\infty },{A}\right)↔\left({x}\in {ℝ}^{*}\wedge {x}<{A}\right)$
31 21 22 30 3bitr4i ${⊢}{x}\in \left({ℝ}^{*}\setminus \left[{A},\mathrm{+\infty }\right]\right)↔{x}\in \left[\mathrm{-\infty },{A}\right)$
32 31 eqriv ${⊢}{ℝ}^{*}\setminus \left[{A},\mathrm{+\infty }\right]=\left[\mathrm{-\infty },{A}\right)$