← Formalpedia
lean_workbook_plus_64095 Open by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
x = r cos a cos b cos c x = r\cos a\cos b\cos c x = r cos a cos b cos c y = r cos a cos b sin c y = r\cos a\cos b\sin c y = r cos a cos b sin c z = r sin a cos b z = r\sin a\cos b z = r sin a cos b u = r sin b u = r\sin b u = r sin b x 2 + y 2 + z 2 + u 2 = r 2 cos 2 a cos 2 b cos 2 c + r 2 cos 2 a cos 2 b sin 2 c + r 2 sin 2 a cos 2 b + r 2 sin 2 b x^2+y^2+z^2+u^2 = r^2\cos^2 a\cos^2 b\cos^2 c + r^2\cos^2 a\cos^2 b\sin^2 c + r^2\sin^2 a\cos^2 b + r^2\sin^2 b x 2 + y 2 + z 2 + u 2 = r 2 cos 2 a cos 2 b cos 2 c + r 2 cos 2 a cos 2 b sin 2 c + r 2 sin 2 a cos 2 b + r 2 sin 2 b = r 2 cos 2 a cos 2 b ( cos 2 c + sin 2 c ) + r 2 sin 2 a cos 2 b + r 2 sin 2 b = r^2\cos^2a\cos^2 b(\cos^2 c + \sin^2 c) + r^2\sin^2 a\cos^2 b + r^2\sin^2 b = r 2 cos 2 a cos 2 b ( cos 2 c + sin 2 c ) + r 2 sin 2 a cos 2 b + r 2 sin 2 b = r 2 cos 2 a cos 2 b + r 2 sin 2 a cos 2 b + r 2 sin 2 b = r^2\cos^2a\cos^2 b + r^2\sin^2 a\cos^2 b + r^2\sin^2 b = r 2 cos 2 a cos 2 b + r 2 sin 2 a cos 2 b + r 2 sin 2 b = r 2 cos 2 b ( cos 2 a + sin 2 a ) + r 2 sin 2 b =r^2\cos^2 b(\cos^2a + \sin^2 a) + r^2\sin^2 b = r 2 cos 2 b ( cos 2 a + sin 2 a ) + r 2 sin 2 b = r 2 cos 2 b + r 2 sin 2 b =r^2\cos^2 b + r^2\sin^2 b = r 2 cos 2 b + r 2 sin 2 b = r 2 ( cos 2 b + sin 2 b ) =r^2(\cos^2 b+\sin^2 b) = r 2 ( cos 2 b + sin 2 b ) = r 2 . =r^2. = r 2 .
Preamble
import Mathlib.Analysis.Complex.Basic Formal statement
theorem lean_workbook_plus_64095 (x y z u r a b c : ℝ) :
x = r * cos a * cos b * cos c ∧
y = r * cos a * cos b * sin c ∧
z = r * sin a * cos b ∧
u = r * sin b →
x^2 + y^2 + z^2 + u^2 = r^2 := by sorry View graph