BT003B

multiple_decidable_nonzero

Stable checked-use theorem · independently kernel verified

Divisibility by a nonzero natural is constructively decidable.

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

Structural proof guide

Divisibility by a nonzero natural is constructively decidable.

Direct prerequisites: eq_decidable, division_remainder_exists, multiple_has_zero_remainder, division_remainder_unique. The authored body proceeds by case analysis (9), intermediate claims (4), equality transport (2).

Proof neighborhood

Direct dependencies

BT003A eq_decidable BT001P division_remainder_exists BT001W multiple_has_zero_remainder BT001U division_remainder_unique

Direct dependents

BT003C multiple_decidable BT003E factor_search_up_to

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

40 script commands · 18 reading checkpoints · 4 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 (4)
eq decidabledivision remainder existsmultiple has zero remainderdivision remainder unique
01Fix variables and assumptionsL1–3

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

  1. L1
    intro d
  2. L2
    intro n
  3. L3
    intro hd
02Establish hdivL4–6

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

  1. L4
    have hdiv : exists q r. n = d * q + r /\ S r <= d
  2. L5
    apply division_remainder_exists
  3. L6
    exact hd
03Separate the logical casesL7–9

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

  1. L7
    cases hdiv
  2. L8
    cases hdiv_witness
  3. L9
    cases hdiv_witness_witness
04Use earlier factsL10–11

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

  1. L10
    specialize eq_decidable x1
  2. L11
    specialize eq_decidable 0
05Establish hrL12–13

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

  1. L12
    have hr : x1 = 0 \/ ~(x1 = 0)
  2. L13
    apply eq_decidable
06Separate the logical casesL14–15

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

  1. L14
    cases hr
  2. L15
    left
07Construct an explicit witnessL16–16

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

  1. L16
    exists x
08Calculate and transport equalitiesL17–18

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

  1. L17
    rewrite hr_left at hdiv_witness_witness_left
  2. L18
    rewrite PA3 at hdiv_witness_witness_left
09Use earlier factsL19–19

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

  1. L19
    exact hdiv_witness_witness_left
10Separate the logical casesL20–20

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

  1. L20
    right
11Fix variables and assumptionsL21–21

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

  1. L21
    intro hmul
12Establish hzeroL22–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply multiple has zero remainder.

  1. L22
    have hzero : exists q r. ((n = d * q + r /\ r = 0) /\ S r <= d)
  2. L23
    apply multiple_has_zero_remainder
  3. L24
    exact hd
  4. L25
    exact hmul
13Separate the logical casesL26–29

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

  1. L26
    cases hzero
  2. L27
    cases hzero_witness
  3. L28
    cases hzero_witness_witness
  4. L29
    cases hzero_witness_witness_left
14Establish huniqL30–35

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

  1. L30
    have huniq : x = x2 /\ x1 = x3
  2. L31
    apply division_remainder_unique
  3. L32
    exact hdiv_witness_witness_left
  4. L33
    exact hdiv_witness_witness_right
  5. L34
    exact hzero_witness_witness_left_left
  6. L35
    exact hzero_witness_witness_right
15Separate the logical casesL36–36

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

  1. L36
    cases huniq
16Use earlier factsL37–37

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

  1. L37
    apply hr_right
17Calculate and transport equalitiesL38–38

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

  1. L38
    trans x3
18Use earlier factsL39–40

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

  1. L39
    exact huniq_right
  2. L40
    exact hzero_witness_witness_left_right

Library-wide reading audit

Original exact command ledger · 40 lines
  1. 0001intro d
  2. 0002intro n
  3. 0003intro hd
  4. 0004have hdiv : exists q r. n = d * q + r /\ S r <= d
  5. 0005apply division_remainder_exists
  6. 0006exact hd
  7. 0007cases hdiv
  8. 0008cases hdiv_witness
  9. 0009cases hdiv_witness_witness
  10. 0010specialize eq_decidable x1
  11. 0011specialize eq_decidable 0
  12. 0012have hr : x1 = 0 \/ ~(x1 = 0)
  13. 0013apply eq_decidable
  14. 0014cases hr
  15. 0015left
  16. 0016exists x
  17. 0017rewrite hr_left at hdiv_witness_witness_left
  18. 0018rewrite PA3 at hdiv_witness_witness_left
  19. 0019exact hdiv_witness_witness_left
  20. 0020right
  21. 0021intro hmul
  22. 0022have hzero : exists q r. ((n = d * q + r /\ r = 0) /\ S r <= d)
  23. 0023apply multiple_has_zero_remainder
  24. 0024exact hd
  25. 0025exact hmul
  26. 0026cases hzero
  27. 0027cases hzero_witness
  28. 0028cases hzero_witness_witness
  29. 0029cases hzero_witness_witness_left
  30. 0030have huniq : x = x2 /\ x1 = x3
  31. 0031apply division_remainder_unique
  32. 0032exact hdiv_witness_witness_left
  33. 0033exact hdiv_witness_witness_right
  34. 0034exact hzero_witness_witness_left_left
  35. 0035exact hzero_witness_witness_right
  36. 0036cases huniq
  37. 0037apply hr_right
  38. 0038trans x3
  39. 0039exact huniq_right
  40. 0040exact hzero_witness_witness_left_right