BT0022 · Bertrand theorem

mul_left_cancel_nonzero

Stable checked-use theorem · independently kernel verified

A nonzero common left factor can be cancelled.

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

forall a b c. ~(a = 0) -> a * b = a * c -> b = c

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

none

0 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall a b c. ~(a = 0) -> a * b = a * c -> b = c

Proof neighborhood

Direct theorem prerequisites

BT000M mul_eq_zero BT0021 mul_ne_zero BT000U add_right_cancel BT000C succ_ne_zero

Direct theorem dependents

BT002F multiple_antisymm BT003E factor_search_up_to BT003J proper_factor_lt BT00QN prime_power_successor_cancel_cofactor BT00RD mul_le_cancel_left_nonzero BT00U2 central_binom_four_weighted_of_recurrence

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

42 script commands · 19 reading checkpoints · 2 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 (4)
mul eq zeromul ne zeroadd right cancelsucc ne zero
01Fix variables and assumptionsL1–1

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

  1. L1
    intro a
02Induction on bL2–5

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction b
  2. L3
    intro c
  3. L4
    intro ha
  4. L5
    intro h
03Establish hzL6–9

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

  1. L6
    have hz : a * c = 0
  2. L7
    symm
  3. L8
    rewrite PA5 at h
  4. L9
    exact h
04Establish factorsL10–14

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

  1. L10
    have factors : a = 0 \/ c = 0
  2. L11
    specialize mul_eq_zero a
  3. L12
    specialize mul_eq_zero c
  4. L13
    apply mul_eq_zero
  5. L14
    exact hz
05Separate the logical casesL15–16

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

  1. L15
    cases factors
  2. L16
    exfalso
06Use earlier factsL17–18

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

  1. L17
    apply ha
  2. L18
    exact factors_left
07Calculate and transport equalitiesL19–19

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

  1. L19
    symm
08Use earlier factsL20–20

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

  1. L20
    exact factors_right
09Fix variables and assumptionsL21–21

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

  1. L21
    intro c
10Induction on cL22–24

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L22
    induction c
  2. L23
    intro ha
  3. L24
    intro h
11Separate the logical casesL25–25

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

  1. L25
    exfalso
12Use earlier factsL26–31

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

  1. L26
    specialize mul_ne_zero a
  2. L27
    specialize mul_ne_zero (S b)
  3. L28
    apply mul_ne_zero
  4. L29
    exact ha
  5. L30
    specialize succ_ne_zero b
  6. L31
    exact succ_ne_zero
13Calculate and transport equalitiesL32–32

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

  1. L32
    rewrite PA5 at h
14Use earlier factsL33–33

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

  1. L33
    exact h
15Fix variables and assumptionsL34–35

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

  1. L34
    intro ha
  2. L35
    intro h
16Calculate and transport equalitiesL36–36

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

  1. L36
    congr
17Use earlier factsL37–39

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

  1. L37
    apply IH
  2. L38
    exact ha
  3. L39
    apply add_right_cancel
18Calculate and transport equalitiesL40–41

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

  1. L40
    rewrite PA6 at h
  2. L41
    rewrite PA6 at h
19Use earlier factsL42–42

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

  1. L42
    exact h

Library-wide reading audit

Original defined command ledger · 42 lines
  1. 0001intro a
  2. 0002induction b
  3. 0003intro c
  4. 0004intro ha
  5. 0005intro h
  6. 0006have hz : a * c = 0
  7. 0007symm
  8. 0008rewrite PA5 at h
  9. 0009exact h
  10. 0010have factors : a = 0 \/ c = 0
  11. 0011specialize mul_eq_zero a
  12. 0012specialize mul_eq_zero c
  13. 0013apply mul_eq_zero
  14. 0014exact hz
  15. 0015cases factors
  16. 0016exfalso
  17. 0017apply ha
  18. 0018exact factors_left
  19. 0019symm
  20. 0020exact factors_right
  21. 0021intro c
  22. 0022induction c
  23. 0023intro ha
  24. 0024intro h
  25. 0025exfalso
  26. 0026specialize mul_ne_zero a
  27. 0027specialize mul_ne_zero (S b)
  28. 0028apply mul_ne_zero
  29. 0029exact ha
  30. 0030specialize succ_ne_zero b
  31. 0031exact succ_ne_zero
  32. 0032rewrite PA5 at h
  33. 0033exact h
  34. 0034intro ha
  35. 0035intro h
  36. 0036congr
  37. 0037apply IH
  38. 0038exact ha
  39. 0039apply add_right_cancel
  40. 0040rewrite PA6 at h
  41. 0041rewrite PA6 at h
  42. 0042exact h