This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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