Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ (𝐶 ∈ (𝐴[,]𝐵) ∧ ¬ 𝐶 ∈ (𝐴[,)𝐵))) → 𝐴 ∈
ℝ*) |
2 | | simpl2 1193 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ (𝐶 ∈ (𝐴[,]𝐵) ∧ ¬ 𝐶 ∈ (𝐴[,)𝐵))) → 𝐵 ∈
ℝ*) |
3 | | simprl 770 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ (𝐶 ∈ (𝐴[,]𝐵) ∧ ¬ 𝐶 ∈ (𝐴[,)𝐵))) → 𝐶 ∈ (𝐴[,]𝐵)) |
4 | | elicc1 13317 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) |
5 | 4 | biimpa 478 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) |
6 | 5 | simp1d 1143 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ∈
ℝ*) |
7 | 1, 2, 3, 6 | syl21anc 837 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ (𝐶 ∈ (𝐴[,]𝐵) ∧ ¬ 𝐶 ∈ (𝐴[,)𝐵))) → 𝐶 ∈
ℝ*) |
8 | 5 | simp3d 1145 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ≤ 𝐵) |
9 | 1, 2, 3, 8 | syl21anc 837 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ (𝐶 ∈ (𝐴[,]𝐵) ∧ ¬ 𝐶 ∈ (𝐴[,)𝐵))) → 𝐶 ≤ 𝐵) |
10 | 1, 2 | jca 513 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ (𝐶 ∈ (𝐴[,]𝐵) ∧ ¬ 𝐶 ∈ (𝐴[,)𝐵))) → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) |
11 | | simprr 772 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ (𝐶 ∈ (𝐴[,]𝐵) ∧ ¬ 𝐶 ∈ (𝐴[,)𝐵))) → ¬ 𝐶 ∈ (𝐴[,)𝐵)) |
12 | 5 | simp2d 1144 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝐶) |
13 | 10, 3, 12 | syl2anc 585 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ (𝐶 ∈ (𝐴[,]𝐵) ∧ ¬ 𝐶 ∈ (𝐴[,)𝐵))) → 𝐴 ≤ 𝐶) |
14 | | elico1 13316 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵))) |
15 | 14 | notbid 318 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (¬ 𝐶 ∈ (𝐴[,)𝐵) ↔ ¬ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵))) |
16 | 15 | biimpa 478 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ ¬ 𝐶 ∈ (𝐴[,)𝐵)) → ¬ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) |
17 | | df-3an 1090 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ ℝ*
∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵) ↔ ((𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶) ∧ 𝐶 < 𝐵)) |
18 | 17 | notbii 320 |
. . . . . . . . 9
⊢ (¬
(𝐶 ∈
ℝ* ∧ 𝐴
≤ 𝐶 ∧ 𝐶 < 𝐵) ↔ ¬ ((𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶) ∧ 𝐶 < 𝐵)) |
19 | | imnan 401 |
. . . . . . . . 9
⊢ (((𝐶 ∈ ℝ*
∧ 𝐴 ≤ 𝐶) → ¬ 𝐶 < 𝐵) ↔ ¬ ((𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶) ∧ 𝐶 < 𝐵)) |
20 | 18, 19 | bitr4i 278 |
. . . . . . . 8
⊢ (¬
(𝐶 ∈
ℝ* ∧ 𝐴
≤ 𝐶 ∧ 𝐶 < 𝐵) ↔ ((𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶) → ¬ 𝐶 < 𝐵)) |
21 | 16, 20 | sylib 217 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ ¬ 𝐶 ∈ (𝐴[,)𝐵)) → ((𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶) → ¬ 𝐶 < 𝐵)) |
22 | 21 | imp 408 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ ¬ 𝐶 ∈ (𝐴[,)𝐵)) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶)) → ¬ 𝐶 < 𝐵) |
23 | 10, 11, 7, 13, 22 | syl22anc 838 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ (𝐶 ∈ (𝐴[,]𝐵) ∧ ¬ 𝐶 ∈ (𝐴[,)𝐵))) → ¬ 𝐶 < 𝐵) |
24 | | xeqlelt 31733 |
. . . . . 6
⊢ ((𝐶 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐶 = 𝐵 ↔ (𝐶 ≤ 𝐵 ∧ ¬ 𝐶 < 𝐵))) |
25 | 24 | biimpar 479 |
. . . . 5
⊢ (((𝐶 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐶 ≤ 𝐵 ∧ ¬ 𝐶 < 𝐵)) → 𝐶 = 𝐵) |
26 | 7, 2, 9, 23, 25 | syl22anc 838 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ (𝐶 ∈ (𝐴[,]𝐵) ∧ ¬ 𝐶 ∈ (𝐴[,)𝐵))) → 𝐶 = 𝐵) |
27 | 26 | ex 414 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → ((𝐶 ∈ (𝐴[,]𝐵) ∧ ¬ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐶 = 𝐵)) |
28 | | pm5.6 1001 |
. . 3
⊢ (((𝐶 ∈ (𝐴[,]𝐵) ∧ ¬ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐶 = 𝐵) ↔ (𝐶 ∈ (𝐴[,]𝐵) → (𝐶 ∈ (𝐴[,)𝐵) ∨ 𝐶 = 𝐵))) |
29 | 27, 28 | sylib 217 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → (𝐶 ∈ (𝐴[,]𝐵) → (𝐶 ∈ (𝐴[,)𝐵) ∨ 𝐶 = 𝐵))) |
30 | | icossicc 13362 |
. . . . 5
⊢ (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵) |
31 | | simpr 486 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐶 ∈ (𝐴[,)𝐵)) |
32 | 30, 31 | sselid 3946 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐶 ∈ (𝐴[,]𝐵)) |
33 | | simpr 486 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝐶 = 𝐵) → 𝐶 = 𝐵) |
34 | | simpl2 1193 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝐶 = 𝐵) → 𝐵 ∈
ℝ*) |
35 | 33, 34 | eqeltrd 2834 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝐶 = 𝐵) → 𝐶 ∈
ℝ*) |
36 | | simpl3 1194 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝐶 = 𝐵) → 𝐴 ≤ 𝐵) |
37 | 36, 33 | breqtrrd 5137 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝐶 = 𝐵) → 𝐴 ≤ 𝐶) |
38 | 34 | xrleidd 13080 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝐶 = 𝐵) → 𝐵 ≤ 𝐵) |
39 | 33, 38 | eqbrtrd 5131 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝐶 = 𝐵) → 𝐶 ≤ 𝐵) |
40 | | simpl1 1192 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝐶 = 𝐵) → 𝐴 ∈
ℝ*) |
41 | 40, 34, 4 | syl2anc 585 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝐶 = 𝐵) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) |
42 | 35, 37, 39, 41 | mpbir3and 1343 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝐶 = 𝐵) → 𝐶 ∈ (𝐴[,]𝐵)) |
43 | 32, 42 | jaodan 957 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ (𝐶 ∈ (𝐴[,)𝐵) ∨ 𝐶 = 𝐵)) → 𝐶 ∈ (𝐴[,]𝐵)) |
44 | 43 | ex 414 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → ((𝐶 ∈ (𝐴[,)𝐵) ∨ 𝐶 = 𝐵) → 𝐶 ∈ (𝐴[,]𝐵))) |
45 | 29, 44 | impbid 211 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ (𝐴[,)𝐵) ∨ 𝐶 = 𝐵))) |