Theorem iccdili

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

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

Proof

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