let a, b be Real; :: thesis: ( |.(|.a.| - |.b.|).| = |.(a + b).| iff |.(a - b).| = |.a.| + |.b.| )

per cases ( a >= 0 or a < 0 ) ;

suppose B1: a >= 0 ; :: thesis: ( |.(|.a.| - |.b.|).| = |.(a + b).| iff |.(a - b).| = |.a.| + |.b.| )

per cases ( b >= 0 or b < 0 ) ;

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

then ( |.a.| = a & |.b.| = b ) by B1, ABSVALUE:def 1;
hence ( |.(|.a.| - |.b.|).| = |.(a + b).| iff |.(a - b).| = |.a.| + |.b.| ) ; :: thesis: verum

end;

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

then ( |.a.| = a & |.b.| = - b ) by B1, ABSVALUE:def 1;
hence ( |.(|.a.| - |.b.|).| = |.(a + b).| iff |.(a - b).| = |.a.| + |.b.| ) ; :: thesis: verum

end;

end;

end;

suppose B1: a < 0 ; :: thesis: ( |.(|.a.| - |.b.|).| = |.(a + b).| iff |.(a - b).| = |.a.| + |.b.| )

per cases ( b >= 0 or b < 0 ) ;

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

then C1: ( |.a.| = - a & |.b.| = b ) by B1, ABSVALUE:def 1;
then C2: |.(|.a.| - |.b.|).| = |.(- (a + b)).| ;
|.(a - b).| = |.(- (|.a.| + |.b.|)).| by C1
.= |.(|.a.| + |.b.|).| by COMPLEX1:52 ;
hence ( |.(|.a.| - |.b.|).| = |.(a + b).| iff |.(a - b).| = |.a.| + |.b.| ) by C2, COMPLEX1:52; :: thesis: verum

end;

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

then C1: ( |.a.| = - a & |.b.| = - b ) by B1, ABSVALUE:def 1;
then C2: |.(|.a.| - |.b.|).| = |.(- (a - b)).| ;
|.(a + b).| = |.(- (|.a.| + |.b.|)).| by C1
.= |.(|.a.| + |.b.|).| by COMPLEX1:52 ;
hence ( |.(|.a.| - |.b.|).| = |.(a + b).| iff |.(a - b).| = |.a.| + |.b.| ) by COMPLEX1:52, C2; :: thesis: verum

end;

end;

end;

end;