Metamath Proof Explorer

Table of Contents - 6.2.12. Lagrange's four-square theorem

1. cgz
2. df-gz
3. elgz
4. gzcn
5. zgz
6. igz
7. gznegcl
8. gzcjcl
9. gzaddcl
10. gzmulcl
11. gzreim
12. gzsubcl
13. gzabssqcl
14. 4sqlem5
15. 4sqlem6
16. 4sqlem7
17. 4sqlem8
18. 4sqlem9
19. 4sqlem10
20. 4sqlem1
21. 4sqlem2
22. 4sqlem3
23. 4sqlem4a
24. 4sqlem4
25. mul4sqlem
26. mul4sq
27. 4sqlem11
28. 4sqlem12
29. 4sqlem13
30. 4sqlem14
31. 4sqlem15
32. 4sqlem16
33. 4sqlem17
34. 4sqlem18
35. 4sqlem19
36. 4sq