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

Metamath Proof Explorer

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