Proof of Theorem iooshf
Step | Hyp | Ref
| Expression |
1 | | ltaddsub 7226 |
. . . . . 6
⊢ ((𝐶 ∈ ℝ ∧
B ∈
ℝ ∧ A ∈ ℝ)
→ ((𝐶 + B) < A ↔
𝐶 < (A − B))) |
2 | 1 | 3com13 1108 |
. . . . 5
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → ((𝐶 +
B) < A ↔ 𝐶 < (A
− B))) |
3 | 2 | 3expa 1103 |
. . . 4
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ 𝐶 ∈
ℝ) → ((𝐶 +
B) < A ↔ 𝐶 < (A
− B))) |
4 | 3 | adantrr 448 |
. . 3
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → ((𝐶 +
B) < A ↔ 𝐶 < (A
− B))) |
5 | | ltsubadd 7222 |
. . . . . 6
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐷 ∈
ℝ) → ((A − B) < 𝐷 ↔ A < (𝐷 + B))) |
6 | 5 | bicomd 129 |
. . . . 5
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐷 ∈
ℝ) → (A < (𝐷 + B)
↔ (A − B) < 𝐷)) |
7 | 6 | 3expa 1103 |
. . . 4
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ 𝐷 ∈
ℝ) → (A < (𝐷 + B)
↔ (A − B) < 𝐷)) |
8 | 7 | adantrl 447 |
. . 3
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → (A < (𝐷 + B)
↔ (A − B) < 𝐷)) |
9 | 4, 8 | anbi12d 442 |
. 2
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → (((𝐶 +
B) < A ∧ A < (𝐷 + B))
↔ (𝐶 < (A − B)
∧ (A
− B) < 𝐷))) |
10 | | readdcl 6805 |
. . . . . 6
⊢ ((𝐶 ∈ ℝ ∧
B ∈
ℝ) → (𝐶 +
B) ∈
ℝ) |
11 | 10 | rexrd 6872 |
. . . . 5
⊢ ((𝐶 ∈ ℝ ∧
B ∈
ℝ) → (𝐶 +
B) ∈
ℝ*) |
12 | 11 | ad2ant2rl 480 |
. . . 4
⊢ (((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧
(A ∈
ℝ ∧ B ∈ ℝ))
→ (𝐶 + B) ∈
ℝ*) |
13 | | readdcl 6805 |
. . . . . 6
⊢ ((𝐷 ∈ ℝ ∧
B ∈
ℝ) → (𝐷 +
B) ∈
ℝ) |
14 | 13 | rexrd 6872 |
. . . . 5
⊢ ((𝐷 ∈ ℝ ∧
B ∈
ℝ) → (𝐷 +
B) ∈
ℝ*) |
15 | 14 | ad2ant2l 477 |
. . . 4
⊢ (((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧
(A ∈
ℝ ∧ B ∈ ℝ))
→ (𝐷 + B) ∈
ℝ*) |
16 | | rexr 6868 |
. . . . 5
⊢ (A ∈ ℝ →
A ∈
ℝ*) |
17 | 16 | ad2antrl 459 |
. . . 4
⊢ (((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧
(A ∈
ℝ ∧ B ∈ ℝ))
→ A ∈ ℝ*) |
18 | | elioo5 8572 |
. . . 4
⊢ (((𝐶 + B) ∈
ℝ* ∧ (𝐷 + B)
∈ ℝ* ∧ A ∈ ℝ*) → (A ∈ ((𝐶 + B)(,)(𝐷 + B))
↔ ((𝐶 + B) < A ∧ A < (𝐷 + B)))) |
19 | 12, 15, 17, 18 | syl3anc 1134 |
. . 3
⊢ (((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧
(A ∈
ℝ ∧ B ∈ ℝ))
→ (A ∈ ((𝐶 + B)(,)(𝐷 + B))
↔ ((𝐶 + B) < A ∧ A < (𝐷 + B)))) |
20 | 19 | ancoms 255 |
. 2
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → (A ∈ ((𝐶 + B)(,)(𝐷 + B))
↔ ((𝐶 + B) < A ∧ A < (𝐷 + B)))) |
21 | | rexr 6868 |
. . . 4
⊢ (𝐶 ∈ ℝ → 𝐶 ∈
ℝ*) |
22 | 21 | ad2antrl 459 |
. . 3
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → 𝐶 ∈ ℝ*) |
23 | | rexr 6868 |
. . . 4
⊢ (𝐷 ∈ ℝ → 𝐷 ∈
ℝ*) |
24 | 23 | ad2antll 460 |
. . 3
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → 𝐷 ∈ ℝ*) |
25 | | resubcl 7071 |
. . . . 5
⊢
((A ∈ ℝ ∧
B ∈
ℝ) → (A − B) ∈
ℝ) |
26 | 25 | rexrd 6872 |
. . . 4
⊢
((A ∈ ℝ ∧
B ∈
ℝ) → (A − B) ∈
ℝ*) |
27 | 26 | adantr 261 |
. . 3
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → (A − B) ∈
ℝ*) |
28 | | elioo5 8572 |
. . 3
⊢ ((𝐶 ∈ ℝ* ∧ 𝐷 ∈
ℝ* ∧ (A − B)
∈ ℝ*) → ((A − B)
∈ (𝐶(,)𝐷) ↔ (𝐶 < (A
− B) ∧ (A −
B) < 𝐷))) |
29 | 22, 24, 27, 28 | syl3anc 1134 |
. 2
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → ((A − B) ∈ (𝐶(,)𝐷) ↔ (𝐶 < (A
− B) ∧ (A −
B) < 𝐷))) |
30 | 9, 20, 29 | 3bitr4rd 210 |
1
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → ((A − B) ∈ (𝐶(,)𝐷) ↔ A ∈ ((𝐶 + B)(,)(𝐷 + B)))) |