Here's something I've been thinking about again recently

So, a while ago I tried to prove that the derivative of sin is cos using the limit calculation, that's lim h->0 [sin(x + h) - sin(x)] / h. After finishing it, I realized that I used the rule of L'hopital, so I used the fact that sin' = cos in order to prove that sin' = cos. And ofc logically speaking, sin' = cos => sin' = cos is a tautology, so it doesn't prove anything. But then I realized that it's actually still pretty strong evidence – certainly it would be strong rational evidence if you didn't know what the derivative of sin was – because if you postulate an incorrect derivative, the same calculation will most likely get you a contradiction. For example, if you postulate that sin(x)' cos(x)' = x, then what you prove is that sin'(x) = cos'(x) = x => sin(x) = 0, which is a contradiction, so it does give you a valid proof that sin(x)' or cos(x)' does not equal x.

The other replies are good for the general question, but this specific question seems to have some interesting points in it.

First: note that applying l'Hopital to the general derivative rule produces a tautology:

lim h->0 f(x+h)-f(x)/h=lim h->0 f'(x+h)/1=f'(x).

If you restrict yourself to using the derivative of

*sin*, then you'll get the tautology. The reason your problem gets wonky is because you're involving the derivative of cos as well, because of the other steps involved in finding the actual solution.

Trying to solve the limit, I assume you used the addition rule for sin, and got to:

sin'(x) = lim h->0 (sin(x)*(cos(h)-1)/h)+ (cos(x)*(sin(h)/h))

Now what's interesting here is that the parts of this equation involving the limit are in fact derivatives at 0. i.e. lim h->0 (cos(h)-1)/h=cos'(0) and lim h->0 sin(h)/h=sin'(0).

So, applying l'Hopital here is no longer a tautology, it's in fact not changing the equation at all. So, we have an equation that tells us a relationship between sin'(x) and sin'(0) and cos'(0). To simplify the form of the relationship let's suppose sin'(x)=f(x) and cos'(x)=g(x) we get:

f(x)=g(0)*sin(x)+f(0)*cos(x).

Now, if we evaluate this at 0 we see that f(0)=g(0)*0+f(0)*1=f(0). So we can choose any values for f(0) and g(0) and it's valid. So we get the full set of all solutions:

f(x)=C*sin(x)+D*cos(x).

Note that g(x) does not depend at all on f(x), so it can be whatever you want as long as you choose it first, rather than trying to arbitrarily choose both at the same time.

So, in the end it's funny because using l'Hopital on the derivative rule produces a tautology, but using it on this modified form does not produce a tautology, but actually just expresses what's already true. The "tautology" element comes from the f(0) evaluation above, but the produced equation is actually a pretty tight constraint on the form of sin'(x).