Metamath Proof Explorer

Table of Contents - 21.50.22. Elementary geometry (extension)

1. Auxiliary theorems
   1. fv1prop
   2. fv2prop
   3. submuladdmuld
   4. affinecomb1
   5. affinecomb2
   6. affineid
   7. 1subrec1sub
   8. resum2sqcl
   9. resum2sqgt0
   10. resum2sqrp
   11. resum2sqorgt0
   12. reorelicc
2. Real euclidean space of dimension 2
   1. rrx2pxel
   2. rrx2pyel
   3. prelrrx2
   4. prelrrx2b
   5. rrx2pnecoorneor
   6. rrx2pnedifcoorneor
   7. rrx2pnedifcoorneorr
   8. rrx2xpref1o
   9. rrx2xpreen
   10. rrx2plord
   11. rrx2plord1
   12. rrx2plord2
   13. rrx2plordisom
   14. rrx2plordso
   15. ehl2eudisval0
   16. ehl2eudis0lt
3. Spheres and lines in real Euclidean spaces
   1. cline
   2. csph
   3. df-line
   4. df-sph
   5. lines
   6. line
   7. rrxlines
   8. rrxline
   9. rrxlinesc
   10. rrxlinec
   11. eenglngeehlnmlem1
   12. eenglngeehlnmlem2
   13. eenglngeehlnm
   14. rrx2line
   15. rrx2vlinest
   16. rrx2linest
   17. rrx2linesl
   18. rrx2linest2
   19. elrrx2linest2
   20. spheres
   21. sphere
   22. rrxsphere
   23. 2sphere
   24. 2sphere0
   25. line2ylem
   26. line2
   27. line2xlem
   28. line2x
   29. line2y
   30. itsclc0lem1
   31. itsclc0lem2
   32. itsclc0lem3
   33. itscnhlc0yqe
   34. itschlc0yqe
   35. itsclc0yqe
   36. itsclc0yqsollem1
   37. itsclc0yqsollem2
   38. itsclc0yqsol
   39. itscnhlc0xyqsol
   40. itschlc0xyqsol1
   41. itschlc0xyqsol
   42. itsclc0xyqsol
   43. itsclc0xyqsolr
   44. itsclc0xyqsolb
   45. itsclc0
   46. itsclc0b
   47. itsclinecirc0
   48. itsclinecirc0b
   49. itsclinecirc0in
   50. itsclquadb
   51. itsclquadeu
   52. 2itscplem1
   53. 2itscplem2
   54. 2itscplem3
   55. 2itscp
   56. itscnhlinecirc02plem1
   57. itscnhlinecirc02plem2
   58. itscnhlinecirc02plem3
   59. itscnhlinecirc02p
   60. inlinecirc02plem
   61. inlinecirc02p
   62. inlinecirc02preu