Database
REAL AND COMPLEX NUMBERS
Order sets
Real number intervals
iccdili
Next ⟩
icccntr
Metamath Proof Explorer
Ascii
Unicode
Theorem
iccdili
Description:
Membership in a dilated interval.
(Contributed by
Jeff Madsen
, 2-Sep-2009)
Ref
Expression
Hypotheses
iccdili.1
⊢
A
∈
ℝ
iccdili.2
⊢
B
∈
ℝ
iccdili.3
⊢
R
∈
ℝ
+
iccdili.4
⊢
A
⁢
R
=
C
iccdili.5
⊢
B
⁢
R
=
D
Assertion
iccdili
⊢
X
∈
A
B
→
X
⁢
R
∈
C
D
Proof
Step
Hyp
Ref
Expression
1
iccdili.1
⊢
A
∈
ℝ
2
iccdili.2
⊢
B
∈
ℝ
3
iccdili.3
⊢
R
∈
ℝ
+
4
iccdili.4
⊢
A
⁢
R
=
C
5
iccdili.5
⊢
B
⁢
R
=
D
6
iccssre
⊢
A
∈
ℝ
∧
B
∈
ℝ
→
A
B
⊆
ℝ
7
1
2
6
mp2an
⊢
A
B
⊆
ℝ
8
7
sseli
⊢
X
∈
A
B
→
X
∈
ℝ
9
4
5
iccdil
⊢
A
∈
ℝ
∧
B
∈
ℝ
∧
X
∈
ℝ
∧
R
∈
ℝ
+
→
X
∈
A
B
↔
X
⁢
R
∈
C
D
10
1
2
9
mpanl12
⊢
X
∈
ℝ
∧
R
∈
ℝ
+
→
X
∈
A
B
↔
X
⁢
R
∈
C
D
11
3
10
mpan2
⊢
X
∈
ℝ
→
X
∈
A
B
↔
X
⁢
R
∈
C
D
12
11
biimpd
⊢
X
∈
ℝ
→
X
∈
A
B
→
X
⁢
R
∈
C
D
13
8
12
mpcom
⊢
X
∈
A
B
→
X
⁢
R
∈
C
D