let a, b be non zero Real; :: thesis: ( ( |.(|.a.| - |.b.|).| = |.(a + b).| & |.(a - b).| = |.a.| + |.b.| ) iff ( not |.(|.a.| - |.b.|).| = |.(a - b).| or not |.(a + b).| = |.a.| + |.b.| ) )
A1: ( |.(|.a.| - |.b.|).| = |.(a + b).| iff |.(a - b).| = |.a.| + |.b.| ) by LmABS;
A2: ( |.(|.a.| - |.b.|).| = |.(a - b).| iff |.(a + b).| = |.a.| + |.b.| )

proof

reconsider c = - b as non zero Real ;
( |.(|.a.| - |.c.|).| = |.(a + c).| iff |.(a - c).| = |.a.| + |.c.| ) by LmABS;
hence ( |.(|.a.| - |.b.|).| = |.(a - b).| iff |.(a + b).| = |.a.| + |.b.| ) by COMPLEX1:52; :: thesis: verum

end;

( |.(a + b).| = |.a.| + |.b.| iff not |.(a - b).| = |.a.| + |.b.| )

proof

( (|.a.| - |.b.|) + 0 < (|.a.| - |.b.|) + (2 * |.b.|) & (|.b.| - |.a.|) + 0 < (|.b.| - |.a.|) + (2 * |.a.|) ) by XREAL_1:6;
then B0: ( |.a.| + |.b.| > |.a.| - |.b.| & |.a.| + |.b.| > - (|.a.| - |.b.|) ) ;

per cases ( |.(a + b).| = |.a.| + |.b.| or |.(a - b).| = |.a.| + |.b.| ) by ABS;

suppose |.(a + b).| = |.a.| + |.b.| ; :: thesis: ( |.(a + b).| = |.a.| + |.b.| iff not |.(a - b).| = |.a.| + |.b.| )

hence ( |.(a + b).| = |.a.| + |.b.| iff not |.(a - b).| = |.a.| + |.b.| ) by A2, B0, ABSVALUE:1; :: thesis: verum

end;

suppose |.(a - b).| = |.a.| + |.b.| ; :: thesis: ( |.(a + b).| = |.a.| + |.b.| iff not |.(a - b).| = |.a.| + |.b.| )

hence ( |.(a + b).| = |.a.| + |.b.| iff not |.(a - b).| = |.a.| + |.b.| ) by A1, B0, ABSVALUE:1; :: thesis: verum

end;

end;

end;

hence ( ( |.(|.a.| - |.b.|).| = |.(a + b).| & |.(a - b).| = |.a.| + |.b.| ) iff ( not |.(|.a.| - |.b.|).| = |.(a - b).| or not |.(a + b).| = |.a.| + |.b.| ) ) by LmABS, A2; :: thesis: verum