In Spivak's Calculus, Chapter 1 Question 5.8:
Prove that, if $0 \leq a \lt b$ and $0 \leq c \lt d$, then $ac \lt bd$ using the following axioms:
I have the following worked out:
Theorem 1
$$ \begin{align} a \cdot 0 &= a \cdot 0 &\text{Identity} \tag{1.0} \\ a \cdot ( 0 + 0 ) &= a \cdot 0 &\text{P2} \tag{1.1} \\ a \cdot 0 + a \cdot 0 &= a \cdot 0 &\text{P9} \tag{1.2} \\ ( a \cdot 0 + a \cdot 0 ) + (-a) \cdot 0 &= a \cdot 0 + (-a) \cdot 0 &\text{By Addition} \tag{1.3} \\ a \cdot 0 + \left[ a \cdot 0 + (-a) \cdot 0 \right] &= a \cdot 0 + (-a) \cdot 0 &\text{P1} \tag{1.4} \\ a \cdot 0 + 0 &= 0 &\text{P3} \tag{1.5} \\ a \cdot 0 &= 0 &\text{P2 QED} \tag{1.6} \\ \end{align} $$
Theorem 2
$$ \begin{align} & ac \lt bc &\text{Assume} \tag{2.0} \\ & 0 \lt bc - ac &\text{Addition of Inverse and P3} \tag{2.1} \\ & 0 \lt c \cdot (b - a) &\text{P9} \tag{2.2} \\ & c \cdot (b - a) \in P &\text{Definition of Positive} \tag{2.3} \\ & ( b - a \in P ) \land ( c \in P ) &\text{P12} \tag{2.4} \\ & ( 0 \lt b - a ) \land ( 0 \lt c ) &\text{Definition of Positive} \tag{2.5} \\ \therefore ( ac \lt bc ) \to & \left[ ( 0 \lt b - a ) \land ( 0 \lt c ) \right] \tag{2.6} \\ \\ &( 0 \lt b - a ) \land ( 0 \lt c ) &\text{Assume} \tag{2.7} \\ & ( b - a \in P ) \land ( c \in P ) &\text{Definition of Positive} \tag{2.8} \\ & c \cdot (b - a) \in P &\text{P12} \tag{2.9} \\ & 0 \lt c \cdot (b - a) &\text{Definition of Positive} \tag{2.10} \\ & 0 \lt bc - ac &\text{P9} \tag{2.11} \\ & ac \lt bc &\text{Addition of Inverse and P3} \tag{2.12} \\ \therefore ( a \lt b ) \land ( 0 \lt c ) \Leftrightarrow &( ac \lt bc ) &\text{2.6 and 2.12 QED} \tag{2.13} \\ \end{align} $$
Exercise 5.8
$$ \begin{align} \left[ ( 0 = a \lt b ) \land ( 0 = c \lt d ) \right] &\to ( ac = 0 ) &\text{Theorem 1} \tag{3.0} \\ \left[ ( 0 = a \lt b ) \land ( 0 = c \lt d ) \right] &\to ( b,d \in P ) &\text{Definition of Positive} \tag{3.1} \\ ( b,d \in P ) &\to (bd \in P ) &\text{P12} \tag{3.2} \\ ( b,d \in P ) &\to ( 0 \lt bd ) &\text{Definition of Positive} \tag{3.3} \\ \left[ ( 0 = a \lt b ) \land ( 0 = c \lt d ) \right] &\to ( ac \lt bd ) &\text{Substitution of 3.0} \tag{3.4} \\ \end{align} $$
Which gets me part of the way there, but I still need to show that the following is true:
$$ \begin{align} \left[ ( 0 \lt a \lt b ) \land ( 0 \lt c \lt d ) \right] &\to ( ac \lt bd ) &\text{Substitution of 3.0} \tag{3.5} \\ \end{align} $$
The answer key in the back of the book hints that I should apply Theorem 2 twice to something to show 3.5 is true--but I'm not seeing how.
Any help would be much appreciated.