Metamath Proof Explorer

Table of Contents - 5.3.2. Subtraction

  1. cmin
  2. cneg
  3. df-sub
  4. df-neg
  5. 0cnALT
  6. 0cnALT2
  7. negeu
  8. subval
  9. negeq
  10. negeqi
  11. negeqd
  12. nfnegd
  13. nfneg
  14. csbnegg
  15. negex
  16. subcl
  17. negcl
  18. negicn
  19. subf
  20. subadd
  21. subadd2
  22. subsub23
  23. pncan
  24. pncan2
  25. pncan3
  26. npcan
  27. addsubass
  28. addsub
  29. subadd23
  30. addsub12
  31. 2addsub
  32. addsubeq4
  33. pncan3oi
  34. mvrraddi
  35. mvlladdi
  36. subid
  37. subid1
  38. npncan
  39. nppcan
  40. nnpcan
  41. nppcan3
  42. subcan2
  43. subeq0
  44. npncan2
  45. subsub2
  46. nncan
  47. subsub
  48. nppcan2
  49. subsub3
  50. subsub4
  51. sub32
  52. nnncan
  53. nnncan1
  54. nnncan2
  55. npncan3
  56. pnpcan
  57. pnpcan2
  58. pnncan
  59. ppncan
  60. addsub4
  61. subadd4
  62. sub4
  63. neg0
  64. negid
  65. negsub
  66. subneg
  67. negneg
  68. neg11
  69. negcon1
  70. negcon2
  71. negeq0
  72. subcan
  73. negsubdi
  74. negdi
  75. negdi2
  76. negsubdi2
  77. neg2sub
  78. renegcli
  79. resubcli
  80. renegcl
  81. resubcl
  82. negreb
  83. peano2cnm
  84. peano2rem
  85. negcli
  86. negidi
  87. negnegi
  88. subidi
  89. subid1i
  90. negne0bi
  91. negrebi
  92. negne0i
  93. subcli
  94. pncan3i
  95. negsubi
  96. subnegi
  97. subeq0i
  98. neg11i
  99. negcon1i
  100. negcon2i
  101. negdii
  102. negsubdii
  103. negsubdi2i
  104. subaddi
  105. subadd2i
  106. subaddrii
  107. subsub23i
  108. addsubassi
  109. addsubi
  110. subcani
  111. subcan2i
  112. pnncani
  113. addsub4i
  114. 0reALT
  115. negcld
  116. subidd
  117. subid1d
  118. negidd
  119. negnegd
  120. negeq0d
  121. negne0bd
  122. negcon1d
  123. negcon1ad
  124. neg11ad
  125. negned
  126. negne0d
  127. negrebd
  128. subcld
  129. pncand
  130. pncan2d
  131. pncan3d
  132. npcand
  133. nncand
  134. negsubd
  135. subnegd
  136. subeq0d
  137. subne0d
  138. subeq0ad
  139. subne0ad
  140. neg11d
  141. negdid
  142. negdi2d
  143. negsubdid
  144. negsubdi2d
  145. neg2subd
  146. subaddd
  147. subadd2d
  148. addsubassd
  149. addsubd
  150. subadd23d
  151. addsub12d
  152. npncand
  153. nppcand
  154. nppcan2d
  155. nppcan3d
  156. subsubd
  157. subsub2d
  158. subsub3d
  159. subsub4d
  160. sub32d
  161. nnncand
  162. nnncan1d
  163. nnncan2d
  164. npncan3d
  165. pnpcand
  166. pnpcan2d
  167. pnncand
  168. ppncand
  169. subcand
  170. subcan2d
  171. subcanad
  172. subneintrd
  173. subcan2ad
  174. subneintr2d
  175. addsub4d
  176. subadd4d
  177. sub4d
  178. 2addsubd
  179. addsubeq4d
  180. subeqxfrd
  181. mvlraddd
  182. mvlladdd
  183. mvrraddd
  184. mvrladdd
  185. assraddsubd
  186. subaddeqd
  187. addlsub
  188. addrsub
  189. subexsub
  190. addid0
  191. addn0nid
  192. pnpncand
  193. subeqrev
  194. addeq0
  195. pncan1
  196. npcan1
  197. subeq0bd
  198. renegcld
  199. resubcld
  200. negn0
  201. negf1o