Metamath Proof Explorer

Table of Contents - 21.31.3. Exponents and divisibility

1. oexpreposd
2. explt1d
3. expeq1d
4. expeqidd
5. exp11d
6. 0dvds0
7. absdvdsabsb
8. gcdnn0id
9. gcdle1d
10. gcdle2d
11. dvdsexpad
12. dvdsexpnn
13. dvdsexpnn0
14. dvdsexpb
15. posqsqznn
16. zdivgd
17. efsubd
18. ef11d
19. logccne0d
20. cxp112d
21. cxp111d
22. cxpi11d
23. logne0d
24. rxp112d
25. log11d
26. rplog11d
27. rxp11d