Validity of "circular" proofs

Question

I believe this is an easy question. I put circular in quotations because I'm pretty sure I'm not talking about circular proofs in general.

I was thinking about how to prove that any function whose derivative is 0 for any $x$ is a constant function. The first thing that came to mind is using the result $f(a)-f(b)=f'(c)(b -a)$

This proves the statement trivially.

The thing is, I don't remember how the proof for the mean value theorem went so as far as I know, it might have used the statement that I wanted to prove.

Now here's my question. If we take some system of axioms as true and prove all these things without circular proofs, meaning that all of those statements hold true as long as their premises are true. Does that mean that I can use a "higher" result to prove some other statement that might have been used in the proof of the "higher" result? (take into account that both the "higher" result and the one I'm trying to prove have already been shown true in legal ways)

Answer 1

First, rest assured that the proof of the mean value theorem does not rely on the fact that a function with zero derivative is constant.

To your seoncd concern: Yes, it is valid to do this. There is no circularity involved because you can align the argumentation non-cyclic (think of time axis).

For example, in order to show that a specific map with five countries can be coloured with only four colours, it is valid to summon theorem (with ultra-long computer-based proof by Aplle/Haken) that every planar map is four-colourable. You may do so even if their proof required them to explicitly show for some maps, perhaps including yor map, that they could be coloured. (Of course, you could also simply exhibit an explicit colouring).

As another example, when asked to show that the Klein 4-group is not simple, you could refer to the classification of finite simple groups and verify that this group is not on the list. Of course the (very long) proof of the classification theorem involves explicit proofs that certain (families of) groups are not simple, but that doesn't matter later on.

Of course you cannot write a book and have some lemma on page 50 and write "We postpone the proof until later (see page 101)", then have a theorem on page 100 the proof of which relies on all preceeding material (including the lemma on page 50) and then on page 101 write "We now come back to the proof of the lemma on page 50 as promised: It is just a special case of the preceeding theorem."