Metamath Proof Explorer

Theorem icoshft

Description: A shifted real is a member of a shifted, closed-below, open-above real interval. (Contributed by Paul Chapman, 25-Mar-2008)

Ref Expression
Assertion icoshft ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → X ∈ A B → X + C ∈ A + C B + C

Proof

Step Hyp Ref Expression
1 rexr ⊢ B ∈ ℝ → B ∈ ℝ *
2 elico2 ⊢ A ∈ ℝ ∧ B ∈ ℝ * → X ∈ A B ↔ X ∈ ℝ ∧ A ≤ X ∧ X < B
3 1 2 sylan2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → X ∈ A B ↔ X ∈ ℝ ∧ A ≤ X ∧ X < B
4 3 biimpd ⊢ A ∈ ℝ ∧ B ∈ ℝ → X ∈ A B → X ∈ ℝ ∧ A ≤ X ∧ X < B
5 4 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → X ∈ A B → X ∈ ℝ ∧ A ≤ X ∧ X < B
6 3anass ⊢ X ∈ ℝ ∧ A ≤ X ∧ X < B ↔ X ∈ ℝ ∧ A ≤ X ∧ X < B
7 5 6 syl6ib ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → X ∈ A B → X ∈ ℝ ∧ A ≤ X ∧ X < B
8 leadd1 ⊢ A ∈ ℝ ∧ X ∈ ℝ ∧ C ∈ ℝ → A ≤ X ↔ A + C ≤ X + C
9 8 3com12 ⊢ X ∈ ℝ ∧ A ∈ ℝ ∧ C ∈ ℝ → A ≤ X ↔ A + C ≤ X + C
10 9 3expib ⊢ X ∈ ℝ → A ∈ ℝ ∧ C ∈ ℝ → A ≤ X ↔ A + C ≤ X + C
11 10 com12 ⊢ A ∈ ℝ ∧ C ∈ ℝ → X ∈ ℝ → A ≤ X ↔ A + C ≤ X + C
12 11 3adant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → X ∈ ℝ → A ≤ X ↔ A + C ≤ X + C
13 12 imp ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ X ∈ ℝ → A ≤ X ↔ A + C ≤ X + C
14 ltadd1 ⊢ X ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → X < B ↔ X + C < B + C
15 14 3expib ⊢ X ∈ ℝ → B ∈ ℝ ∧ C ∈ ℝ → X < B ↔ X + C < B + C
16 15 com12 ⊢ B ∈ ℝ ∧ C ∈ ℝ → X ∈ ℝ → X < B ↔ X + C < B + C
17 16 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → X ∈ ℝ → X < B ↔ X + C < B + C
18 17 imp ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ X ∈ ℝ → X < B ↔ X + C < B + C
19 13 18 anbi12d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ X ∈ ℝ → A ≤ X ∧ X < B ↔ A + C ≤ X + C ∧ X + C < B + C
20 19 pm5.32da ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → X ∈ ℝ ∧ A ≤ X ∧ X < B ↔ X ∈ ℝ ∧ A + C ≤ X + C ∧ X + C < B + C
21 readdcl ⊢ X ∈ ℝ ∧ C ∈ ℝ → X + C ∈ ℝ
22 21 expcom ⊢ C ∈ ℝ → X ∈ ℝ → X + C ∈ ℝ
23 22 anim1d ⊢ C ∈ ℝ → X ∈ ℝ ∧ A + C ≤ X + C ∧ X + C < B + C → X + C ∈ ℝ ∧ A + C ≤ X + C ∧ X + C < B + C
24 3anass ⊢ X + C ∈ ℝ ∧ A + C ≤ X + C ∧ X + C < B + C ↔ X + C ∈ ℝ ∧ A + C ≤ X + C ∧ X + C < B + C
25 23 24 syl6ibr ⊢ C ∈ ℝ → X ∈ ℝ ∧ A + C ≤ X + C ∧ X + C < B + C → X + C ∈ ℝ ∧ A + C ≤ X + C ∧ X + C < B + C
26 25 3ad2ant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → X ∈ ℝ ∧ A + C ≤ X + C ∧ X + C < B + C → X + C ∈ ℝ ∧ A + C ≤ X + C ∧ X + C < B + C
27 readdcl ⊢ A ∈ ℝ ∧ C ∈ ℝ → A + C ∈ ℝ
28 27 3adant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + C ∈ ℝ
29 readdcl ⊢ B ∈ ℝ ∧ C ∈ ℝ → B + C ∈ ℝ
30 29 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B + C ∈ ℝ
31 rexr ⊢ B + C ∈ ℝ → B + C ∈ ℝ *
32 elico2 ⊢ A + C ∈ ℝ ∧ B + C ∈ ℝ * → X + C ∈ A + C B + C ↔ X + C ∈ ℝ ∧ A + C ≤ X + C ∧ X + C < B + C
33 31 32 sylan2 ⊢ A + C ∈ ℝ ∧ B + C ∈ ℝ → X + C ∈ A + C B + C ↔ X + C ∈ ℝ ∧ A + C ≤ X + C ∧ X + C < B + C
34 33 biimprd ⊢ A + C ∈ ℝ ∧ B + C ∈ ℝ → X + C ∈ ℝ ∧ A + C ≤ X + C ∧ X + C < B + C → X + C ∈ A + C B + C
35 28 30 34 syl2anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → X + C ∈ ℝ ∧ A + C ≤ X + C ∧ X + C < B + C → X + C ∈ A + C B + C
36 26 35 syld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → X ∈ ℝ ∧ A + C ≤ X + C ∧ X + C < B + C → X + C ∈ A + C B + C
37 20 36 sylbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → X ∈ ℝ ∧ A ≤ X ∧ X < B → X + C ∈ A + C B + C
38 7 37 syld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → X ∈ A B → X + C ∈ A + C B + C