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