PA008A

mod_eq_zero_to_dvd_nonzero

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

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

30 script commands · 14 reading checkpoints · 3 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (3)
nonzero is succmod eq to remainder decompositionmul comm
01Fix variables and assumptionsL1–4

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro hp
  4. L4
    intro hmod
02Establish hpsL5–8

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply nonzero is succ.

  1. L5
    have hps : exists n. p = S n
  2. L6
    specialize nonzero_is_succ p
  3. L7
    apply nonzero_is_succ
  4. L8
    exact hp
03Separate the logical casesL9–9

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L9
    cases hps
04Establish hboundL10–10

Establish this local claim before using it. It is not an additional assumption.

  1. L10
    have hbound : exists d. d + S 0 = p
05Construct an explicit witnessL11–11

Supply the displayed value, then prove that it has the required property.

  1. L11
    exists x
06Calculate and transport equalitiesL12–14

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L12
    trans S x
  2. L13
    simp
  3. L14
    symm
07Use earlier factsL15–15

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L15
    exact hps_witness
08Establish hdecompL16–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq to remainder decomposition.

  1. L16
    have hdecomp : exists q. a = q * p + 0
  2. L17
    specialize mod_eq_to_remainder_decomposition p
  3. L18
    specialize mod_eq_to_remainder_decomposition a
  4. L19
    specialize mod_eq_to_remainder_decomposition 0
  5. L20
    apply mod_eq_to_remainder_decomposition
  6. L21
    exact hp
  7. L22
    exact hbound
  8. L23
    exact hmod
09Separate the logical casesL24–24

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L24
    cases hdecomp
10Construct an explicit witnessL25–25

Supply the displayed value, then prove that it has the required property.

  1. L25
    exists x1
11Calculate and transport equalitiesL26–26

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L26
    trans x1 * p + 0
12Use earlier factsL27–27

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L27
    exact hdecomp_witness
13Calculate and transport equalitiesL28–29

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L28
    trans x1 * p
  2. L29
    simp
14Use earlier factsL30–30

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L30
    apply mul_comm

Library-wide reading audit

Original exact command ledger · 30 lines
  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