PA008A

mod_eq_zero_to_dvd_nonzero

Alpha v16 checked-use theorem · independently closed; not Stable

For a nonzero modulus, congruence to zero gives an explicit divisor witness.

Exact expanded PA statement

forall p a. ~(p = 0) -> (exists wpp_mod_left_euler_zero_mod wpp_mod_right_euler_zero_mod. (a) + p * wpp_mod_left_euler_zero_mod = (0) + p * wpp_mod_right_euler_zero_mod) -> exists k. a = p * k

Structural proof guide

Generated structural guide

For a nonzero modulus, congruence to zero gives an explicit divisor witness.

Use the direct prerequisites nonzero_is_succ, mod_eq_to_remainder_decomposition, mul_comm as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (3), certified simplification (2).

Referenced ingredients

PA001V nonzero_is_succ PA002V mod_eq_to_remainder_decomposition PA000H mul_comm

Proof neighborhood

Direct dependencies

PA001V nonzero_is_succ PA002V mod_eq_to_remainder_decomposition PA000H mul_comm

Direct dependents

PA008M quadratic_residue_half_power_mod_one PA00D4 mod_two_zero_to_even

Formal native tactic body

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

  1. 0001intro p
  2. 0002intro a
  3. 0003intro hp
  4. 0004intro hmod
  5. 0005have hps : exists n. p = S n
  6. 0006specialize nonzero_is_succ p
  7. 0007apply nonzero_is_succ
  8. 0008exact hp
  9. 0009cases hps
  10. 0010have hbound : exists d. d + S 0 = p
  11. 0011exists x
  12. 0012trans S x
  13. 0013simp
  14. 0014symm
  15. 0015exact hps_witness
  16. 0016have hdecomp : exists q. a = q * p + 0
  17. 0017specialize mod_eq_to_remainder_decomposition p
  18. 0018specialize mod_eq_to_remainder_decomposition a
  19. 0019specialize mod_eq_to_remainder_decomposition 0
  20. 0020apply mod_eq_to_remainder_decomposition
  21. 0021exact hp
  22. 0022exact hbound
  23. 0023exact hmod
  24. 0024cases hdecomp
  25. 0025exists x1
  26. 0026trans x1 * p + 0
  27. 0027exact hdecomp_witness
  28. 0028trans x1 * p
  29. 0029simp
  30. 0030apply mul_comm