Theorem icccntri

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

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

Proof

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