Metamath Proof Explorer


Theorem iccshftri

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

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

Proof

Step Hyp Ref Expression
1 iccshftri.1
 |-  A e. RR
2 iccshftri.2
 |-  B e. RR
3 iccshftri.3
 |-  R e. RR
4 iccshftri.4
 |-  ( A + R ) = C
5 iccshftri.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 iccshftr
 |-  ( ( ( 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 ) )