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 ⊢A∈ℝ∧B∈ℝ→ℝ∖AB=−∞A∪B+∞

Proof

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