PA0039

divisor_le_nonzero

Stable checked-use theorem · independently closed

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

Generated structural guide

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

Use the direct prerequisites one_le_of_ne_zero as previously established PA formulas.

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

Referenced ingredients

PA002L one_le_of_ne_zero

Proof neighborhood

Direct dependencies

PA002L one_le_of_ne_zero

Direct dependents

PA0063 prime_bounded_nonzero_mod_inverse PA0072 gauss_half_range_signed_choices PA0082 prime_positive_bounded_product_coprime PA0089 bounded_nonzero_not_divides PA008B prime_mul_index_map_exists_up_to PA008K prime_range_product_coprime PA009C prime_scaled_inverse_unique PA00AG prime_bounded_square_one_cases PA00D8 distinct_odd_prime_half_products_ne PA00DN prime_nondivisor_bounded_scaled_remainder_nonzero

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

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