Metamath Proof Explorer

Table of Contents - 5.5.1. Positive reals (as a subset of complex numbers)

1. crp
2. df-rp
3. elrp
4. elrpii
5. 1rp
6. 2rp
7. 3rp
8. 5rp
9. rpssre
10. rpre
11. rpxr
12. rpcn
13. nnrp
14. rpgt0
15. rpge0
16. rpregt0
17. rprege0
18. rpne0
19. rprene0
20. rpcnne0
21. rpcndif0
22. ralrp
23. rexrp
24. rpaddcl
25. rpmulcl
26. rpmtmip
27. rpdivcl
28. rpreccl
29. rphalfcl
30. rpgecl
31. rphalflt
32. rerpdivcl
33. ge0p1rp
34. rpneg
35. negelrp
36. negelrpd
37. 0nrp
38. ltsubrp
39. ltaddrp
40. difrp
41. elrpd
42. nnrpd
43. zgt1rpn0n1
44. rpred
45. rpxrd
46. rpcnd
47. rpgt0d
48. rpge0d
49. rpne0d
50. rpregt0d
51. rprege0d
52. rprene0d
53. rpcnne0d
54. rpreccld
55. rprecred
56. rphalfcld
57. reclt1d
58. recgt1d
59. rpaddcld
60. rpmulcld
61. rpdivcld
62. ltrecd
63. lerecd
64. ltrec1d
65. lerec2d
66. lediv2ad
67. ltdiv2d
68. lediv2d
69. ledivdivd
70. divge1
71. divlt1lt
72. divle1le
73. ledivge1le
74. ge0p1rpd
75. rerpdivcld
76. ltsubrpd
77. ltaddrpd
78. ltaddrp2d
79. ltmulgt11d
80. ltmulgt12d
81. gt0divd
82. ge0divd
83. rpgecld
84. divge0d
85. ltmul1d
86. ltmul2d
87. lemul1d
88. lemul2d
89. ltdiv1d
90. lediv1d
91. ltmuldivd
92. ltmuldiv2d
93. lemuldivd
94. lemuldiv2d
95. ltdivmuld
96. ltdivmul2d
97. ledivmuld
98. ledivmul2d
99. ltmul1dd
100. ltmul2dd
101. ltdiv1dd
102. lediv1dd
103. lediv12ad
104. mul2lt0rlt0
105. mul2lt0rgt0
106. mul2lt0llt0
107. mul2lt0lgt0
108. mul2lt0bi
109. prodge0rd
110. prodge0ld
111. ltdiv23d
112. lediv23d
113. lt2mul2divd
114. nnledivrp
115. nn0ledivnn
116. addlelt
117. ge2halflem1