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 ) )