Theorem iccshftri

Description: Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Hypotheses	iccshftri.1	⊢ 𝐴 ∈ ℝ
	iccshftri.2	⊢ 𝐵 ∈ ℝ
	iccshftri.3	⊢ 𝑅 ∈ ℝ
	iccshftri.4	⊢ ( 𝐴 + 𝑅 ) = 𝐶
	iccshftri.5	⊢ ( 𝐵 + 𝑅 ) = 𝐷
Assertion	iccshftri	⊢ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝑋 + 𝑅 ) ∈ ( 𝐶 [,] 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		iccshftri.1	⊢ 𝐴 ∈ ℝ
2		iccshftri.2	⊢ 𝐵 ∈ ℝ
3		iccshftri.3	⊢ 𝑅 ∈ ℝ
4		iccshftri.4	⊢ ( 𝐴 + 𝑅 ) = 𝐶
5		iccshftri.5	⊢ ( 𝐵 + 𝑅 ) = 𝐷
6		iccssre	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
7	1 2 6	mp2an	⊢ ( 𝐴 [,] 𝐵 ) ⊆ ℝ
8	7	sseli	⊢ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) → 𝑋 ∈ ℝ )
9	4 5	iccshftr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ ) ) → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑋 + 𝑅 ) ∈ ( 𝐶 [,] 𝐷 ) ) )
10	1 2 9	mpanl12	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑋 + 𝑅 ) ∈ ( 𝐶 [,] 𝐷 ) ) )
11	3 10	mpan2	⊢ ( 𝑋 ∈ ℝ → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑋 + 𝑅 ) ∈ ( 𝐶 [,] 𝐷 ) ) )
12	11	biimpd	⊢ ( 𝑋 ∈ ℝ → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝑋 + 𝑅 ) ∈ ( 𝐶 [,] 𝐷 ) ) )
13	8 12	mpcom	⊢ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝑋 + 𝑅 ) ∈ ( 𝐶 [,] 𝐷 ) )