Metamath Proof Explorer

Table of Contents - 10.4.3. Absolute value (abstract algebra)

1. cabv
2. df-abv
3. abvfval
4. isabv
5. isabvd
6. abvrcl
7. abvfge0
8. abvf
9. abvcl
10. abvge0
11. abveq0
12. abvne0
13. abvgt0
14. abvmul
15. abvtri
16. abv0
17. abv1z
18. abv1
19. abvneg
20. abvsubtri
21. abvrec
22. abvdiv
23. abvdom
24. abvres
25. abvtrivd
26. abvtriv
27. abvpropd