Metamath Proof Explorer


Table of Contents - 21.20.6.5. Extended numbers and projective lines as sets

We parameterize the set of infinite extended complex numbers (df-bj-ccinfty) using the real numbers (df-r) via the function . Since at that point, we have only defined the set of real numbers but no operations on it, we define a temporary "fractional part" function, which is more convenient to define on the temporary reals (df-nr) since we can use operations on the latter. We also define the temporary real "one-half" in order to define minus infinity (df-bj-minfty) and then we can define the sets of extended real numbers and of extended complex numbers, and the projective real and complex lines, as well as addition and negation on these, and also the order relation on the extended reals (which bypasses the intermediate definition of a temporary order on the real numbers and then a superseding one on the extended real numbers).

  1. cfractemp
  2. df-bj-fractemp
  3. cinftyexpitau
  4. df-bj-inftyexpitau
  5. cccinftyN
  6. df-bj-ccinftyN
  7. bj-inftyexpitaufo
  8. chalf
  9. df-bj-onehalf
  10. bj-inftyexpitaudisj
  11. cinftyexpi
  12. df-bj-inftyexpi
  13. bj-inftyexpiinv
  14. bj-inftyexpiinj
  15. bj-inftyexpidisj
  16. cccinfty
  17. df-bj-ccinfty
  18. bj-ccinftydisj
  19. bj-elccinfty
  20. cccbar
  21. df-bj-ccbar
  22. bj-ccssccbar
  23. bj-ccinftyssccbar
  24. cpinfty
  25. df-bj-pinfty
  26. bj-pinftyccb
  27. bj-pinftynrr
  28. cminfty
  29. df-bj-minfty
  30. bj-minftyccb
  31. bj-minftynrr
  32. bj-pinftynminfty
  33. crrbar
  34. df-bj-rrbar
  35. cinfty
  36. df-bj-infty
  37. ccchat
  38. df-bj-cchat
  39. crrhat
  40. df-bj-rrhat
  41. bj-rrhatsscchat