1. The problem statement, all variables and given/known data prove 2ab<= a^2+b^2 using order axioms Of course use of other basic axioms for real numbers are also okay. 2. Relevant equations axioms for set of real numbers. 3. The attempt at a solution The easy way to do this would be just subtract 2ab from both sides, factor, and see that (a-b)^2 is greater or equal to zero. But we have to use the basic axioms. So I tried constructing a^2+b^2-2ab by multiplying (a-b)(a-b) using the axioms. I'm not sure I was rigorous enough. Also I'm not sure whether I can just say a square of a real number is greater than zero. Though it is easy to prove.