BT003J

proper_factor_lt

Stable checked-use theorem · independently kernel verified

A factor with a nonunit cofactor is strictly smaller than a nonzero product.

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

Structural proof guide

A factor with a nonunit cofactor is strictly smaller than a nonzero product.

Direct prerequisites: divisor_le_nonzero, le_eq_or_lt, mul_left_cancel_nonzero, mul_one. The authored body proceeds by case analysis (1), intermediate claims (3).

Proof neighborhood

Direct dependencies

BT002D divisor_le_nonzero BT001C le_eq_or_lt BT0022 mul_left_cancel_nonzero BT000A mul_one

Direct dependents

BT003K prime_divisor_exists_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

43 script commands · 15 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 (4)
divisor le nonzerole eq or ltmul left cancel nonzeromul one
01Fix variables and assumptionsL1–6

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

  1. L1
    intro n
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro hn
  5. L5
    intro hfactor
  6. L6
    intro hd
02Establish hleL7–11

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

  1. L7
    have hle : exists k. k + c = n
  2. L8
    specialize divisor_le_nonzero c
  3. L9
    specialize divisor_le_nonzero n
  4. L10
    apply divisor_le_nonzero
  5. L11
    exact hn
03Construct an explicit witnessL12–12

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

  1. L12
    exists d
04Use earlier factsL13–13

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

  1. L13
    exact hfactor
05Establish hcasesL14–18

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

  1. L14
    have hcases : c = n \/ exists k. k + S c = n
  2. L15
    specialize le_eq_or_lt c
  3. L16
    specialize le_eq_or_lt n
  4. L17
    apply le_eq_or_lt
  5. L18
    exact hle
06Separate the logical casesL19–20

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

  1. L19
    cases hcases
  2. L20
    exfalso
07Use earlier factsL21–21

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

  1. L21
    apply hd
08Establish hcL22–31

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

  1. L22
    have hc : ~(c = 0)
  2. L23
    intro hc0
  3. L24
    apply hn
  4. L25
    trans c
  5. L26
    symm
  6. L27
    exact hcases_left
  7. L28
    exact hc0
  8. L29
    specialize mul_left_cancel_nonzero c
  9. L30
    specialize mul_left_cancel_nonzero d
  10. L31
    specialize mul_left_cancel_nonzero 1
09Use earlier factsL32–33

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

  1. L32
    apply mul_left_cancel_nonzero
  2. L33
    exact hc
10Calculate and transport equalitiesL34–35

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

  1. L34
    trans n
  2. L35
    symm
11Use earlier factsL36–36

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

  1. L36
    exact hfactor
12Calculate and transport equalitiesL37–38

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

  1. L37
    trans c
  2. L38
    symm
13Use earlier factsL39–39

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

  1. L39
    exact hcases_left
14Calculate and transport equalitiesL40–40

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

  1. L40
    symm
15Use earlier factsL41–43

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

  1. L41
    specialize mul_one c
  2. L42
    exact mul_one
  3. L43
    exact hcases_right

Library-wide reading audit

Original exact command ledger · 43 lines
  1. 0001intro n
  2. 0002intro c
  3. 0003intro d
  4. 0004intro hn
  5. 0005intro hfactor
  6. 0006intro hd
  7. 0007have hle : exists k. k + c = n
  8. 0008specialize divisor_le_nonzero c
  9. 0009specialize divisor_le_nonzero n
  10. 0010apply divisor_le_nonzero
  11. 0011exact hn
  12. 0012exists d
  13. 0013exact hfactor
  14. 0014have hcases : c = n \/ exists k. k + S c = n
  15. 0015specialize le_eq_or_lt c
  16. 0016specialize le_eq_or_lt n
  17. 0017apply le_eq_or_lt
  18. 0018exact hle
  19. 0019cases hcases
  20. 0020exfalso
  21. 0021apply hd
  22. 0022have hc : ~(c = 0)
  23. 0023intro hc0
  24. 0024apply hn
  25. 0025trans c
  26. 0026symm
  27. 0027exact hcases_left
  28. 0028exact hc0
  29. 0029specialize mul_left_cancel_nonzero c
  30. 0030specialize mul_left_cancel_nonzero d
  31. 0031specialize mul_left_cancel_nonzero 1
  32. 0032apply mul_left_cancel_nonzero
  33. 0033exact hc
  34. 0034trans n
  35. 0035symm
  36. 0036exact hfactor
  37. 0037trans c
  38. 0038symm
  39. 0039exact hcases_left
  40. 0040symm
  41. 0041specialize mul_one c
  42. 0042exact mul_one
  43. 0043exact hcases_right