PA0089

bounded_nonzero_not_divides

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

A nonzero value strictly below a modulus is not divisible by it.

Exact expanded PA statement

forall p a. ~(a = 0) -> (exists wpo_gap_ecb_a_lt_p. wpo_gap_ecb_a_lt_p + S (a) = p) -> (~(exists frm_factor_ecb_not_divisor. a = p * frm_factor_ecb_not_divisor))

Structural proof guide

Generated structural guide

A nonzero value strictly below a modulus is not divisible by it.

Use the direct prerequisites divisor_le_nonzero, lt_not_le as previously established PA formulas.

The proof proceeds by intermediate claims (1).

Referenced ingredients

PA0039 divisor_le_nonzero PA003A lt_not_le

Proof neighborhood

Direct dependencies

PA0039 divisor_le_nonzero PA003A lt_not_le

Direct dependents

PA00BN bounded_euler_criterion_dichotomy

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 ha0
  4. 0004intro hap
  5. 0005intro hdiv
  6. 0006have hpa : exists t. t + p = a
  7. 0007specialize divisor_le_nonzero p
  8. 0008specialize divisor_le_nonzero a
  9. 0009apply divisor_le_nonzero
  10. 0010exact ha0
  11. 0011exact hdiv
  12. 0012specialize lt_not_le a
  13. 0013specialize lt_not_le p
  14. 0014apply lt_not_le
  15. 0015exact hap
  16. 0016exact hpa