PA0086

nondivisor_canonical_remainder_exists

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

Every nonmultiple has a nonzero canonical remainder congruent to it.

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

  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