Metamath Proof Explorer

Table of Contents - 5.4.5. Simple number properties

1. halfcl
2. rehalfcl
3. half0
4. halfpos2
5. halfpos
6. halfnneg2
7. halfaddsubcl
8. halfaddsub
9. subhalfhalf
10. lt2halves
11. addltmul
12. nominpos
13. avglt1
14. avglt2
15. avgle1
16. avgle2
17. avgle
18. 2timesd
19. times2d
20. halfcld
21. 2halvesd
22. rehalfcld
23. lt2halvesd
24. rehalfcli
25. lt2addmuld
26. add1p1
27. sub1m1
28. cnm2m1cnm3
29. xp1d2m1eqxm1d2
30. div4p1lem1div2