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

Metamath Proof Explorer

Theorem icoshft

Proof