Metamath Proof Explorer


Table of Contents - 21.38.4.35. Additions for square root; absolute value

This is based on the observation that the real and imaginary parts of a complex number can be calculated from the number's absolute and real part and the sign of its imaginary part.

Formalization of the formula in sqrtcval was motivated by a short <A HREF="https://www.youtube.com/watch?v=QAhWTQ4Ravw">Michael Penn video</A>.

  1. sqrtcvallem1
  2. reabsifneg
  3. reabsifnpos
  4. reabsifpos
  5. reabsifnneg
  6. reabssgn
  7. sqrtcvallem2
  8. sqrtcvallem3
  9. sqrtcvallem4
  10. sqrtcvallem5
  11. sqrtcval
  12. sqrtcval2
  13. resqrtval
  14. imsqrtval
  15. resqrtvalex
  16. imsqrtvalex