Proof of Theorem icoshft
Step | Hyp | Ref
| Expression |
1 | | rexr 6868 |
. . . . . 6
⊢ (B ∈ ℝ →
B ∈
ℝ*) |
2 | | elico2 8576 |
. . . . . 6
⊢
((A ∈ ℝ ∧
B ∈
ℝ*) → (𝑋 ∈
(A[,)B)
↔ (𝑋 ∈ ℝ ∧
A ≤ 𝑋 ∧ 𝑋 < B))) |
3 | 1, 2 | sylan2 270 |
. . . . 5
⊢
((A ∈ ℝ ∧
B ∈
ℝ) → (𝑋 ∈ (A[,)B) ↔ (𝑋 ∈ ℝ
∧ A ≤
𝑋 ∧ 𝑋 < B))) |
4 | 3 | biimpd 132 |
. . . 4
⊢
((A ∈ ℝ ∧
B ∈
ℝ) → (𝑋 ∈ (A[,)B) → (𝑋 ∈ ℝ
∧ A ≤
𝑋 ∧ 𝑋 < B))) |
5 | 4 | 3adant3 923 |
. . 3
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → (𝑋 ∈ (A[,)B) → (𝑋 ∈ ℝ
∧ A ≤
𝑋 ∧ 𝑋 < B))) |
6 | | 3anass 888 |
. . 3
⊢ ((𝑋 ∈ ℝ ∧
A ≤ 𝑋 ∧ 𝑋 < B) ↔ (𝑋 ∈ ℝ
∧ (A ≤
𝑋 ∧ 𝑋 < B))) |
7 | 5, 6 | syl6ib 150 |
. 2
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → (𝑋 ∈ (A[,)B) → (𝑋 ∈ ℝ
∧ (A ≤
𝑋 ∧ 𝑋 < B)))) |
8 | | leadd1 7220 |
. . . . . . . . . 10
⊢
((A ∈ ℝ ∧ 𝑋 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (A ≤ 𝑋 ↔ (A + 𝐶) ≤ (𝑋 + 𝐶))) |
9 | 8 | 3com12 1107 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℝ ∧
A ∈
ℝ ∧ 𝐶 ∈
ℝ) → (A ≤ 𝑋 ↔ (A + 𝐶) ≤ (𝑋 + 𝐶))) |
10 | 9 | 3expib 1106 |
. . . . . . . 8
⊢ (𝑋 ∈ ℝ → ((A ∈ ℝ ∧ 𝐶 ∈
ℝ) → (A ≤ 𝑋 ↔ (A + 𝐶) ≤ (𝑋 + 𝐶)))) |
11 | 10 | com12 27 |
. . . . . . 7
⊢
((A ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑋 ∈ ℝ
→ (A ≤ 𝑋 ↔ (A + 𝐶) ≤ (𝑋 + 𝐶)))) |
12 | 11 | 3adant2 922 |
. . . . . 6
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → (𝑋 ∈ ℝ → (A ≤ 𝑋 ↔ (A + 𝐶) ≤ (𝑋 + 𝐶)))) |
13 | 12 | imp 115 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ 𝑋 ∈
ℝ) → (A ≤ 𝑋 ↔ (A + 𝐶) ≤ (𝑋 + 𝐶))) |
14 | | ltadd1 7219 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → (𝑋 <
B ↔ (𝑋 + 𝐶) < (B + 𝐶))) |
15 | 14 | 3expib 1106 |
. . . . . . . 8
⊢ (𝑋 ∈ ℝ → ((B ∈ ℝ ∧ 𝐶 ∈
ℝ) → (𝑋 <
B ↔ (𝑋 + 𝐶) < (B + 𝐶)))) |
16 | 15 | com12 27 |
. . . . . . 7
⊢
((B ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑋 ∈ ℝ
→ (𝑋 < B ↔ (𝑋 + 𝐶) < (B + 𝐶)))) |
17 | 16 | 3adant1 921 |
. . . . . 6
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → (𝑋 ∈ ℝ → (𝑋 < B
↔ (𝑋 + 𝐶) < (B + 𝐶)))) |
18 | 17 | imp 115 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ 𝑋 ∈
ℝ) → (𝑋 <
B ↔ (𝑋 + 𝐶) < (B + 𝐶))) |
19 | 13, 18 | anbi12d 442 |
. . . 4
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ 𝑋 ∈
ℝ) → ((A ≤ 𝑋 ∧ 𝑋 < B) ↔ ((A +
𝐶) ≤ (𝑋 + 𝐶) ∧ (𝑋 + 𝐶) < (B + 𝐶)))) |
20 | 19 | pm5.32da 425 |
. . 3
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → ((𝑋 ∈ ℝ ∧
(A ≤ 𝑋 ∧ 𝑋 < B)) ↔ (𝑋 ∈ ℝ
∧ ((A +
𝐶) ≤ (𝑋 + 𝐶) ∧ (𝑋 + 𝐶) < (B + 𝐶))))) |
21 | | readdcl 6805 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑋 + 𝐶) ∈
ℝ) |
22 | 21 | expcom 109 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ → (𝑋 ∈ ℝ
→ (𝑋 + 𝐶) ∈ ℝ)) |
23 | 22 | anim1d 319 |
. . . . . 6
⊢ (𝐶 ∈ ℝ → ((𝑋 ∈ ℝ
∧ ((A +
𝐶) ≤ (𝑋 + 𝐶) ∧ (𝑋 + 𝐶) < (B + 𝐶))) → ((𝑋 + 𝐶) ∈
ℝ ∧ ((A + 𝐶) ≤ (𝑋 + 𝐶) ∧ (𝑋 + 𝐶) < (B + 𝐶))))) |
24 | | 3anass 888 |
. . . . . 6
⊢ (((𝑋 + 𝐶) ∈
ℝ ∧ (A + 𝐶) ≤ (𝑋 + 𝐶) ∧ (𝑋 + 𝐶) < (B + 𝐶)) ↔ ((𝑋 + 𝐶) ∈
ℝ ∧ ((A + 𝐶) ≤ (𝑋 + 𝐶) ∧ (𝑋 + 𝐶) < (B + 𝐶)))) |
25 | 23, 24 | syl6ibr 151 |
. . . . 5
⊢ (𝐶 ∈ ℝ → ((𝑋 ∈ ℝ
∧ ((A +
𝐶) ≤ (𝑋 + 𝐶) ∧ (𝑋 + 𝐶) < (B + 𝐶))) → ((𝑋 + 𝐶) ∈
ℝ ∧ (A + 𝐶) ≤ (𝑋 + 𝐶) ∧ (𝑋 + 𝐶) < (B + 𝐶)))) |
26 | 25 | 3ad2ant3 926 |
. . . 4
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → ((𝑋 ∈ ℝ ∧
((A + 𝐶) ≤ (𝑋 + 𝐶) ∧ (𝑋 + 𝐶) < (B + 𝐶))) → ((𝑋 + 𝐶) ∈
ℝ ∧ (A + 𝐶) ≤ (𝑋 + 𝐶) ∧ (𝑋 + 𝐶) < (B + 𝐶)))) |
27 | | readdcl 6805 |
. . . . . 6
⊢
((A ∈ ℝ ∧ 𝐶 ∈ ℝ) → (A + 𝐶) ∈
ℝ) |
28 | 27 | 3adant2 922 |
. . . . 5
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → (A + 𝐶) ∈
ℝ) |
29 | | readdcl 6805 |
. . . . . 6
⊢
((B ∈ ℝ ∧ 𝐶 ∈ ℝ) → (B + 𝐶) ∈
ℝ) |
30 | 29 | 3adant1 921 |
. . . . 5
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → (B + 𝐶) ∈
ℝ) |
31 | | rexr 6868 |
. . . . . . 7
⊢
((B + 𝐶) ∈
ℝ → (B + 𝐶) ∈
ℝ*) |
32 | | elico2 8576 |
. . . . . . 7
⊢
(((A + 𝐶) ∈
ℝ ∧ (B + 𝐶) ∈
ℝ*) → ((𝑋 + 𝐶) ∈
((A + 𝐶)[,)(B +
𝐶)) ↔ ((𝑋 + 𝐶) ∈
ℝ ∧ (A + 𝐶) ≤ (𝑋 + 𝐶) ∧ (𝑋 + 𝐶) < (B + 𝐶)))) |
33 | 31, 32 | sylan2 270 |
. . . . . 6
⊢
(((A + 𝐶) ∈
ℝ ∧ (B + 𝐶) ∈
ℝ) → ((𝑋 + 𝐶) ∈ ((A + 𝐶)[,)(B + 𝐶)) ↔ ((𝑋 + 𝐶) ∈
ℝ ∧ (A + 𝐶) ≤ (𝑋 + 𝐶) ∧ (𝑋 + 𝐶) < (B + 𝐶)))) |
34 | 33 | biimprd 147 |
. . . . 5
⊢
(((A + 𝐶) ∈
ℝ ∧ (B + 𝐶) ∈
ℝ) → (((𝑋 +
𝐶) ∈ ℝ ∧
(A + 𝐶) ≤ (𝑋 + 𝐶) ∧ (𝑋 + 𝐶) < (B + 𝐶)) → (𝑋 + 𝐶) ∈
((A + 𝐶)[,)(B +
𝐶)))) |
35 | 28, 30, 34 | syl2anc 391 |
. . . 4
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → (((𝑋 +
𝐶) ∈ ℝ ∧
(A + 𝐶) ≤ (𝑋 + 𝐶) ∧ (𝑋 + 𝐶) < (B + 𝐶)) → (𝑋 + 𝐶) ∈
((A + 𝐶)[,)(B +
𝐶)))) |
36 | 26, 35 | syld 40 |
. . 3
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → ((𝑋 ∈ ℝ ∧
((A + 𝐶) ≤ (𝑋 + 𝐶) ∧ (𝑋 + 𝐶) < (B + 𝐶))) → (𝑋 + 𝐶) ∈
((A + 𝐶)[,)(B +
𝐶)))) |
37 | 20, 36 | sylbid 139 |
. 2
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → ((𝑋 ∈ ℝ ∧
(A ≤ 𝑋 ∧ 𝑋 < B)) → (𝑋 + 𝐶) ∈
((A + 𝐶)[,)(B +
𝐶)))) |
38 | 7, 37 | syld 40 |
1
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → (𝑋 ∈ (A[,)B) → (𝑋 + 𝐶) ∈
((A + 𝐶)[,)(B +
𝐶)))) |