Metamath Proof Explorer

Table of Contents - 15.5.2. Negation and Subtraction

1. cnegs
2. csubs
3. df-negs
4. df-subs
5. negsfn
6. subsfn
7. negsval
8. negs0s
9. negsproplem1
10. negsproplem2
11. negsproplem3
12. negsproplem4
13. negsproplem5
14. negsproplem6
15. negsproplem7
16. negsprop
17. negscl
18. negscld
19. sltnegim
20. negscut
21. negscut2
22. negsid
23. negsidd
24. negsex
25. negnegs
26. sltneg
27. sleneg
28. sltnegd
29. slenegd
30. negs11
31. negsdi
32. slt0neg2d
33. negsf
34. negsfo
35. negsf1o
36. negsunif
37. negsbdaylem
38. negsbday
39. subsval
40. subsvald
41. subscl
42. subscld
43. subsf
44. subsfo
45. negsval2
46. negsval2d
47. subsid1
48. subsid
49. subadds
50. subaddsd
51. pncans
52. pncan3s
53. pncan2s
54. npcans
55. sltsub1
56. sltsub2
57. sltsub1d
58. sltsub2d
59. negsubsdi2d
60. addsubsassd
61. addsubsd
62. sltsubsubbd
63. sltsubsub2bd
64. sltsubsub3bd
65. slesubsubbd
66. slesubsub2bd
67. slesubsub3bd
68. sltsubaddd
69. sltsubadd2d
70. sltaddsubd
71. sltaddsub2d
72. slesubaddd
73. subsubs4d
74. subsubs2d
75. nncansd
76. posdifsd
77. sltsubposd
78. subsge0d