PA0086

nondivisor_canonical_remainder_exists

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

Every nonmultiple has a nonzero canonical remainder congruent to it.

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 frm_factor_eca_canonical_not_divisor. a = p * frm_factor_eca_canonical_not_divisor)) -> (exists r. ~(r = 0) /\ ((exists wpo_gap_eca_canonical_bound. wpo_gap_eca_canonical_bound + S (r) = p) /\ (exists wpp_mod_left_eca_canonical_mod wpp_mod_right_eca_canonical_mod. (a) + p * wpp_mod_left_eca_canonical_mod = (r) + p * wpp_mod_right_eca_canonical_mod)))

Structural proof guide

Generated structural guide

Every nonmultiple has a nonzero canonical remainder congruent to it.

Use the direct prerequisites division_remainder_exists, mul_comm, remainder_decomposition_to_mod_eq as previously established PA formulas.

The proof proceeds by case analysis (3), intermediate claims (4), equality transport (1), certified simplification (1).

Referenced ingredients

PA001D division_remainder_exists PA000H mul_comm PA003C remainder_decomposition_to_mod_eq

Proof neighborhood

Direct dependencies

PA001D division_remainder_exists PA000H mul_comm PA003C remainder_decomposition_to_mod_eq

Direct dependents

PA00BR arbitrary_euler_criterion_residue_iff PA00BT arbitrary_euler_criterion_nonresidue_iff

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

39 script commands · 15 reading checkpoints · 4 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)
division remainder existsmul commremainder decomposition to mod eq
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 hp0
  4. L4
    intro hnotdiv
02Establish hdivisionL5–9

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply division remainder exists.

  1. L5
    have hdivision : exists q r. a = p * q + r /\ exists gap. gap + S r = p
  2. L6
    specialize division_remainder_exists p
  3. L7
    specialize division_remainder_exists a
  4. L8
    apply division_remainder_exists
  5. L9
    exact hp0
03Separate the logical casesL10–12

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

  1. L10
    cases hdivision
  2. L11
    cases hdivision_witness
  3. L12
    cases hdivision_witness_witness
04Establish hr0L13–15

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

  1. L13
    have hr0 : ~(x1 = 0)
  2. L14
    intro hrzero
  3. L15
    apply hnotdiv
05Construct an explicit witnessL16–16

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

  1. L16
    exists x
06Calculate and transport equalitiesL17–17

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

  1. L17
    trans p * x + x1
07Use earlier factsL18–18

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

  1. L18
    exact hdivision_witness_witness_left
08Calculate and transport equalitiesL19–20

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

  1. L19
    rewrite hrzero
  2. L20
    simp
09Establish hdecompositionL21–26

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

  1. L21
    have hdecomposition : a = x * p + x1
  2. L22
    trans p * x + x1
  3. L23
    exact hdivision_witness_witness_left
  4. L24
    congr
  5. L25
    apply mul_comm
  6. L26
    refl
10Establish hmodL27–33

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

  1. L27
    have hmod : exists wpp_mod_left_eca_canonical_proof_mod wpp_mod_right_eca_canonical_proof_mod. (a) + p * wpp_mod_left_eca_canonical_proof_mod = (x1) + p * wpp_mod_right_eca_canonical_proof_mod
  2. L28
    specialize remainder_decomposition_to_mod_eq p
  3. L29
    specialize remainder_decomposition_to_mod_eq a
  4. L30
    specialize remainder_decomposition_to_mod_eq x
  5. L31
    specialize remainder_decomposition_to_mod_eq x1
  6. L32
    apply remainder_decomposition_to_mod_eq
  7. L33
    exact hdecomposition
11Construct an explicit witnessL34–34

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

  1. L34
    exists x1
12Separate the logical casesL35–35

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

  1. L35
    split
13Use earlier factsL36–36

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

  1. L36
    exact hr0
14Separate the logical casesL37–37

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

  1. L37
    split
15Use earlier factsL38–39

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

  1. L38
    exact hdivision_witness_witness_right
  2. L39
    exact hmod

Library-wide reading audit

Original exact command ledger · 39 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro hp0
  4. 0004intro hnotdiv
  5. 0005have hdivision : exists q r. a = p * q + r /\ exists gap. gap + S r = p
  6. 0006specialize division_remainder_exists p
  7. 0007specialize division_remainder_exists a
  8. 0008apply division_remainder_exists
  9. 0009exact hp0
  10. 0010cases hdivision
  11. 0011cases hdivision_witness
  12. 0012cases hdivision_witness_witness
  13. 0013have hr0 : ~(x1 = 0)
  14. 0014intro hrzero
  15. 0015apply hnotdiv
  16. 0016exists x
  17. 0017trans p * x + x1
  18. 0018exact hdivision_witness_witness_left
  19. 0019rewrite hrzero
  20. 0020simp
  21. 0021have hdecomposition : a = x * p + x1
  22. 0022trans p * x + x1
  23. 0023exact hdivision_witness_witness_left
  24. 0024congr
  25. 0025apply mul_comm
  26. 0026refl
  27. 0027have hmod : exists wpp_mod_left_eca_canonical_proof_mod wpp_mod_right_eca_canonical_proof_mod. (a) + p * wpp_mod_left_eca_canonical_proof_mod = (x1) + p * wpp_mod_right_eca_canonical_proof_mod
  28. 0028specialize remainder_decomposition_to_mod_eq p
  29. 0029specialize remainder_decomposition_to_mod_eq a
  30. 0030specialize remainder_decomposition_to_mod_eq x
  31. 0031specialize remainder_decomposition_to_mod_eq x1
  32. 0032apply remainder_decomposition_to_mod_eq
  33. 0033exact hdecomposition
  34. 0034exists x1
  35. 0035split
  36. 0036exact hr0
  37. 0037split
  38. 0038exact hdivision_witness_witness_right
  39. 0039exact hmod