Proof of Theorem iccshftl
Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . . . 5
⊢ ((𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ) → 𝑋 ∈
ℝ) |
2 | | resubcl 11031 |
. . . . 5
⊢ ((𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑋 − 𝑅) ∈ ℝ) |
3 | 1, 2 | 2thd 268 |
. . . 4
⊢ ((𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑋 ∈ ℝ ↔ (𝑋 − 𝑅) ∈ ℝ)) |
4 | 3 | adantl 485 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ∈ ℝ ↔ (𝑋 − 𝑅) ∈ ℝ)) |
5 | | lesub1 11215 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝐴 ≤ 𝑋 ↔ (𝐴 − 𝑅) ≤ (𝑋 − 𝑅))) |
6 | 5 | 3expb 1121 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝐴 ≤ 𝑋 ↔ (𝐴 − 𝑅) ≤ (𝑋 − 𝑅))) |
7 | 6 | adantlr 715 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝐴 ≤ 𝑋 ↔ (𝐴 − 𝑅) ≤ (𝑋 − 𝑅))) |
8 | | iccshftl.1 |
. . . . 5
⊢ (𝐴 − 𝑅) = 𝐶 |
9 | 8 | breq1i 5038 |
. . . 4
⊢ ((𝐴 − 𝑅) ≤ (𝑋 − 𝑅) ↔ 𝐶 ≤ (𝑋 − 𝑅)) |
10 | 7, 9 | bitrdi 290 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝐴 ≤ 𝑋 ↔ 𝐶 ≤ (𝑋 − 𝑅))) |
11 | | lesub1 11215 |
. . . . . . 7
⊢ ((𝑋 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑋 ≤ 𝐵 ↔ (𝑋 − 𝑅) ≤ (𝐵 − 𝑅))) |
12 | 11 | 3expb 1121 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ≤ 𝐵 ↔ (𝑋 − 𝑅) ≤ (𝐵 − 𝑅))) |
13 | 12 | an12s 649 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ≤ 𝐵 ↔ (𝑋 − 𝑅) ≤ (𝐵 − 𝑅))) |
14 | 13 | adantll 714 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ≤ 𝐵 ↔ (𝑋 − 𝑅) ≤ (𝐵 − 𝑅))) |
15 | | iccshftl.2 |
. . . . 5
⊢ (𝐵 − 𝑅) = 𝐷 |
16 | 15 | breq2i 5039 |
. . . 4
⊢ ((𝑋 − 𝑅) ≤ (𝐵 − 𝑅) ↔ (𝑋 − 𝑅) ≤ 𝐷) |
17 | 14, 16 | bitrdi 290 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ≤ 𝐵 ↔ (𝑋 − 𝑅) ≤ 𝐷)) |
18 | 4, 10, 17 | 3anbi123d 1437 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → ((𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵) ↔ ((𝑋 − 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 − 𝑅) ∧ (𝑋 − 𝑅) ≤ 𝐷))) |
19 | | elicc2 12889 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵))) |
20 | 19 | adantr 484 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵))) |
21 | | resubcl 11031 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝐴 − 𝑅) ∈ ℝ) |
22 | 8, 21 | eqeltrrid 2839 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑅 ∈ ℝ) → 𝐶 ∈
ℝ) |
23 | | resubcl 11031 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝐵 − 𝑅) ∈ ℝ) |
24 | 15, 23 | eqeltrrid 2839 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ) → 𝐷 ∈
ℝ) |
25 | | elicc2 12889 |
. . . . 5
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑋 − 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 − 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 − 𝑅) ∧ (𝑋 − 𝑅) ≤ 𝐷))) |
26 | 22, 24, 25 | syl2an 599 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝑅 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → ((𝑋 − 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 − 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 − 𝑅) ∧ (𝑋 − 𝑅) ≤ 𝐷))) |
27 | 26 | anandirs 679 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑅 ∈ ℝ) → ((𝑋 − 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 − 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 − 𝑅) ∧ (𝑋 − 𝑅) ≤ 𝐷))) |
28 | 27 | adantrl 716 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → ((𝑋 − 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 − 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 − 𝑅) ∧ (𝑋 − 𝑅) ≤ 𝐷))) |
29 | 18, 20, 28 | 3bitr4d 314 |
1
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 − 𝑅) ∈ (𝐶[,]𝐷))) |