Proof of Theorem elico2
Step | Hyp | Ref
| Expression |
1 | | rexr 7925 |
. . 3
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) |
2 | | elico1 9833 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵))) |
3 | 1, 2 | sylan 281 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵))) |
4 | | mnfxr 7936 |
. . . . . . . 8
⊢ -∞
∈ ℝ* |
5 | 4 | a1i 9 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
∧ (𝐶 ∈
ℝ* ∧ 𝐴
≤ 𝐶 ∧ 𝐶 < 𝐵)) → -∞ ∈
ℝ*) |
6 | 1 | ad2antrr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
∧ (𝐶 ∈
ℝ* ∧ 𝐴
≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐴 ∈
ℝ*) |
7 | | simpr1 988 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
∧ (𝐶 ∈
ℝ* ∧ 𝐴
≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐶 ∈
ℝ*) |
8 | | mnflt 9696 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → -∞
< 𝐴) |
9 | 8 | ad2antrr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
∧ (𝐶 ∈
ℝ* ∧ 𝐴
≤ 𝐶 ∧ 𝐶 < 𝐵)) → -∞ < 𝐴) |
10 | | simpr2 989 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
∧ (𝐶 ∈
ℝ* ∧ 𝐴
≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐴 ≤ 𝐶) |
11 | 5, 6, 7, 9, 10 | xrltletrd 9721 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
∧ (𝐶 ∈
ℝ* ∧ 𝐴
≤ 𝐶 ∧ 𝐶 < 𝐵)) → -∞ < 𝐶) |
12 | | simplr 520 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
∧ (𝐶 ∈
ℝ* ∧ 𝐴
≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐵 ∈
ℝ*) |
13 | | pnfxr 7932 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
14 | 13 | a1i 9 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
∧ (𝐶 ∈
ℝ* ∧ 𝐴
≤ 𝐶 ∧ 𝐶 < 𝐵)) → +∞ ∈
ℝ*) |
15 | | simpr3 990 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
∧ (𝐶 ∈
ℝ* ∧ 𝐴
≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐶 < 𝐵) |
16 | | pnfge 9702 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ*
→ 𝐵 ≤
+∞) |
17 | 16 | ad2antlr 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
∧ (𝐶 ∈
ℝ* ∧ 𝐴
≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐵 ≤ +∞) |
18 | 7, 12, 14, 15, 17 | xrltletrd 9721 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
∧ (𝐶 ∈
ℝ* ∧ 𝐴
≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐶 < +∞) |
19 | | xrrebnd 9729 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ*
→ (𝐶 ∈ ℝ
↔ (-∞ < 𝐶
∧ 𝐶 <
+∞))) |
20 | 7, 19 | syl 14 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
∧ (𝐶 ∈
ℝ* ∧ 𝐴
≤ 𝐶 ∧ 𝐶 < 𝐵)) → (𝐶 ∈ ℝ ↔ (-∞ < 𝐶 ∧ 𝐶 < +∞))) |
21 | 11, 18, 20 | mpbir2and 929 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
∧ (𝐶 ∈
ℝ* ∧ 𝐴
≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐶 ∈ ℝ) |
22 | 21, 10, 15 | 3jca 1162 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
∧ (𝐶 ∈
ℝ* ∧ 𝐴
≤ 𝐶 ∧ 𝐶 < 𝐵)) → (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) |
23 | 22 | ex 114 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
→ ((𝐶 ∈
ℝ* ∧ 𝐴
≤ 𝐶 ∧ 𝐶 < 𝐵) → (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵))) |
24 | | rexr 7925 |
. . . 4
⊢ (𝐶 ∈ ℝ → 𝐶 ∈
ℝ*) |
25 | 24 | 3anim1i 1168 |
. . 3
⊢ ((𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵) → (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) |
26 | 23, 25 | impbid1 141 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
→ ((𝐶 ∈
ℝ* ∧ 𝐴
≤ 𝐶 ∧ 𝐶 < 𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵))) |
27 | 3, 26 | bitrd 187 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵))) |