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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝑋 ∈ ( 𝐴 [,) 𝐵 ) → ( 𝑋 + 𝐶 ) ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) )

Proof

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