Measurability of sqrt over an algebra with an isometric CFC

If A is a measurable non-unital normed ring with an isometric continuous functional calculus, then the square root function sqrt : A → A is measurable.

theorem CFC.measurable_sqrt {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [CompleteSpace A] [ContinuousStar A] [OrderClosedTopology A] [MeasurableSpace A] [BorelSpace A] : Measurable sqrt