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).
- 1pneg1e0
- 0m0e0
- 1m0e1
- 0p1e1
- fv0p1e1
- 1p0e1
- 1p1e2
- 2m1e1
- 2m1e1OLD
- 1e2m1
- 3m1e2
- 4m1e3
- 5m1e4
- 6m1e5
- 7m1e6
- 8m1e7
- 9m1e8
- 2p2e4
- 2times
- times2
- 2timesi
- times2i
- 2txmxeqx
- 2div2e1
- 2p1e3
- 1p2e3
- 1p2e3ALT
- 3p1e4
- 4p1e5
- 5p1e6
- 6p1e7
- 7p1e8
- 8p1e9
- 3p2e5
- 3p3e6
- 4p2e6
- 4p3e7
- 4p4e8
- 5p2e7
- 5p3e8
- 5p4e9
- 6p2e8
- 6p3e9
- 7p2e9
- 1t1e1
- 2t1e2
- 2t2e4
- 3t1e3
- 3t2e6
- 2t3e6
- 3t3e9
- 4t2e8
- 2t4e8
- 2t0e0
- 4div2e2
- 1lt2
- 2lt3
- 2le3
- 1lt3
- 3lt4
- 2lt4
- 1lt4
- 4lt5
- 3lt5
- 2lt5
- 1lt5
- 5lt6
- 4lt6
- 3lt6
- 2lt6
- 1lt6
- 6lt7
- 5lt7
- 4lt7
- 3lt7
- 2lt7
- 1lt7
- 7lt8
- 6lt8
- 5lt8
- 4lt8
- 3lt8
- 2lt8
- 1lt8
- 8lt9
- 7lt9
- 6lt9
- 5lt9
- 4lt9
- 3lt9
- 2lt9
- 1lt9
- 0ne2
- 1ne2
- 1le2
- 2cnne0
- 2rene0
- 1le3
- neg1mulneg1e1
- halfre
- halfcn
- halfgt0
- halfge0
- halflt1
- 2halves
- 1mhlfehlf
- 8th4div3
- halfthird
- halfpm6th
- it0e0
- 2mulicn
- 2muline0