Metamath Proof Explorer


Table of Contents - 5.4.4. Some properties of specific numbers

This section includes specific theorems about one-digit natural numbers (membership, addition, subtraction, multiplication, division, ordering).

  1. neg1cn
  2. neg1rr
  3. neg1ne0
  4. neg1lt0
  5. negneg1e1
  6. 1pneg1e0
  7. 0m0e0
  8. 1m0e1
  9. 0p1e1
  10. fv0p1e1
  11. 1p0e1
  12. 1p1e2
  13. 2m1e1
  14. 1e2m1
  15. 3m1e2
  16. 4m1e3
  17. 5m1e4
  18. 6m1e5
  19. 7m1e6
  20. 8m1e7
  21. 9m1e8
  22. 2p2e4
  23. 2times
  24. times2
  25. 2timesi
  26. times2i
  27. 2txmxeqx
  28. 2div2e1
  29. 2p1e3
  30. 1p2e3
  31. 1p2e3ALT
  32. 3p1e4
  33. 4p1e5
  34. 5p1e6
  35. 6p1e7
  36. 7p1e8
  37. 8p1e9
  38. 3p2e5
  39. 3p3e6
  40. 4p2e6
  41. 4p3e7
  42. 4p4e8
  43. 5p2e7
  44. 5p3e8
  45. 5p4e9
  46. 6p2e8
  47. 6p3e9
  48. 7p2e9
  49. 1t1e1
  50. 2t1e2
  51. 2t2e4
  52. 3t1e3
  53. 3t2e6
  54. 3t3e9
  55. 4t2e8
  56. 2t0e0
  57. 4d2e2
  58. 1lt2
  59. 2lt3
  60. 1lt3
  61. 3lt4
  62. 2lt4
  63. 1lt4
  64. 4lt5
  65. 3lt5
  66. 2lt5
  67. 1lt5
  68. 5lt6
  69. 4lt6
  70. 3lt6
  71. 2lt6
  72. 1lt6
  73. 6lt7
  74. 5lt7
  75. 4lt7
  76. 3lt7
  77. 2lt7
  78. 1lt7
  79. 7lt8
  80. 6lt8
  81. 5lt8
  82. 4lt8
  83. 3lt8
  84. 2lt8
  85. 1lt8
  86. 8lt9
  87. 7lt9
  88. 6lt9
  89. 5lt9
  90. 4lt9
  91. 3lt9
  92. 2lt9
  93. 1lt9
  94. 0ne2
  95. 1ne2
  96. 1le2
  97. 2cnne0
  98. 2rene0
  99. 1le3
  100. neg1mulneg1e1
  101. halfre
  102. halfcn
  103. halfgt0
  104. halfge0
  105. halflt1
  106. 1mhlfehlf
  107. 8th4div3
  108. halfpm6th
  109. it0e0
  110. 2mulicn
  111. 2muline0