|- Unless Mathematica has changed completely over the years, one thing that Jordi seems to overlook is that it is designed to be used to expose the step by step logic of mathematical proof,[...]
No, this is not what it was designed for. Quoting right from Wolfram's book "Mathematica: A System for Doing Mathematics by Computer", page vii,
One way to use Mathematica is as a "calculator". You type in a calculation, and Mathematica immediately tries to do it. [...] You can use Mathematica as a language for representing mathematical knowledge. You can take mathematical relations from handbooks and textbooks and enter them almost directly into Mathematica.
In general, the idea he is giving is that "Mathematica does this for you" and doesn't care about intermediate steps. Also see http://reference.wolfram.com/mathematica/tutorial/WhyYouDoNotUsuallyNeedToKnowAboutInternals.html which essentially says that what's going on inside -- steps, details, etc. -- are irrelevant to the end user.