Clarification required for proof structure in Spivak's Calculus There is a particular "proof structure" I routinely observe throughout Michael Spivak's Calculus that I hoped I could get some commentary on (I will provide the most recently encountered example shortly).
Such questions will be framed as "Prove $P$", and then Spivak's solutions proceed as follows:

*

*Assume $P$ is true.


*Algebraic manipulation


*Arrive at a previously proven statement $Q$.


*Claim $\square$
Here is one such example:

Prove that $\sqrt{(x_1+y_1)^2+(x_2+y_2)^2} \leq \sqrt{x_1^{\ \ \ 2}+x_2^{\ \ \ 2}} + \sqrt{y_1^{\ \ \ 2}+y_2^{\ \ \ 2}}$

The "$Q$" that we have in our back pocket is the Schwarz inequality, which reads as:
$$x_1y_1+x_2y_2 \leq \sqrt{x_1^{\ \ \ 2}+x_2^{\ \ \ 2}}\sqrt{y_1^{\ \ \ 2}+y_2^{\ \ \ 2}}$$
Here is Spivak's solution (verbatim):

This inequality is equivalent to the squared inequality, $$(x_1+y_1)^2+(x_2+y_2)^2 \leq (x_1^{\ \ \ 2}+x_2^{\ \ \ 2})+ (y_1^{\ \ \ 2}+y_2^{\ \ \ 2})+2\sqrt{x_1^{\ \ \ 2}+x_2^{\ \ \ 2}}\sqrt{y_1^{\ \ \ 2}+y_2^{\ \ \ 2}}$$ which is easily seen to be equivalent to the Schwarz inequality


My major confusion with this proof strategy is that I view it as a proof of the implication $P \rightarrow Q$. If I am keen on proving $P$, certainly I am trying to prove $Q \rightarrow P$, right?
Is Spivak glossing over the fact that in order to work backwards (i.e. to start from the Schwarz inequality and arrive at our initial $P$ statement), we must necessarily be in an algebraic field?
I ask this question because it appears as though one of the unspoken assumptions here by Spivak is that we can casually "reverse" all of the algebraic manipulations that allowed us to traverse from $P$ to $Q$, so that we can then go from $Q$ to $P$.
Is this the correct interpretation?

I believe another relevant assumed-to-be-true statement that must be in play for the reversed $Q \rightarrow P$ direction (at least for this particular example) is that $$x,y \gt 0 \land x^2 \geq y^2 \rightarrow x \geq y$$
 A: If Spivak states that he wants to prove $P$, then he observers that $P\iff Q$ and finally he states that $Q$ has been proved before, then since $P\iff Q$, $P$ is proved. There is nothing wrong with that, precisely because we are dealing with an equivalence here.
A: José Carlos Santos answered this specific example perfectly.
All that I'd add is that for real numbers $a$ and $b$,
$$a,b \gt 0 \land a^2 \geq b^2 \rightarrow a \geq b$$
comes from an earlier problem (3rd Edition, 1-5).
Results from past problems are employed throughout the text, both in the chapters themselves and in subsequent problems.
Spivak does slip up here and there. It's good you're keeping him honest.
In general, I think some of the book's arguments do sometimes rely on equivalence relations that aren't explicitly demonstrated, or even acknowledged.
Here are some other things the book uses without (I think) first providing adequate justification. Spivak likely (and fairly) assumes the reader is familiar with these things, but their tacit use is somewhat at odds with his "let's start from nothing" approach. Some of these are maybe not themselves used by the book, but are themselves used to prove others on the list:

*

*Basic algebraic properties (ex: we can add the same number to both sides of an equation)

*Relationships between angles generated by parallel lines cut by a transversal

*Pythagorean Theorem

*Triangle side/angle relationsip (bigger side, bigger angle)

*Sum of two sides of triangle always greater than the third

*Law of sines

*Law of cosines

*$\sqrt a$ (existence of roots is eventually proven, but not before many problems that involve terms like $\sqrt 2$ and $\sqrt{(x_1+y_1)^2+(x_2+y_2)^2}$

*Several limits and a useful limit substitution trick (Chapter 5 "Limits")

There are likely more. My list of things Spivak leaves out probably leaves some things out.
Edit:
Spivak does acknowledge much of this, and is careful not to rely on geometry in his formal proofs. He works to define lines, curves, distance, trigonometric functions, and all in terms of pairs of real numbers.
It's just that some of these things are invoked a bit before they've been fully justified, especially in the examples and problems.
