Metamath Proof Explorer

Table of Contents - 20.43.23.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