let n be Element of NAT ; :: thesis: for z1, z2 being Element of COMPLEX n holds |.z1.| - |.z2.| <= |.(z1 + z2).|
let z1, z2 be Element of COMPLEX n; :: thesis: |.z1.| - |.z2.| <= |.(z1 + z2).|
z1 = (z1 + z2) - z2 by Th96;
then |.z1.| <= |.(z1 + z2).| + |.z2.| by Th116;
hence |.z1.| - |.z2.| <= |.(z1 + z2).| by XREAL_1:20; :: thesis: verum