# Metamath Proof Explorer

## Theorem difreicc

Description: The class difference of RR and a closed interval. (Contributed by FL, 18-Jun-2007)

Ref Expression
Assertion difreicc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to ℝ\setminus \left[{A},{B}\right]=\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)$

### Proof

Step Hyp Ref Expression
1 eldif ${⊢}{x}\in \left(ℝ\setminus \left[{A},{B}\right]\right)↔\left({x}\in ℝ\wedge ¬{x}\in \left[{A},{B}\right]\right)$
2 rexr ${⊢}{A}\in ℝ\to {A}\in {ℝ}^{*}$
3 rexr ${⊢}{B}\in ℝ\to {B}\in {ℝ}^{*}$
4 elicc1 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({x}\in \left[{A},{B}\right]↔\left({x}\in {ℝ}^{*}\wedge {A}\le {x}\wedge {x}\le {B}\right)\right)$
5 2 3 4 syl2an ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({x}\in \left[{A},{B}\right]↔\left({x}\in {ℝ}^{*}\wedge {A}\le {x}\wedge {x}\le {B}\right)\right)$
6 5 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\to \left({x}\in \left[{A},{B}\right]↔\left({x}\in {ℝ}^{*}\wedge {A}\le {x}\wedge {x}\le {B}\right)\right)$
7 6 notbid ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\to \left(¬{x}\in \left[{A},{B}\right]↔¬\left({x}\in {ℝ}^{*}\wedge {A}\le {x}\wedge {x}\le {B}\right)\right)$
8 3anass ${⊢}\left({x}\in {ℝ}^{*}\wedge {A}\le {x}\wedge {x}\le {B}\right)↔\left({x}\in {ℝ}^{*}\wedge \left({A}\le {x}\wedge {x}\le {B}\right)\right)$
9 8 notbii ${⊢}¬\left({x}\in {ℝ}^{*}\wedge {A}\le {x}\wedge {x}\le {B}\right)↔¬\left({x}\in {ℝ}^{*}\wedge \left({A}\le {x}\wedge {x}\le {B}\right)\right)$
10 ianor ${⊢}¬\left({x}\in {ℝ}^{*}\wedge \left({A}\le {x}\wedge {x}\le {B}\right)\right)↔\left(¬{x}\in {ℝ}^{*}\vee ¬\left({A}\le {x}\wedge {x}\le {B}\right)\right)$
11 rexr ${⊢}{x}\in ℝ\to {x}\in {ℝ}^{*}$
12 11 pm2.24d ${⊢}{x}\in ℝ\to \left(¬{x}\in {ℝ}^{*}\to \left({x}\in \left(\mathrm{-\infty },{A}\right)\vee {x}\in \left({B},\mathrm{+\infty }\right)\right)\right)$
13 12 adantl ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\to \left(¬{x}\in {ℝ}^{*}\to \left({x}\in \left(\mathrm{-\infty },{A}\right)\vee {x}\in \left({B},\mathrm{+\infty }\right)\right)\right)$
14 ianor ${⊢}¬\left({A}\le {x}\wedge {x}\le {B}\right)↔\left(¬{A}\le {x}\vee ¬{x}\le {B}\right)$
15 11 ad2antlr ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\wedge ¬{A}\le {x}\right)\to {x}\in {ℝ}^{*}$
16 mnflt ${⊢}{x}\in ℝ\to \mathrm{-\infty }<{x}$
17 16 ad2antlr ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\wedge ¬{A}\le {x}\right)\to \mathrm{-\infty }<{x}$
18 simpr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\to {x}\in ℝ$
19 simpll ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\to {A}\in ℝ$
20 ltnle ${⊢}\left({x}\in ℝ\wedge {A}\in ℝ\right)\to \left({x}<{A}↔¬{A}\le {x}\right)$
21 20 bicomd ${⊢}\left({x}\in ℝ\wedge {A}\in ℝ\right)\to \left(¬{A}\le {x}↔{x}<{A}\right)$
22 18 19 21 syl2anc ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\to \left(¬{A}\le {x}↔{x}<{A}\right)$
23 22 biimpa ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\wedge ¬{A}\le {x}\right)\to {x}<{A}$
24 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
25 2 ad3antrrr ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\wedge ¬{A}\le {x}\right)\to {A}\in {ℝ}^{*}$
26 elioo1 ${⊢}\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge {A}\in {ℝ}^{*}\right)\to \left({x}\in \left(\mathrm{-\infty },{A}\right)↔\left({x}\in {ℝ}^{*}\wedge \mathrm{-\infty }<{x}\wedge {x}<{A}\right)\right)$
27 24 25 26 sylancr ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\wedge ¬{A}\le {x}\right)\to \left({x}\in \left(\mathrm{-\infty },{A}\right)↔\left({x}\in {ℝ}^{*}\wedge \mathrm{-\infty }<{x}\wedge {x}<{A}\right)\right)$
28 15 17 23 27 mpbir3and ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\wedge ¬{A}\le {x}\right)\to {x}\in \left(\mathrm{-\infty },{A}\right)$
29 28 ex ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\to \left(¬{A}\le {x}\to {x}\in \left(\mathrm{-\infty },{A}\right)\right)$
30 ltnle ${⊢}\left({B}\in ℝ\wedge {x}\in ℝ\right)\to \left({B}<{x}↔¬{x}\le {B}\right)$
31 30 adantll ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\to \left({B}<{x}↔¬{x}\le {B}\right)$
32 11 ad2antlr ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\wedge {B}<{x}\right)\to {x}\in {ℝ}^{*}$
33 simpr ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\wedge {B}<{x}\right)\to {B}<{x}$
34 ltpnf ${⊢}{x}\in ℝ\to {x}<\mathrm{+\infty }$
35 34 ad2antlr ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\wedge {B}<{x}\right)\to {x}<\mathrm{+\infty }$
36 3 ad3antlr ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\wedge {B}<{x}\right)\to {B}\in {ℝ}^{*}$
37 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
38 elioo1 ${⊢}\left({B}\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left({x}\in \left({B},\mathrm{+\infty }\right)↔\left({x}\in {ℝ}^{*}\wedge {B}<{x}\wedge {x}<\mathrm{+\infty }\right)\right)$
39 36 37 38 sylancl ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\wedge {B}<{x}\right)\to \left({x}\in \left({B},\mathrm{+\infty }\right)↔\left({x}\in {ℝ}^{*}\wedge {B}<{x}\wedge {x}<\mathrm{+\infty }\right)\right)$
40 32 33 35 39 mpbir3and ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\wedge {B}<{x}\right)\to {x}\in \left({B},\mathrm{+\infty }\right)$
41 40 ex ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\to \left({B}<{x}\to {x}\in \left({B},\mathrm{+\infty }\right)\right)$
42 31 41 sylbird ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\to \left(¬{x}\le {B}\to {x}\in \left({B},\mathrm{+\infty }\right)\right)$
43 29 42 orim12d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\to \left(\left(¬{A}\le {x}\vee ¬{x}\le {B}\right)\to \left({x}\in \left(\mathrm{-\infty },{A}\right)\vee {x}\in \left({B},\mathrm{+\infty }\right)\right)\right)$
44 14 43 syl5bi ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\to \left(¬\left({A}\le {x}\wedge {x}\le {B}\right)\to \left({x}\in \left(\mathrm{-\infty },{A}\right)\vee {x}\in \left({B},\mathrm{+\infty }\right)\right)\right)$
45 13 44 jaod ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\to \left(\left(¬{x}\in {ℝ}^{*}\vee ¬\left({A}\le {x}\wedge {x}\le {B}\right)\right)\to \left({x}\in \left(\mathrm{-\infty },{A}\right)\vee {x}\in \left({B},\mathrm{+\infty }\right)\right)\right)$
46 10 45 syl5bi ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\to \left(¬\left({x}\in {ℝ}^{*}\wedge \left({A}\le {x}\wedge {x}\le {B}\right)\right)\to \left({x}\in \left(\mathrm{-\infty },{A}\right)\vee {x}\in \left({B},\mathrm{+\infty }\right)\right)\right)$
47 9 46 syl5bi ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\to \left(¬\left({x}\in {ℝ}^{*}\wedge {A}\le {x}\wedge {x}\le {B}\right)\to \left({x}\in \left(\mathrm{-\infty },{A}\right)\vee {x}\in \left({B},\mathrm{+\infty }\right)\right)\right)$
48 7 47 sylbid ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in ℝ\right)\to \left(¬{x}\in \left[{A},{B}\right]\to \left({x}\in \left(\mathrm{-\infty },{A}\right)\vee {x}\in \left({B},\mathrm{+\infty }\right)\right)\right)$
49 48 expimpd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left({x}\in ℝ\wedge ¬{x}\in \left[{A},{B}\right]\right)\to \left({x}\in \left(\mathrm{-\infty },{A}\right)\vee {x}\in \left({B},\mathrm{+\infty }\right)\right)\right)$
50 elun ${⊢}{x}\in \left(\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)\right)↔\left({x}\in \left(\mathrm{-\infty },{A}\right)\vee {x}\in \left({B},\mathrm{+\infty }\right)\right)$
51 49 50 syl6ibr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left({x}\in ℝ\wedge ¬{x}\in \left[{A},{B}\right]\right)\to {x}\in \left(\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)\right)\right)$
52 ioossre ${⊢}\left(\mathrm{-\infty },{A}\right)\subseteq ℝ$
53 ioossre ${⊢}\left({B},\mathrm{+\infty }\right)\subseteq ℝ$
54 52 53 unssi ${⊢}\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)\subseteq ℝ$
55 54 sseli ${⊢}{x}\in \left(\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)\right)\to {x}\in ℝ$
56 55 adantl ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in \left(\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)\right)\right)\to {x}\in ℝ$
57 elioo2 ${⊢}\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge {A}\in {ℝ}^{*}\right)\to \left({x}\in \left(\mathrm{-\infty },{A}\right)↔\left({x}\in ℝ\wedge \mathrm{-\infty }<{x}\wedge {x}<{A}\right)\right)$
58 24 2 57 sylancr ${⊢}{A}\in ℝ\to \left({x}\in \left(\mathrm{-\infty },{A}\right)↔\left({x}\in ℝ\wedge \mathrm{-\infty }<{x}\wedge {x}<{A}\right)\right)$
59 58 adantr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({x}\in \left(\mathrm{-\infty },{A}\right)↔\left({x}\in ℝ\wedge \mathrm{-\infty }<{x}\wedge {x}<{A}\right)\right)$
60 20 biimpd ${⊢}\left({x}\in ℝ\wedge {A}\in ℝ\right)\to \left({x}<{A}\to ¬{A}\le {x}\right)$
61 60 ex ${⊢}{x}\in ℝ\to \left({A}\in ℝ\to \left({x}<{A}\to ¬{A}\le {x}\right)\right)$
62 61 a1i ${⊢}\mathrm{-\infty }<{x}\to \left({x}\in ℝ\to \left({A}\in ℝ\to \left({x}<{A}\to ¬{A}\le {x}\right)\right)\right)$
63 62 com13 ${⊢}{A}\in ℝ\to \left({x}\in ℝ\to \left(\mathrm{-\infty }<{x}\to \left({x}<{A}\to ¬{A}\le {x}\right)\right)\right)$
64 63 adantr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({x}\in ℝ\to \left(\mathrm{-\infty }<{x}\to \left({x}<{A}\to ¬{A}\le {x}\right)\right)\right)$
65 64 3impd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left({x}\in ℝ\wedge \mathrm{-\infty }<{x}\wedge {x}<{A}\right)\to ¬{A}\le {x}\right)$
66 59 65 sylbid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({x}\in \left(\mathrm{-\infty },{A}\right)\to ¬{A}\le {x}\right)$
67 3 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {B}\in {ℝ}^{*}$
68 67 37 38 sylancl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({x}\in \left({B},\mathrm{+\infty }\right)↔\left({x}\in {ℝ}^{*}\wedge {B}<{x}\wedge {x}<\mathrm{+\infty }\right)\right)$
69 xrltnle ${⊢}\left({B}\in {ℝ}^{*}\wedge {x}\in {ℝ}^{*}\right)\to \left({B}<{x}↔¬{x}\le {B}\right)$
70 69 biimpd ${⊢}\left({B}\in {ℝ}^{*}\wedge {x}\in {ℝ}^{*}\right)\to \left({B}<{x}\to ¬{x}\le {B}\right)$
71 70 ex ${⊢}{B}\in {ℝ}^{*}\to \left({x}\in {ℝ}^{*}\to \left({B}<{x}\to ¬{x}\le {B}\right)\right)$
72 71 a1ddd ${⊢}{B}\in {ℝ}^{*}\to \left({x}\in {ℝ}^{*}\to \left({B}<{x}\to \left({x}<\mathrm{+\infty }\to ¬{x}\le {B}\right)\right)\right)$
73 3 72 syl ${⊢}{B}\in ℝ\to \left({x}\in {ℝ}^{*}\to \left({B}<{x}\to \left({x}<\mathrm{+\infty }\to ¬{x}\le {B}\right)\right)\right)$
74 73 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({x}\in {ℝ}^{*}\to \left({B}<{x}\to \left({x}<\mathrm{+\infty }\to ¬{x}\le {B}\right)\right)\right)$
75 74 3impd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left({x}\in {ℝ}^{*}\wedge {B}<{x}\wedge {x}<\mathrm{+\infty }\right)\to ¬{x}\le {B}\right)$
76 68 75 sylbid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({x}\in \left({B},\mathrm{+\infty }\right)\to ¬{x}\le {B}\right)$
77 66 76 orim12d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left({x}\in \left(\mathrm{-\infty },{A}\right)\vee {x}\in \left({B},\mathrm{+\infty }\right)\right)\to \left(¬{A}\le {x}\vee ¬{x}\le {B}\right)\right)$
78 50 77 syl5bi ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({x}\in \left(\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)\right)\to \left(¬{A}\le {x}\vee ¬{x}\le {B}\right)\right)$
79 78 imp ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in \left(\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)\right)\right)\to \left(¬{A}\le {x}\vee ¬{x}\le {B}\right)$
80 79 14 sylibr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in \left(\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)\right)\right)\to ¬\left({A}\le {x}\wedge {x}\le {B}\right)$
81 80 intnand ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in \left(\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)\right)\right)\to ¬\left({x}\in {ℝ}^{*}\wedge \left({A}\le {x}\wedge {x}\le {B}\right)\right)$
82 81 8 sylnibr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in \left(\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)\right)\right)\to ¬\left({x}\in {ℝ}^{*}\wedge {A}\le {x}\wedge {x}\le {B}\right)$
83 2 3 anim12i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)$
84 83 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in \left(\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)\right)\right)\to \left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)$
85 4 notbid ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(¬{x}\in \left[{A},{B}\right]↔¬\left({x}\in {ℝ}^{*}\wedge {A}\le {x}\wedge {x}\le {B}\right)\right)$
86 84 85 syl ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in \left(\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)\right)\right)\to \left(¬{x}\in \left[{A},{B}\right]↔¬\left({x}\in {ℝ}^{*}\wedge {A}\le {x}\wedge {x}\le {B}\right)\right)$
87 82 86 mpbird ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in \left(\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)\right)\right)\to ¬{x}\in \left[{A},{B}\right]$
88 56 87 jca ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in \left(\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)\right)\right)\to \left({x}\in ℝ\wedge ¬{x}\in \left[{A},{B}\right]\right)$
89 88 ex ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({x}\in \left(\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)\right)\to \left({x}\in ℝ\wedge ¬{x}\in \left[{A},{B}\right]\right)\right)$
90 51 89 impbid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left({x}\in ℝ\wedge ¬{x}\in \left[{A},{B}\right]\right)↔{x}\in \left(\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)\right)\right)$
91 1 90 syl5bb ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({x}\in \left(ℝ\setminus \left[{A},{B}\right]\right)↔{x}\in \left(\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)\right)\right)$
92 91 eqrdv ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to ℝ\setminus \left[{A},{B}\right]=\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)$