theorem
proved
wrapper
dalembert_cascade
show as:
view Lean formalization →
formal statement (Lean)
264theorem dalembert_cascade (a b : ℤ) :
265 Jcost (PhiForcing.φ ^ a * PhiForcing.φ ^ b) +
266 Jcost (PhiForcing.φ ^ a / PhiForcing.φ ^ b) =
267 2 * Jcost (PhiForcing.φ ^ a) + 2 * Jcost (PhiForcing.φ ^ b) +
268 2 * Jcost (PhiForcing.φ ^ a) * Jcost (PhiForcing.φ ^ b) :=
proof body
One-line wrapper that applies dalembert_identity.
269 dalembert_identity (zpow_pos PhiForcing.phi_pos a) (zpow_pos PhiForcing.phi_pos b)
270