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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) = ( ( -∞ (,) 𝐴 ) ∪ ( 𝐵 (,) +∞ ) ) )

Proof

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