Theorem iccshftli

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

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

Proof

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