Metamath Proof Explorer


Theorem elicc4abs

Description: Membership in a symmetric closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Assertion elicc4abs
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C e. ( ( A - B ) [,] ( A + B ) ) <-> ( abs ` ( C - A ) ) <_ B ) )

Proof

Step Hyp Ref Expression
1 resubcl
 |-  ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR )
2 1 3adant3
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A - B ) e. RR )
3 2 rexrd
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A - B ) e. RR* )
4 readdcl
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
5 4 3adant3
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A + B ) e. RR )
6 5 rexrd
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A + B ) e. RR* )
7 rexr
 |-  ( C e. RR -> C e. RR* )
8 7 3ad2ant3
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. RR* )
9 elicc4
 |-  ( ( ( A - B ) e. RR* /\ ( A + B ) e. RR* /\ C e. RR* ) -> ( C e. ( ( A - B ) [,] ( A + B ) ) <-> ( ( A - B ) <_ C /\ C <_ ( A + B ) ) ) )
10 3 6 8 9 syl3anc
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C e. ( ( A - B ) [,] ( A + B ) ) <-> ( ( A - B ) <_ C /\ C <_ ( A + B ) ) ) )
11 absdifle
 |-  ( ( C e. RR /\ A e. RR /\ B e. RR ) -> ( ( abs ` ( C - A ) ) <_ B <-> ( ( A - B ) <_ C /\ C <_ ( A + B ) ) ) )
12 11 3coml
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( abs ` ( C - A ) ) <_ B <-> ( ( A - B ) <_ C /\ C <_ ( A + B ) ) ) )
13 10 12 bitr4d
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C e. ( ( A - B ) [,] ( A + B ) ) <-> ( abs ` ( C - A ) ) <_ B ) )