Formal Proof that area of a rectangle is $ab$
Solution 1:
This is a good question! On the face of it, it seems that before you can start being rigorous, you have to define precisely what you mean by the area of a rectangle. But this is just what you are trying to prove!
However, there is another approach: you define exactly the properties that you require of a reasonable area metric. Then you adopt these properties as your axioms, and use them to show that an $a \times\ b$ rectangle has area $ab$.
In a Euclidean plane, we would expect the following axioms to hold for a reasonable area metric on $a \times b$ rectangles (with $a, b \ge 0$):
$A1$: The area of a $1 \times 1$ rectangle is $1$.
$A2$: Any two congruent rectangles have the same area.
$A3$: If a rectangle $R$ is the union of disjoint rectangles $S$ and $T$, then the area of $R$ is equal to the sum of the areas of $S$ and $T$.
Given these axioms, I think we can show by induction that for rational numbers $a$ and $b$, the area of an $a \times b$ rectangle is indeed $ab$. But what about rectangles with irrational sides? I think this might require another axiom:
$A4$: If a rectangle $R$ contains a rectangle $S$, then the area of $R$ is not less than the area of $S$.
Otherwise you might be able to construct pathological area metrics using the Axiom of Choice. But I am open to correction on this.
If anybody can suggest corrections or improvements to this axiom set, feel free to post them as a separate answer, so they don't get lost in the comments.
Solution 2:
One can also start from the following axioms:
$A1$: The area of a $a \times a$ square is $a^2$.
$A2$: Any two congruent shapes have the same area.
$A3$: If a shape $R$ is disjoint union of shapes $S$ and $T$, then the area of $R$ is equal to the sum of the areas of $S$ and $T$.
With these axioms at hand one readily finds the area of a rectangle with sides $a$ and $b$:
On the sides of the rectangle $ABCD$ build the squares $ABC_1D_1$ and $A_1BCD_2$. Let $D_3= (A_1D_2)\cap (C_1D_1)$.
Obviously the rectangles $ABCD$ and $A_1BC_1D_3$ are congruent. Therefore from our axioms one obtains: $$\begin{align} 2[ABCD]&=[DD_1D_3D_2]-[ABC_1D_1]-[A_1BCD_2]\\ &=(a+b)^2-a^2-b^2=2ab. \end{align} $$