Metamath Proof Explorer

Table of Contents - 5.4.10. Decimal arithmetic

  1. cdc
  2. df-dec
  3. 9p1e10
  4. dfdec10
  5. decex
  6. deceq1
  7. deceq2
  8. deceq1i
  9. deceq2i
  10. deceq12i
  11. numnncl
  12. num0u
  13. num0h
  14. numcl
  15. numsuc
  16. deccl
  17. 10nn
  18. 10pos
  19. 10nn0
  20. 10re
  21. decnncl
  22. dec0u
  23. dec0h
  24. numnncl2
  25. decnncl2
  26. numlt
  27. numltc
  28. le9lt10
  29. declt
  30. decltc
  31. declth
  32. decsuc
  33. 3declth
  34. 3decltc
  35. decle
  36. decleh
  37. declei
  38. numlti
  39. declti
  40. decltdi
  41. numsucc
  42. decsucc
  43. 1e0p1
  44. dec10p
  45. numma
  46. nummac
  47. numma2c
  48. numadd
  49. numaddc
  50. nummul1c
  51. nummul2c
  52. decma
  53. decmac
  54. decma2c
  55. decadd
  56. decaddc
  57. decaddc2
  58. decrmanc
  59. decrmac
  60. decaddm10
  61. decaddi
  62. decaddci
  63. decaddci2
  64. decsubi
  65. decmul1
  66. decmul1c
  67. decmul2c
  68. decmulnc
  69. 11multnc
  70. decmul10add
  71. 6p5lem
  72. 5p5e10
  73. 6p4e10
  74. 6p5e11
  75. 6p6e12
  76. 7p3e10
  77. 7p4e11
  78. 7p5e12
  79. 7p6e13
  80. 7p7e14
  81. 8p2e10
  82. 8p3e11
  83. 8p4e12
  84. 8p5e13
  85. 8p6e14
  86. 8p7e15
  87. 8p8e16
  88. 9p2e11
  89. 9p3e12
  90. 9p4e13
  91. 9p5e14
  92. 9p6e15
  93. 9p7e16
  94. 9p8e17
  95. 9p9e18
  96. 10p10e20
  97. 10m1e9
  98. 4t3lem
  99. 4t3e12
  100. 4t4e16
  101. 5t2e10
  102. 5t3e15
  103. 5t4e20
  104. 5t5e25
  105. 6t2e12
  106. 6t3e18
  107. 6t4e24
  108. 6t5e30
  109. 6t6e36
  110. 7t2e14
  111. 7t3e21
  112. 7t4e28
  113. 7t5e35
  114. 7t6e42
  115. 7t7e49
  116. 8t2e16
  117. 8t3e24
  118. 8t4e32
  119. 8t5e40
  120. 8t6e48
  121. 8t7e56
  122. 8t8e64
  123. 9t2e18
  124. 9t3e27
  125. 9t4e36
  126. 9t5e45
  127. 9t6e54
  128. 9t7e63
  129. 9t8e72
  130. 9t9e81
  131. 9t11e99
  132. 9lt10
  133. 8lt10
  134. 7lt10
  135. 6lt10
  136. 5lt10
  137. 4lt10
  138. 3lt10
  139. 2lt10
  140. 1lt10
  141. decbin0
  142. decbin2
  143. decbin3
  144. halfthird
  145. 5recm6rec