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 e. RR /\ B e. RR ) -> ( RR \ ( A [,] B ) ) = ( ( -oo (,) A ) u. ( B (,) +oo ) ) )

Proof

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