PA0089 · theorem

bounded_nonzero_not_divides

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

A nonzero value strictly below a modulus is not divisible by 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.

Statement with defined notation

∀ p. ∀ a. ¬a = 0 → Lt(a,p) → ¬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

PD0002 Lt PD0003 Dvd

2 occurrences

In local proof propositions

PD0001 Le

1 occurrences

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

Proof neighborhood

Direct theorem prerequisites

PA0039 divisor_le_nonzero PA003A lt_not_le

Direct theorem dependents

PA00BN bounded_euler_criterion_dichotomy

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

16 script commands · 3 reading checkpoints · 1 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 (2)
divisor le nonzerolt not le
01Fix variables and assumptionsL1–5

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro ha0
  4. L4
    intro hap
  5. L5
    intro hdiv
02Establish hpaL6–15

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

  1. L6
  2. L7
    specialize divisor_le_nonzero p
  3. L8
    specialize divisor_le_nonzero a
  4. L9
    apply divisor_le_nonzero
  5. L10
    exact ha0
  6. L11
    exact hdiv
  7. L12
    specialize lt_not_le a
  8. L13
    specialize lt_not_le p
  9. L14
    apply lt_not_le
  10. L15
    exact hap
03Use earlier factsL16–16

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

  1. L16
    exact hpa

Library-wide reading audit

Original defined command ledger · 16 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro ha0
  4. 0004intro hap
  5. 0005intro hdiv
  6. 0006have hpa : Le(p,a)
    Exact native replay linehave 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