PA0021

dvd_to_mod_zero

Stable checked-use theorem · independently closed

A multiple is balanced-congruent to zero.

Exact expanded PA statement

forall m a. (exists k. a = m * k) -> exists u v. a + m * u = 0 + m * v

Structural proof guide

Generated structural guide

A multiple is balanced-congruent to zero.

Use the direct prerequisites zero_add as previously established PA formulas.

The proof proceeds by case analysis (1), equality transport (1), certified simplification (1).

Referenced ingredients

PA0001 zero_add

Proof neighborhood

Direct dependencies

PA0001 zero_add

Direct dependents

PA0026 binary_crt PA007B gauss_mixed_sign_scaled_source_impossible PA008M quadratic_residue_half_power_mod_one PA00CH even_to_mod_two_zero

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  1. 0001intro m
  2. 0002intro a
  3. 0003intro h
  4. 0004cases h
  5. 0005exists 0
  6. 0006exists x
  7. 0007rewrite h_witness
  8. 0008simp [zero_add]