Step |
Hyp |
Ref |
Expression |
1 |
|
resubcl |
|- ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR ) |
2 |
|
abslt |
|- ( ( ( A - B ) e. RR /\ C e. RR ) -> ( ( abs ` ( A - B ) ) < C <-> ( -u C < ( A - B ) /\ ( A - B ) < C ) ) ) |
3 |
1 2
|
stoic3 |
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( abs ` ( A - B ) ) < C <-> ( -u C < ( A - B ) /\ ( A - B ) < C ) ) ) |
4 |
|
renegcl |
|- ( C e. RR -> -u C e. RR ) |
5 |
|
ltaddsub2 |
|- ( ( B e. RR /\ -u C e. RR /\ A e. RR ) -> ( ( B + -u C ) < A <-> -u C < ( A - B ) ) ) |
6 |
4 5
|
syl3an2 |
|- ( ( B e. RR /\ C e. RR /\ A e. RR ) -> ( ( B + -u C ) < A <-> -u C < ( A - B ) ) ) |
7 |
6
|
3comr |
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( B + -u C ) < A <-> -u C < ( A - B ) ) ) |
8 |
|
recn |
|- ( B e. RR -> B e. CC ) |
9 |
|
recn |
|- ( C e. RR -> C e. CC ) |
10 |
|
negsub |
|- ( ( B e. CC /\ C e. CC ) -> ( B + -u C ) = ( B - C ) ) |
11 |
8 9 10
|
syl2an |
|- ( ( B e. RR /\ C e. RR ) -> ( B + -u C ) = ( B - C ) ) |
12 |
11
|
3adant1 |
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B + -u C ) = ( B - C ) ) |
13 |
12
|
breq1d |
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( B + -u C ) < A <-> ( B - C ) < A ) ) |
14 |
7 13
|
bitr3d |
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( -u C < ( A - B ) <-> ( B - C ) < A ) ) |
15 |
|
ltsubadd2 |
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A - B ) < C <-> A < ( B + C ) ) ) |
16 |
14 15
|
anbi12d |
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( -u C < ( A - B ) /\ ( A - B ) < C ) <-> ( ( B - C ) < A /\ A < ( B + C ) ) ) ) |
17 |
3 16
|
bitrd |
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( abs ` ( A - B ) ) < C <-> ( ( B - C ) < A /\ A < ( B + C ) ) ) ) |