There is a theorem in Murphy's book on operator theory and $C^\ast$-algebras:
Let $u$ be a unitary element in a unital $C^\ast$-algebra $A$. Then if $\sigma(u) \subsetneq S^1$ then there exists a self-adjoint element $a\in A$ such that $u = e^{ia}$.
This theorem comes after a discussion of some properties of $C^\ast$-algebras and the Gelfand representaiton theorem. The theorem is followed by a proof of the existence of a functional calculus at a normal element $a$. The theorem does not appear to be used in any of the two proofs of the theorems that follow it.
I don't understand where this theorem fits into the theory: what is it used for? Why does it appear in a seemingly random place with no relation to adjacent theorems and proofs in the book?
I understand that it gives a sufficient condition for a unitary element to have a logarithm. I also understand its proof. I don't know anything about functional calculus so perhaps this is a very important theorem in functinoal calculus. But if it is this is not mentioned in the book and I'd be very grateful for context!
As far as I can tell, the theorem is there because it allows Murphy to show an application of the Gelfand transform (2.1.10), and because it has to be somewhere in the book.
He later uses the theorem a couple times (in the proof of 7.3.2 and in the proof of 7.5.6).