Metamath Proof Explorer

Table of Contents - 5.5.2. Infinity and the extended real number system (cont.)

1. cxne
2. cxad
3. cxmu
4. df-xneg
5. df-xadd
6. df-xmul
7. ltxr
8. elxr
9. xrnemnf
10. xrnepnf
11. xrltnr
12. ltpnf
13. ltpnfd
14. 0ltpnf
15. mnflt
16. mnfltd
17. mnflt0
18. mnfltpnf
19. mnfltxr
20. pnfnlt
21. nltmnf
22. pnfge
23. pnfged
24. xnn0n0n1ge2b
25. 0lepnf
26. xnn0ge0
27. mnfle
28. mnfled
29. xrltnsym
30. xrltnsym2
31. xrlttri
32. xrlttr
33. xrltso
34. xrlttri2
35. xrlttri3
36. xrleloe
37. xrleltne
38. xrltlen
39. dfle2
40. dflt2
41. xrltle
42. xrltled
43. xrleid
44. xrleidd
45. xrletri
46. xrletri3
47. xrletrid
48. xrlelttr
49. xrltletr
50. xrletr
51. xrlttrd
52. xrlelttrd
53. xrltletrd
54. xrletrd
55. xrltne
56. xrgtned
57. nltpnft
58. xgepnf
59. ngtmnft
60. xlemnf
61. xrrebnd
62. xrre
63. xrre2
64. xrre3
65. ge0gtmnf
66. ge0nemnf
67. xrrege0
68. xrmax1
69. xrmax2
70. xrmin1
71. xrmin2
72. xrmaxeq
73. xrmineq
74. xrmaxlt
75. xrltmin
76. xrmaxle
77. xrlemin
78. max1
79. max1ALT
80. max2
81. 2resupmax
82. min1
83. min2
84. maxle
85. lemin
86. maxlt
87. ltmin
88. lemaxle
89. max0sub
90. ifle
91. z2ge
92. qbtwnre
93. qbtwnxr
94. qsqueeze
95. qextltlem
96. qextlt
97. qextle
98. xralrple
99. alrple
100. xnegeq
101. xnegex
102. xnegpnf
103. xnegmnf
104. rexneg
105. xneg0
106. xnegcl
107. xnegneg
108. xneg11
109. xltnegi
110. xltneg
111. xleneg
112. xlt0neg1
113. xlt0neg2
114. xle0neg1
115. xle0neg2
116. xaddval
117. xaddf
118. xmulval
119. xaddpnf1
120. xaddpnf2
121. xaddmnf1
122. xaddmnf2
123. pnfaddmnf
124. mnfaddpnf
125. rexadd
126. rexsub
127. rexaddd
128. xnn0xaddcl
129. xaddnemnf
130. xaddnepnf
131. xnegid
132. xaddcl
133. xaddcom
134. xaddrid
135. xaddlid
136. xaddridd
137. xnn0lem1lt
138. xnn0lenn0nn0
139. xnn0le2is012
140. xnn0xadd0
141. xnegdi
142. xaddass
143. xaddass2
144. xpncan
145. xnpcan
146. xleadd1a
147. xleadd2a
148. xleadd1
149. xltadd1
150. xltadd2
151. xaddge0
152. xle2add
153. xlt2add
154. xsubge0
155. xposdif
156. xlesubadd
157. xmullem
158. xmullem2
159. xmulcom
160. xmul01
161. xmul02
162. xmulneg1
163. xmulneg2
164. rexmul
165. xmulf
166. xmulcl
167. xmulpnf1
168. xmulpnf2
169. xmulmnf1
170. xmulmnf2
171. xmulpnf1n
172. xmulrid
173. xmullid
174. xmulm1
175. xmulasslem2
176. xmulgt0
177. xmulge0
178. xmulasslem
179. xmulasslem3
180. xmulass
181. xlemul1a
182. xlemul2a
183. xlemul1
184. xlemul2
185. xltmul1
186. xltmul2
187. xadddilem
188. xadddi
189. xadddir
190. xadddi2
191. xadddi2r
192. x2times
193. xnegcld
194. xaddcld
195. xmulcld
196. xadd4d
197. xnn0add4d