HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem abs3lemt 4865
Description: Lemma involving absolute value of differences.
Assertion
Ref Expression
abs3lemt |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. RR)) -> (((abs` (A - C)) < (D / 2) /\ (abs` (C - B)) < (D / 2)) -> (abs` (A - B)) < D))
Proof of Theorem abs3lemt
StepHypRef Expression
1 opreq1 3006 . . . . . 6 |- (A = if(A e. CC, A, 0) -> (A - C) = (if(A e. CC, A, 0) - C))
21fveq2d 2836 . . . . 5 |- (A = if(A e. CC, A, 0) -> (abs` (A - C)) = (abs` (if(A e. CC, A, 0) - C)))
32breq1d 2071 . . . 4 |- (A = if(A e. CC, A, 0) -> ((abs` (A - C)) < (D / 2) <-> (abs` (if(A e. CC, A, 0) - C)) < (D / 2)))
43anbi1d 469 . . 3 |- (A = if(A e. CC, A, 0) -> (((abs` (A - C)) < (D / 2) /\ (abs` (C - B)) < (D / 2)) <-> ((abs` (if(A e. CC, A, 0) - C)) < (D / 2) /\ (abs` (C - B)) < (D / 2))))
5 opreq1 3006 . . . . 5 |- (A = if(A e. CC, A, 0) -> (A - B) = (if(A e. CC, A, 0) - B))
65fveq2d 2836 . . . 4 |- (A = if(A e. CC, A, 0) -> (abs` (A - B)) = (abs` (if(A e. CC, A, 0) - B)))
76breq1d 2071 . . 3 |- (A = if(A e. CC, A, 0) -> ((abs` (A - B)) < D <-> (abs` (if(A e. CC, A, 0) - B)) < D))
84, 7imbi12d 474 . 2 |- (A = if(A e. CC, A, 0) -> ((((abs` (A - C)) < (D / 2) /\ (abs` (C - B)) < (D / 2)) -> (abs` (A - B)) < D) <-> (((abs` (if(A e. CC, A, 0) - C)) < (D / 2) /\ (abs` (C - B)) < (D / 2)) -> (abs` (if(A e. CC, A, 0) - B)) < D)))
9 opreq2 3007 . . . . . 6 |- (B = if(B e. CC, B, 0) -> (C - B) = (C - if(B e. CC, B, 0)))
109fveq2d 2836 . . . . 5 |- (B = if(B e. CC, B, 0) -> (abs` (C - B)) = (abs` (C - if(B e. CC, B, 0))))
1110breq1d 2071 . . . 4 |- (B = if(B e. CC, B, 0) -> ((abs` (C - B)) < (D / 2) <-> (abs` (C - if(B e. CC, B, 0))) < (D / 2)))
1211anbi2d 468 . . 3 |- (B = if(B e. CC, B, 0) -> (((abs` (if(A e. CC, A, 0) - C)) < (D / 2) /\ (abs` (C - B)) < (D / 2)) <-> ((abs` (if(A e. CC, A, 0) - C)) < (D / 2) /\ (abs` (C - if(B e. CC, B, 0))) < (D / 2))))
13 opreq2 3007 . . . . 5 |- (B = if(B e. CC, B, 0) -> (if(A e. CC, A, 0) - B) = (if(A e. CC, A, 0) - if(B e. CC, B, 0)))
1413fveq2d 2836 . . . 4 |- (B = if(B e. CC, B, 0) -> (abs` (if(A e. CC, A, 0) - B)) = (abs` (if(A e. CC, A, 0) - if(B e. CC, B, 0))))
1514breq1d 2071 . . 3 |- (B = if(B e. CC, B, 0) -> ((abs` (if(A e. CC, A, 0) - B)) < D <-> (abs` (if(A e. CC, A, 0) - if(B e. CC, B, 0))) < D))
1612, 15imbi12d 474 . 2 |- (B = if(B e. CC, B, 0) -> ((((abs` (if(A e. CC, A, 0) - C)) < (D / 2) /\ (abs` (C - B)) < (D / 2)) -> (abs` (if(A e. CC, A, 0) - B)) < D) <-> (((abs` (if(A e. CC, A, 0) - C)) < (D / 2) /\ (abs` (C - if(B e. CC, B, 0))) < (D / 2)) -> (abs` (if(A e. CC, A, 0) - if(B e. CC, B, 0))) < D)))
17 opreq2 3007 . . . . . 6 |- (C = if(C e. CC, C, 0) -> (if(A e. CC, A, 0) - C) = (if(A e. CC, A, 0) - if(C e. CC, C, 0)))
1817fveq2d 2836 . . . . 5 |- (C = if(C e. CC, C, 0) -> (abs` (if(A e. CC, A, 0) - C)) = (abs` (if(A e. CC, A, 0) - if(C e. CC, C, 0))))
1918breq1d 2071 . . . 4 |- (C = if(C e. CC, C, 0) -> ((abs` (if(A e. CC, A, 0) - C)) < (D / 2) <-> (abs` (if(A e. CC, A, 0) - if(C e. CC, C, 0))) < (D / 2)))
20 opreq1 3006 . . . . . 6 |- (C = if(C e. CC, C, 0) -> (C - if(B e. CC, B, 0)) = (if(C e. CC, C, 0) - if(B e. CC, B, 0)))
2120fveq2d 2836 . . . . 5 |- (C = if(C e. CC, C, 0) -> (abs` (C - if(B e. CC, B, 0))) = (abs` (if(C e. CC, C, 0) - if(B e. CC, B, 0))))
2221breq1d 2071 . . . 4 |- (C = if(C e. CC, C, 0) -> ((abs` (C - if(B e. CC, B, 0))) < (D / 2) <-> (abs` (if(C e. CC, C, 0) - if(B e. CC, B, 0))) < (D / 2)))
2319, 22anbi12d 476 . . 3 |- (C = if(C e. CC, C, 0) -> (((abs` (if(A e. CC, A, 0) - C)) < (D / 2) /\ (abs` (C - if(B e. CC, B, 0))) < (D / 2)) <-> ((abs` (if(A e. CC, A, 0) - if(C e. CC, C, 0))) < (D / 2) /\ (abs` (if(C e. CC, C, 0) - if(B e. CC, B, 0))) < (D / 2))))
2423imbi1d 465 . 2 |- (C = if(C e. CC, C, 0) -> ((((abs` (if(A e. CC, A, 0) - C)) < (D / 2) /\ (abs` (C - if(B e. CC, B, 0))) < (D / 2)) -> (abs` (if(A e. CC, A, 0) - if(B e. CC, B, 0))) < D) <-> (((abs` (if(A e. CC, A, 0) - if(C e. CC, C, 0))) < (D / 2) /\ (abs` (if(C e. CC, C, 0) - if(B e. CC, B, 0))) < (D / 2)) -> (abs` (if(A e. CC, A, 0) - if(B e. CC, B, 0))) < D)))
25 opreq1 3006 . . . . 5 |- (D = if(D e. RR, D, 0) -> (D / 2) = (if(D e. RR, D, 0) / 2))
2625breq2d 2072 . . . 4 |- (D = if(D e. RR, D, 0) -> ((abs` (if(A e. CC, A, 0) - if(C e. CC, C, 0))) < (D / 2) <-> (abs` (if(A e. CC, A, 0) - if(C e. CC, C, 0))) < (if(D e. RR, D, 0) / 2)))
2725breq2d 2072 . . . 4 |- (D = if(D e. RR, D, 0) -> ((abs` (if(C e. CC, C, 0) - if(B e. CC, B, 0))) < (D / 2) <-> (abs` (if(C e. CC, C, 0) - if(B e. CC, B, 0))) < (if(D e. RR, D, 0) / 2)))
2826, 27anbi12d 476 . . 3 |- (D = if(D e. RR, D, 0) -> (((abs` (if(A e. CC, A, 0) - if(C e. CC, C, 0))) < (D / 2) /\ (abs` (if(C e. CC, C, 0) - if(B e. CC, B, 0))