PA008A · theorem

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.

Statement with defined notation

∀ p. ∀ a. ¬p = 0 → ModEq(p,a,0) → Dvd(p,a)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0003 Dvd PD0008 ModEq

2 occurrences

In local proof propositions

PD0002 Lt

1 occurrences

Exact expanded native-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

Proof neighborhood

Direct theorem prerequisites

PA001V nonzero_is_succ PA002V mod_eq_to_remainder_decomposition PA000H mul_comm

Direct theorem dependents

PA008M quadratic_residue_half_power_mod_one PA00D4 mod_two_zero_to_even

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 : Lt(0,p)Definitions: Lt(0,p)Original native command in the exact edition
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 defined 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 : Lt(0,p)
    Exact native replay linehave 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