⊢ (A ∈ ℂ → (exp ‘(-i · A)) = ((cos ‘A) − (i · (sin ‘A)))).*

That's the exponential function in terms of sine and cosine. Actually, a similar, more familiar proof has been there for a while, but I still wonder: Is a Metamath-checked proof of e^{i π}+1=0 near?

*A full Unicode font is your friend here.