Formal proof for $(-1) \times (-1) = 1$ Is there a formal proof for $(-1) \times (-1) = 1$? It's a fundamental formula not only in arithmetic but also in the whole of math. Is there a proof for it or is it just assumed?

Suppose we're given the natural numbers $\mathbb{N}=\{0,1,2,\ldots\}$ with Peano's axioms. In other words, we know what it means to "add" and "multiply" any two numbers in $\mathbb{N}$, we  can tell if one natural number is bigger than another, and if $x>y$, we know what $x-y$ means---namely, $x-y$ is the natural (this is important) number which when added to $y$ gets you $x$. 
To get the integers, we need to define what negative numbers are. We can do this by representing each integer (which for the time being is an undefined word) by pairs of natural numbers: Consider any two pairs $(x,y)$ and $(x',y')$ of natural numbers. We'd like these guys to "represent the same integer" if $x-y=x'-y'$. But what if $x<y$? Then we don't know what $x-y$ even means! So, we have to do a little juggling. We say that $(x,y)$ and $(x',y')$ both "represent the same integer" if $x+y'=x'+y$. Finally, we define the set of integers $\mathbb{Z}$ to be the set of all these pairs, where two pairs are considered to be the same if they both "represent the same integer". For instance, we define $-1$ to be the pair $(0,1)$ (which is the same as the pairs $(2,3)$ and $(7921,7920)$). 
To see how to define multiplication of integers, we use FOIL: With our usual integers, we have $(a-b)(c-d)=-ad-bc+ac+bd$, so we simply define this to be the case with our new integers: i.e., $(a,b)(c,d)$ is defined to be $(ac+bd,ad+bc)$. In particular, this means that $(-1)(-1)=(0,1)(0,1)=(0\cdot 0 + 1\cdot 1, 0\cdot 1 + 1\cdot 0)=(1,0)=1$. 
