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

Metamath Proof Explorer

Theorem icccntri

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

Ref Expression
Hypotheses icccntri.1 
|- A e. RR
icccntri.2 
|- B e. RR
icccntri.3 
|- R e. RR+
icccntri.4 
|- ( A / R ) = C
icccntri.5 
|- ( B / R ) = D
Assertion icccntri 
|- ( X e. ( A [,] B ) -> ( X / R ) e. ( C [,] D ) )

Proof

Step Hyp Ref Expression
1 icccntri.1 
 |-  A e. RR
2 icccntri.2 
 |-  B e. RR
3 icccntri.3 
 |-  R e. RR+
4 icccntri.4 
 |-  ( A / R ) = C
5 icccntri.5 
 |-  ( B / R ) = D
6 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
7 1 2 6 mp2an 
 |-  ( A [,] B ) C_ RR
8 7 sseli 
 |-  ( X e. ( A [,] B ) -> X e. RR )
9 4 5 icccntr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ R e. RR+ ) ) -> ( X e. ( A [,] B ) <-> ( X / R ) e. ( C [,] D ) ) )
10 1 2 9 mpanl12 
 |-  ( ( X e. RR /\ R e. RR+ ) -> ( X e. ( A [,] B ) <-> ( X / R ) e. ( C [,] D ) ) )
11 3 10 mpan2 
 |-  ( X e. RR -> ( X e. ( A [,] B ) <-> ( X / R ) e. ( C [,] D ) ) )
12 11 biimpd 
 |-  ( X e. RR -> ( X e. ( A [,] B ) -> ( X / R ) e. ( C [,] D ) ) )
13 8 12 mpcom 
 |-  ( X e. ( A [,] B ) -> ( X / R ) e. ( C [,] D ) )