Proof of Theorem iccshftr
Step | Hyp | Ref
| Expression |
1 | | simpl 102 |
. . . . 5
⊢ ((𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ) → 𝑋 ∈
ℝ) |
2 | | readdcl 6805 |
. . . . 5
⊢ ((𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑋 + 𝑅) ∈
ℝ) |
3 | 1, 2 | 2thd 164 |
. . . 4
⊢ ((𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑋 ∈ ℝ
↔ (𝑋 + 𝑅) ∈ ℝ)) |
4 | 3 | adantl 262 |
. . 3
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝑋 ∈ ℝ
∧ 𝑅 ∈
ℝ)) → (𝑋 ∈ ℝ ↔ (𝑋 + 𝑅) ∈
ℝ)) |
5 | | leadd1 7220 |
. . . . . 6
⊢
((A ∈ ℝ ∧ 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (A ≤ 𝑋 ↔ (A + 𝑅) ≤ (𝑋 + 𝑅))) |
6 | 5 | 3expb 1104 |
. . . . 5
⊢
((A ∈ ℝ ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (A ≤ 𝑋 ↔ (A + 𝑅) ≤ (𝑋 + 𝑅))) |
7 | 6 | adantlr 446 |
. . . 4
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝑋 ∈ ℝ
∧ 𝑅 ∈
ℝ)) → (A ≤ 𝑋 ↔ (A + 𝑅) ≤ (𝑋 + 𝑅))) |
8 | | iccshftr.1 |
. . . . 5
⊢ (A + 𝑅) = 𝐶 |
9 | 8 | breq1i 3762 |
. . . 4
⊢
((A + 𝑅) ≤ (𝑋 + 𝑅) ↔ 𝐶 ≤ (𝑋 + 𝑅)) |
10 | 7, 9 | syl6bb 185 |
. . 3
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝑋 ∈ ℝ
∧ 𝑅 ∈
ℝ)) → (A ≤ 𝑋 ↔ 𝐶 ≤ (𝑋 + 𝑅))) |
11 | | leadd1 7220 |
. . . . . . 7
⊢ ((𝑋 ∈ ℝ ∧
B ∈
ℝ ∧ 𝑅 ∈
ℝ) → (𝑋 ≤
B ↔ (𝑋 + 𝑅) ≤ (B + 𝑅))) |
12 | 11 | 3expb 1104 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ ∧
(B ∈
ℝ ∧ 𝑅 ∈
ℝ)) → (𝑋 ≤
B ↔ (𝑋 + 𝑅) ≤ (B + 𝑅))) |
13 | 12 | an12s 499 |
. . . . 5
⊢
((B ∈ ℝ ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ≤ B
↔ (𝑋 + 𝑅) ≤ (B + 𝑅))) |
14 | 13 | adantll 445 |
. . . 4
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝑋 ∈ ℝ
∧ 𝑅 ∈
ℝ)) → (𝑋 ≤
B ↔ (𝑋 + 𝑅) ≤ (B + 𝑅))) |
15 | | iccshftr.2 |
. . . . 5
⊢ (B + 𝑅) = 𝐷 |
16 | 15 | breq2i 3763 |
. . . 4
⊢ ((𝑋 + 𝑅) ≤ (B + 𝑅) ↔ (𝑋 + 𝑅) ≤ 𝐷) |
17 | 14, 16 | syl6bb 185 |
. . 3
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝑋 ∈ ℝ
∧ 𝑅 ∈
ℝ)) → (𝑋 ≤
B ↔ (𝑋 + 𝑅) ≤ 𝐷)) |
18 | 4, 10, 17 | 3anbi123d 1206 |
. 2
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝑋 ∈ ℝ
∧ 𝑅 ∈
ℝ)) → ((𝑋 ∈ ℝ ∧
A ≤ 𝑋 ∧ 𝑋 ≤ B) ↔ ((𝑋 + 𝑅) ∈
ℝ ∧ 𝐶 ≤ (𝑋 + 𝑅) ∧ (𝑋 + 𝑅) ≤ 𝐷))) |
19 | | elicc2 8577 |
. . 3
⊢
((A ∈ ℝ ∧
B ∈
ℝ) → (𝑋 ∈ (A[,]B) ↔ (𝑋 ∈ ℝ
∧ A ≤
𝑋 ∧ 𝑋 ≤ B))) |
20 | 19 | adantr 261 |
. 2
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝑋 ∈ ℝ
∧ 𝑅 ∈
ℝ)) → (𝑋 ∈ (A[,]B) ↔ (𝑋 ∈ ℝ
∧ A ≤
𝑋 ∧ 𝑋 ≤ B))) |
21 | | readdcl 6805 |
. . . . . 6
⊢
((A ∈ ℝ ∧ 𝑅 ∈ ℝ) → (A + 𝑅) ∈
ℝ) |
22 | 8, 21 | syl5eqelr 2122 |
. . . . 5
⊢
((A ∈ ℝ ∧ 𝑅 ∈ ℝ) → 𝐶 ∈
ℝ) |
23 | | readdcl 6805 |
. . . . . 6
⊢
((B ∈ ℝ ∧ 𝑅 ∈ ℝ) → (B + 𝑅) ∈
ℝ) |
24 | 15, 23 | syl5eqelr 2122 |
. . . . 5
⊢
((B ∈ ℝ ∧ 𝑅 ∈ ℝ) → 𝐷 ∈
ℝ) |
25 | | elicc2 8577 |
. . . . 5
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑋 + 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 + 𝑅) ∈
ℝ ∧ 𝐶 ≤ (𝑋 + 𝑅) ∧ (𝑋 + 𝑅) ≤ 𝐷))) |
26 | 22, 24, 25 | syl2an 273 |
. . . 4
⊢
(((A ∈ ℝ ∧ 𝑅 ∈ ℝ) ∧
(B ∈
ℝ ∧ 𝑅 ∈
ℝ)) → ((𝑋 +
𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 + 𝑅) ∈
ℝ ∧ 𝐶 ≤ (𝑋 + 𝑅) ∧ (𝑋 + 𝑅) ≤ 𝐷))) |
27 | 26 | anandirs 527 |
. . 3
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ 𝑅 ∈
ℝ) → ((𝑋 + 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 + 𝑅) ∈
ℝ ∧ 𝐶 ≤ (𝑋 + 𝑅) ∧ (𝑋 + 𝑅) ≤ 𝐷))) |
28 | 27 | adantrl 447 |
. 2
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝑋 ∈ ℝ
∧ 𝑅 ∈
ℝ)) → ((𝑋 +
𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 + 𝑅) ∈
ℝ ∧ 𝐶 ≤ (𝑋 + 𝑅) ∧ (𝑋 + 𝑅) ≤ 𝐷))) |
29 | 18, 20, 28 | 3bitr4d 209 |
1
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝑋 ∈ ℝ
∧ 𝑅 ∈
ℝ)) → (𝑋 ∈ (A[,]B) ↔ (𝑋 + 𝑅) ∈ (𝐶[,]𝐷))) |