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