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