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 Th49;
then |.z1.| <= |.(z1 + z2).| + |.z2.| by Th69;
hence |.z1.| - |.z2.| <= |.(z1 + z2).| by XREAL_1:22; :: thesis: verum