Step | Hyp | Ref
| Expression |
1 | | eldif 3808 |
. . 3
⊢ (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ (𝐴[,]𝐵))) |
2 | | rexr 10402 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) |
3 | | rexr 10402 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℝ*) |
4 | | elicc1 12507 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
5 | 2, 3, 4 | syl2an 591 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
6 | 5 | adantr 474 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
7 | 6 | notbid 310 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (¬
𝑥 ∈ (𝐴[,]𝐵) ↔ ¬ (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
8 | | 3anass 1122 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ*
∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵) ↔ (𝑥 ∈ ℝ* ∧ (𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
9 | 8 | notbii 312 |
. . . . . . . 8
⊢ (¬
(𝑥 ∈
ℝ* ∧ 𝐴
≤ 𝑥 ∧ 𝑥 ≤ 𝐵) ↔ ¬ (𝑥 ∈ ℝ* ∧ (𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
10 | | ianor 1011 |
. . . . . . . . 9
⊢ (¬
(𝑥 ∈
ℝ* ∧ (𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) ↔ (¬ 𝑥 ∈ ℝ* ∨ ¬ (𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
11 | | rexr 10402 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
12 | 11 | pm2.24d 149 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → (¬
𝑥 ∈
ℝ* → (𝑥 ∈ (-∞(,)𝐴) ∨ 𝑥 ∈ (𝐵(,)+∞)))) |
13 | 12 | adantl 475 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (¬
𝑥 ∈
ℝ* → (𝑥 ∈ (-∞(,)𝐴) ∨ 𝑥 ∈ (𝐵(,)+∞)))) |
14 | | ianor 1011 |
. . . . . . . . . . 11
⊢ (¬
(𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵) ↔ (¬ 𝐴 ≤ 𝑥 ∨ ¬ 𝑥 ≤ 𝐵)) |
15 | 11 | ad2antlr 720 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ¬
𝐴 ≤ 𝑥) → 𝑥 ∈ ℝ*) |
16 | | mnflt 12243 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ → -∞
< 𝑥) |
17 | 16 | ad2antlr 720 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ¬
𝐴 ≤ 𝑥) → -∞ < 𝑥) |
18 | | simpr 479 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈
ℝ) |
19 | | simpll 785 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈
ℝ) |
20 | | ltnle 10436 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑥 < 𝐴 ↔ ¬ 𝐴 ≤ 𝑥)) |
21 | 20 | bicomd 215 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (¬
𝐴 ≤ 𝑥 ↔ 𝑥 < 𝐴)) |
22 | 18, 19, 21 | syl2anc 581 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (¬
𝐴 ≤ 𝑥 ↔ 𝑥 < 𝐴)) |
23 | 22 | biimpa 470 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ¬
𝐴 ≤ 𝑥) → 𝑥 < 𝐴) |
24 | | mnfxr 10414 |
. . . . . . . . . . . . . . 15
⊢ -∞
∈ ℝ* |
25 | 2 | ad3antrrr 723 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ¬
𝐴 ≤ 𝑥) → 𝐴 ∈
ℝ*) |
26 | | elioo1 12503 |
. . . . . . . . . . . . . . 15
⊢
((-∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (𝑥 ∈ (-∞(,)𝐴) ↔ (𝑥 ∈ ℝ* ∧ -∞
< 𝑥 ∧ 𝑥 < 𝐴))) |
27 | 24, 25, 26 | sylancr 583 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ¬
𝐴 ≤ 𝑥) → (𝑥 ∈ (-∞(,)𝐴) ↔ (𝑥 ∈ ℝ* ∧ -∞
< 𝑥 ∧ 𝑥 < 𝐴))) |
28 | 15, 17, 23, 27 | mpbir3and 1448 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ¬
𝐴 ≤ 𝑥) → 𝑥 ∈ (-∞(,)𝐴)) |
29 | 28 | ex 403 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (¬
𝐴 ≤ 𝑥 → 𝑥 ∈ (-∞(,)𝐴))) |
30 | | ltnle 10436 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 ↔ ¬ 𝑥 ≤ 𝐵)) |
31 | 30 | adantll 707 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 ↔ ¬ 𝑥 ≤ 𝐵)) |
32 | 11 | ad2antlr 720 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ*) |
33 | | simpr 479 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥) |
34 | | ltpnf 12240 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ → 𝑥 < +∞) |
35 | 34 | ad2antlr 720 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 < +∞) |
36 | 3 | ad3antlr 724 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝐵 ∈
ℝ*) |
37 | | pnfxr 10410 |
. . . . . . . . . . . . . . . 16
⊢ +∞
∈ ℝ* |
38 | | elioo1 12503 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (𝑥 ∈ (𝐵(,)+∞) ↔ (𝑥 ∈ ℝ* ∧ 𝐵 < 𝑥 ∧ 𝑥 < +∞))) |
39 | 36, 37, 38 | sylancl 582 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → (𝑥 ∈ (𝐵(,)+∞) ↔ (𝑥 ∈ ℝ* ∧ 𝐵 < 𝑥 ∧ 𝑥 < +∞))) |
40 | 32, 33, 35, 39 | mpbir3and 1448 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 ∈ (𝐵(,)+∞)) |
41 | 40 | ex 403 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 → 𝑥 ∈ (𝐵(,)+∞))) |
42 | 31, 41 | sylbird 252 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (¬
𝑥 ≤ 𝐵 → 𝑥 ∈ (𝐵(,)+∞))) |
43 | 29, 42 | orim12d 994 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((¬
𝐴 ≤ 𝑥 ∨ ¬ 𝑥 ≤ 𝐵) → (𝑥 ∈ (-∞(,)𝐴) ∨ 𝑥 ∈ (𝐵(,)+∞)))) |
44 | 14, 43 | syl5bi 234 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (¬
(𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵) → (𝑥 ∈ (-∞(,)𝐴) ∨ 𝑥 ∈ (𝐵(,)+∞)))) |
45 | 13, 44 | jaod 892 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((¬
𝑥 ∈
ℝ* ∨ ¬ (𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) → (𝑥 ∈ (-∞(,)𝐴) ∨ 𝑥 ∈ (𝐵(,)+∞)))) |
46 | 10, 45 | syl5bi 234 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (¬
(𝑥 ∈
ℝ* ∧ (𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) → (𝑥 ∈ (-∞(,)𝐴) ∨ 𝑥 ∈ (𝐵(,)+∞)))) |
47 | 9, 46 | syl5bi 234 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (¬
(𝑥 ∈
ℝ* ∧ 𝐴
≤ 𝑥 ∧ 𝑥 ≤ 𝐵) → (𝑥 ∈ (-∞(,)𝐴) ∨ 𝑥 ∈ (𝐵(,)+∞)))) |
48 | 7, 47 | sylbid 232 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (¬
𝑥 ∈ (𝐴[,]𝐵) → (𝑥 ∈ (-∞(,)𝐴) ∨ 𝑥 ∈ (𝐵(,)+∞)))) |
49 | 48 | expimpd 447 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝑥 ∈ ℝ ∧ ¬
𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ (-∞(,)𝐴) ∨ 𝑥 ∈ (𝐵(,)+∞)))) |
50 | | elun 3980 |
. . . . 5
⊢ (𝑥 ∈ ((-∞(,)𝐴) ∪ (𝐵(,)+∞)) ↔ (𝑥 ∈ (-∞(,)𝐴) ∨ 𝑥 ∈ (𝐵(,)+∞))) |
51 | 49, 50 | syl6ibr 244 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝑥 ∈ ℝ ∧ ¬
𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ((-∞(,)𝐴) ∪ (𝐵(,)+∞)))) |
52 | | ioossre 12523 |
. . . . . . . . 9
⊢
(-∞(,)𝐴)
⊆ ℝ |
53 | | ioossre 12523 |
. . . . . . . . 9
⊢ (𝐵(,)+∞) ⊆
ℝ |
54 | 52, 53 | unssi 4015 |
. . . . . . . 8
⊢
((-∞(,)𝐴)
∪ (𝐵(,)+∞))
⊆ ℝ |
55 | 54 | sseli 3823 |
. . . . . . 7
⊢ (𝑥 ∈ ((-∞(,)𝐴) ∪ (𝐵(,)+∞)) → 𝑥 ∈ ℝ) |
56 | 55 | adantl 475 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ((-∞(,)𝐴) ∪ (𝐵(,)+∞))) → 𝑥 ∈ ℝ) |
57 | | elioo2 12504 |
. . . . . . . . . . . . . . . 16
⊢
((-∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (𝑥 ∈ (-∞(,)𝐴) ↔ (𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 < 𝐴))) |
58 | 24, 2, 57 | sylancr 583 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ → (𝑥 ∈ (-∞(,)𝐴) ↔ (𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 < 𝐴))) |
59 | 58 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (-∞(,)𝐴) ↔ (𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 < 𝐴))) |
60 | 20 | biimpd 221 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑥 < 𝐴 → ¬ 𝐴 ≤ 𝑥)) |
61 | 60 | ex 403 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ → (𝐴 ∈ ℝ → (𝑥 < 𝐴 → ¬ 𝐴 ≤ 𝑥))) |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (-∞
< 𝑥 → (𝑥 ∈ ℝ → (𝐴 ∈ ℝ → (𝑥 < 𝐴 → ¬ 𝐴 ≤ 𝑥)))) |
63 | 62 | com13 88 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℝ → (𝑥 ∈ ℝ → (-∞
< 𝑥 → (𝑥 < 𝐴 → ¬ 𝐴 ≤ 𝑥)))) |
64 | 63 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ ℝ → (-∞
< 𝑥 → (𝑥 < 𝐴 → ¬ 𝐴 ≤ 𝑥)))) |
65 | 64 | 3impd 1463 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝑥 ∈ ℝ ∧ -∞
< 𝑥 ∧ 𝑥 < 𝐴) → ¬ 𝐴 ≤ 𝑥)) |
66 | 59, 65 | sylbid 232 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (-∞(,)𝐴) → ¬ 𝐴 ≤ 𝑥)) |
67 | 3 | adantl 475 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈
ℝ*) |
68 | 67, 37, 38 | sylancl 582 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐵(,)+∞) ↔ (𝑥 ∈ ℝ* ∧ 𝐵 < 𝑥 ∧ 𝑥 < +∞))) |
69 | | xrltnle 10424 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐵 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → (𝐵 < 𝑥 ↔ ¬ 𝑥 ≤ 𝐵)) |
70 | 69 | biimpd 221 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐵 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → (𝐵 < 𝑥 → ¬ 𝑥 ≤ 𝐵)) |
71 | 70 | ex 403 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 ∈ ℝ*
→ (𝑥 ∈
ℝ* → (𝐵 < 𝑥 → ¬ 𝑥 ≤ 𝐵))) |
72 | 71 | com3l 89 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ*
→ (𝐵 < 𝑥 → (𝐵 ∈ ℝ* → ¬
𝑥 ≤ 𝐵))) |
73 | 72 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 < +∞ → (𝑥 ∈ ℝ*
→ (𝐵 < 𝑥 → (𝐵 ∈ ℝ* → ¬
𝑥 ≤ 𝐵)))) |
74 | 73 | com14 96 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ ℝ*
→ (𝑥 ∈
ℝ* → (𝐵 < 𝑥 → (𝑥 < +∞ → ¬ 𝑥 ≤ 𝐵)))) |
75 | 3, 74 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ ℝ → (𝑥 ∈ ℝ*
→ (𝐵 < 𝑥 → (𝑥 < +∞ → ¬ 𝑥 ≤ 𝐵)))) |
76 | 75 | adantl 475 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ ℝ*
→ (𝐵 < 𝑥 → (𝑥 < +∞ → ¬ 𝑥 ≤ 𝐵)))) |
77 | 76 | 3impd 1463 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝑥 ∈ ℝ*
∧ 𝐵 < 𝑥 ∧ 𝑥 < +∞) → ¬ 𝑥 ≤ 𝐵)) |
78 | 68, 77 | sylbid 232 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐵(,)+∞) → ¬ 𝑥 ≤ 𝐵)) |
79 | 66, 78 | orim12d 994 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝑥 ∈ (-∞(,)𝐴) ∨ 𝑥 ∈ (𝐵(,)+∞)) → (¬ 𝐴 ≤ 𝑥 ∨ ¬ 𝑥 ≤ 𝐵))) |
80 | 50, 79 | syl5bi 234 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ ((-∞(,)𝐴) ∪ (𝐵(,)+∞)) → (¬ 𝐴 ≤ 𝑥 ∨ ¬ 𝑥 ≤ 𝐵))) |
81 | 80 | imp 397 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ((-∞(,)𝐴) ∪ (𝐵(,)+∞))) → (¬ 𝐴 ≤ 𝑥 ∨ ¬ 𝑥 ≤ 𝐵)) |
82 | 81, 14 | sylibr 226 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ((-∞(,)𝐴) ∪ (𝐵(,)+∞))) → ¬ (𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) |
83 | 82 | intnand 484 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ((-∞(,)𝐴) ∪ (𝐵(,)+∞))) → ¬ (𝑥 ∈ ℝ*
∧ (𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
84 | 83, 8 | sylnibr 321 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ((-∞(,)𝐴) ∪ (𝐵(,)+∞))) → ¬ (𝑥 ∈ ℝ*
∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) |
85 | 2, 3 | anim12i 608 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*)) |
86 | 85 | adantr 474 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ((-∞(,)𝐴) ∪ (𝐵(,)+∞))) → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) |
87 | 4 | notbid 310 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (¬ 𝑥 ∈ (𝐴[,]𝐵) ↔ ¬ (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
88 | 86, 87 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ((-∞(,)𝐴) ∪ (𝐵(,)+∞))) → (¬ 𝑥 ∈ (𝐴[,]𝐵) ↔ ¬ (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
89 | 84, 88 | mpbird 249 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ((-∞(,)𝐴) ∪ (𝐵(,)+∞))) → ¬ 𝑥 ∈ (𝐴[,]𝐵)) |
90 | 56, 89 | jca 509 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ((-∞(,)𝐴) ∪ (𝐵(,)+∞))) → (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ (𝐴[,]𝐵))) |
91 | 90 | ex 403 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ ((-∞(,)𝐴) ∪ (𝐵(,)+∞)) → (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ (𝐴[,]𝐵)))) |
92 | 51, 91 | impbid 204 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝑥 ∈ ℝ ∧ ¬
𝑥 ∈ (𝐴[,]𝐵)) ↔ 𝑥 ∈ ((-∞(,)𝐴) ∪ (𝐵(,)+∞)))) |
93 | 1, 92 | syl5bb 275 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) ↔ 𝑥 ∈ ((-∞(,)𝐴) ∪ (𝐵(,)+∞)))) |
94 | 93 | eqrdv 2823 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (ℝ
∖ (𝐴[,]𝐵)) = ((-∞(,)𝐴) ∪ (𝐵(,)+∞))) |