Metamath Proof Explorer

Table of Contents - 5.1.3. Real and complex number postulates restated as axioms

  1. ax-cnex
  2. ax-resscn
  3. ax-1cn
  4. ax-icn
  5. ax-addcl
  6. ax-addrcl
  7. ax-mulcl
  8. ax-mulrcl
  9. ax-mulcom
  10. ax-addass
  11. ax-mulass
  12. ax-distr
  13. ax-i2m1
  14. ax-1ne0
  15. ax-1rid
  16. ax-rnegex
  17. ax-rrecex
  18. ax-cnre
  19. ax-pre-lttri
  20. ax-pre-lttrn
  21. ax-pre-ltadd
  22. ax-pre-mulgt0
  23. ax-pre-sup
  24. ax-addf
  25. ax-mulf