BT002D

divisor_le_nonzero

Stable checked-use theorem · independently kernel verified

A divisor of a nonzero natural is bounded by that natural.

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 d n. ~(n = 0) -> (exists q. n = d * q) -> exists k. k + d = n

Structural proof guide

A divisor of a nonzero natural is bounded by that natural.

Direct prerequisites: one_le_of_ne_zero. The authored body proceeds by case analysis (2), intermediate claims (3), equality transport (1).

Proof neighborhood

Direct dependencies

BT0010 one_le_of_ne_zero

Direct dependents

BT003F prime_or_composite BT003J proper_factor_lt BT00QG prime_power_divides_exponent_le_value BT00VB factorial_prime_le_of_divides BT00VI primorial_even_interval_le_central BT00VJ primorial_odd_interval_le_middle BT0118 nonprime_has_small_prime_divisor_below_square BT011B nonzero_remainder_not_multiple

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

31 script commands · 13 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.

Named ingredients (1)
one le of ne zero
01Fix variables and assumptionsL1–4

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

  1. L1
    intro d
  2. L2
    intro n
  3. L3
    intro hn
  4. L4
    intro hd
02Separate the logical casesL5–5

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

  1. L5
    cases hd
03Establish hqL6–13

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

  1. L6
    have hq : ~(x = 0)
  2. L7
    intro hx
  3. L8
    apply hn
  4. L9
    trans d * x
  5. L10
    exact hd_witness
  6. L11
    rewrite hx
  7. L12
    apply PA5
  8. L13
    specialize one_le_of_ne_zero x
04Establish h1qL14–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply one le of ne zero.

  1. L14
    have h1q : exists k. k + 1 = x
  2. L15
    apply one_le_of_ne_zero
  3. L16
    exact hq
05Separate the logical casesL17–17

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

  1. L17
    cases h1q
06Establish hsL18–21

Establish this local claim before using it. It is not an additional assumption.

  1. L18
    have hs : S x1 = x
  2. L19
    trans x1 + 1
  3. L20
    simp
  4. L21
    exact h1q_witness
07Construct an explicit witnessL22–22

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

  1. L22
    exists d * x1
08Calculate and transport equalitiesL23–24

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

  1. L23
    trans d * S x1
  2. L24
    symm
09Use earlier factsL25–25

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

  1. L25
    apply PA6
10Calculate and transport equalitiesL26–28

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

  1. L26
    trans d * x
  2. L27
    congr
  3. L28
    refl
11Use earlier factsL29–29

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

  1. L29
    exact hs
12Calculate and transport equalitiesL30–30

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

  1. L30
    symm
13Use earlier factsL31–31

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

  1. L31
    exact hd_witness

Library-wide reading audit

Original exact command ledger · 31 lines
  1. 0001intro d
  2. 0002intro n
  3. 0003intro hn
  4. 0004intro hd
  5. 0005cases hd
  6. 0006have hq : ~(x = 0)
  7. 0007intro hx
  8. 0008apply hn
  9. 0009trans d * x
  10. 0010exact hd_witness
  11. 0011rewrite hx
  12. 0012apply PA5
  13. 0013specialize one_le_of_ne_zero x
  14. 0014have h1q : exists k. k + 1 = x
  15. 0015apply one_le_of_ne_zero
  16. 0016exact hq
  17. 0017cases h1q
  18. 0018have hs : S x1 = x
  19. 0019trans x1 + 1
  20. 0020simp
  21. 0021exact h1q_witness
  22. 0022exists d * x1
  23. 0023trans d * S x1
  24. 0024symm
  25. 0025apply PA6
  26. 0026trans d * x
  27. 0027congr
  28. 0028refl
  29. 0029exact hs
  30. 0030symm
  31. 0031exact hd_witness