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∈AB→X+C∈A+CB+C

Proof

Step Hyp Ref Expression
1 rexr ⊢B∈ℝ→B∈ℝ*
2 elico2 ⊢A∈ℝ∧B∈ℝ*→X∈AB↔X∈ℝ∧A≤X∧X<B
3 1 2 sylan2 ⊢A∈ℝ∧B∈ℝ→X∈AB↔X∈ℝ∧A≤X∧X<B
4 3 biimpd ⊢A∈ℝ∧B∈ℝ→X∈AB→X∈ℝ∧A≤X∧X<B
5 4 3adant3 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→X∈AB→X∈ℝ∧A≤X∧X<B
6 3anass ⊢X∈ℝ∧A≤X∧X<B↔X∈ℝ∧A≤X∧X<B
7 5 6 imbitrdi ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→X∈AB→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 imbitrrdi ⊢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+CB+C↔X+C∈ℝ∧A+C≤X+C∧X+C<B+C
33 31 32 sylan2 ⊢A+C∈ℝ∧B+C∈ℝ→X+C∈A+CB+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+CB+C
35 28 30 34 syl2anc ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→X+C∈ℝ∧A+C≤X+C∧X+C<B+C→X+C∈A+CB+C
36 26 35 syld ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→X∈ℝ∧A+C≤X+C∧X+C<B+C→X+C∈A+CB+C
37 20 36 sylbid ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→X∈ℝ∧A≤X∧X<B→X+C∈A+CB+C
38 7 37 syld ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→X∈AB→X+C∈A+CB+C