Actually Spivak is an old friend of mine but I had not been in contact for a long time and had no chance to hear him for that long time. So it was doubly great for me to hear and see him again.
As to the big theorems in intro calc, I agree with you. In fact I have not included them in the intro course I am teaching now. I did sketch the proof of IVT there though but only briefly.
Nonetheless it was while teaching this course and rereading the material as it is presented in the book, that led me to write down these arguments.
my point is that if they are going to put this stuff in the book at all, for someone to read, they might as well do it better than they do.
e.g. the MVT is a silly theorem that students try to memorize, focusing on whether it is f(b)-f(a)/[b-a] or f(a)-f(b) etc... when this formula is not the important part.
the important part are the corollaries. so those should be stated as the theorems, and this silly formula should be relegated to the proof as I have done.
i.e. there are several key parts to these results:
1) the IVT, that if a function is continuous on an interval then its values also form an interval.
2) next if a function is continuous on a closed bounded interval. then the values also form a closed bounded interval, in particular there is a max and a min.
those are the foundational results, easily proved by just constructing an infinite decimal that works, step by step. still the proof of the second one is a little tedious.
these results are already sufficient to handle almost all max min problems, using the endpoint limit test to deal with open intervals. no MVT or first or second derivative tests are needed. just test critical points and endpoints, or on an open interval, if the limit is infinite at any missing endpoints just test critical points.
using those however, the next results, the MVT type ones, are easier, and should be stated as follows, not as they usually are.
3) a diff'ble function that is not monotone on an open interval, has a critical point on that interval, (at any local extremum). i.e. a function is strictly monotone on any interval where there are no critical points.
this is the way the rolle thm should be stated as it is stronger than that usual statement. this then gives the basic principle of graphing, that a graph is monotone between two successive critical points.
it also gives the first derivative test in a form stronger than the usual corollary of the MVT, namely with this version you only need to test the sign of the derivative at one point of an interval in which there are no critical points, or not at all if you know the value of the function at two successive critical points.
It also follows that if the derivative of a function does not change sign on an interval the function is strictly monotone there, without the MVT.the MVT is just a variation on the rolle thm of course, but there is no point in limiting it to the case usually stated, since that obscures the idea, and makes the statement an unelightening formula instead of a simple statement.
i.e. instead of stating then MVT as it usually is, one should just apply the previous "Rolles" theorem to the difference of two functions.
i.e. the following is a corollary of rolle:
3b) two diff'ble functions that agree at two points, have the same derivative at some intermediate point.
now the whole point of the MVT is the following result which should thus be stated as a theorem:
4) two diff'ble functions with the same derivative on an interval, differ there by a constant, in particular only a constant function can have derivative identically zero.
this is proved as usual by observing that any function agrees at two points with a linear function, hence 3b) implies that a function which is not constant has somewhere the same derivative as a non constant linear one, i.e. has non zero derivative somewhere.
there is no real need for the explicit formula [f(b)-f(a)]/[b-a] to enter the statement at all.my point is this: first the technicalities in the statements of MVT have been allowed to overwhelm the essential results we want people to remember. so for the average students the usual statements are pedagocially flawed.
the statements should be linked to their applications. thus above statement 1 is enough to "solve" equations. statement 2 is enough to do max min problems. 3) is enough for graphing. 4) is enough to do antiderivative problems, like the FTC.
second, for those students who might appreciate the proofs, those proofs have been allowed to become too abstract to present in an elementary course. this too is unnecessary. the arguments using infinite decimals for statements 1, 2 are completely rigorous, and more intuitive than the more abstract least upper bound arguments usually reserved for advanced analysis courses. i.e. one easily constructs least upper bounds as decimals, rather than postulating them for abstractly defined sets.
these are my suggestions.