BT002F · Bertrand theorem

multiple_antisymm

Stable checked-use theorem · independently kernel verified

Mutual divisibility is antisymmetric over natural numbers.

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

∀ a. ∀ b. Dvd(a,b) → Dvd(b,a) → a = b

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

PD0003 Dvd

2 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall a b. (exists x. b = a * x) -> (exists y. a = b * y) -> a = b

Proof neighborhood

Direct theorem prerequisites

BT000Q zero_or_succ BT0004 mul_zero_left BT0008 mul_assoc BT000A mul_one BT0022 mul_left_cancel_nonzero BT0020 mul_eq_one_components

Direct theorem dependents

BT0105 prime_contribution_product_eq

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

50 script commands · 19 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.

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 (6)
zero or succmul zero leftmul assocmul onemul left cancel nonzeromul eq one components
01Fix variables and assumptionsL1–4

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro hab
  4. L4
    intro hba
02Separate the logical casesL5–6

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

  1. L5
    cases hab
  2. L6
    cases hba
03Use earlier factsL7–7

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

  1. L7
    specialize zero_or_succ a
04Separate the logical casesL8–8

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

  1. L8
    cases zero_or_succ
05Calculate and transport equalitiesL9–10

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

  1. L9
    rewrite zero_or_succ_left
  2. L10
    rewrite zero_or_succ_left at hab_witness
06Use earlier factsL11–11

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

  1. L11
    specialize mul_zero_left x
07Calculate and transport equalitiesL12–13

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

  1. L12
    rewrite mul_zero_left at hab_witness
  2. L13
    symm
08Use earlier factsL14–14

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

  1. L14
    exact hab_witness
09Separate the logical casesL15–15

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

  1. L15
    cases zero_or_succ_right
10Establish haL16–20

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

  1. L16
    have ha : ~(a = 0)
  2. L17
    intro ha0
  3. L18
    rewrite zero_or_succ_right_witness at ha0
  4. L19
    apply PA1
  5. L20
    exact ha0
11Establish hcycleL21–30

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

  1. L21
    have hcycle : a = a * (x * x1)
  2. L22
    trans b * x1
  3. L23
    exact hba_witness
  4. L24
    trans (a * x) * x1
  5. L25
    congr
  6. L26
    exact hab_witness
  7. L27
    refl
  8. L28
    apply mul_assoc
  9. L29
    specialize mul_left_cancel_nonzero a
  10. L30
    specialize mul_left_cancel_nonzero 1
12Use earlier factsL31–31

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

  1. L31
    specialize mul_left_cancel_nonzero (x * x1)
13Establish hunitL32–40

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

  1. L32
    have hunit : 1 = x * x1
  2. L33
    apply mul_left_cancel_nonzero
  3. L34
    exact ha
  4. L35
    specialize mul_one a
  5. L36
    trans a
  6. L37
    apply mul_one
  7. L38
    exact hcycle
  8. L39
    specialize mul_eq_one_components x
  9. L40
    specialize mul_eq_one_components x1
14Establish hpartsL41–44

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

  1. L41
    have hparts : x = 1 /\ x1 = 1
  2. L42
    apply mul_eq_one_components
  3. L43
    symm
  4. L44
    exact hunit
15Separate the logical casesL45–45

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

  1. L45
    cases hparts
16Calculate and transport equalitiesL46–47

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

  1. L46
    symm
  2. L47
    trans a * x
17Use earlier factsL48–48

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

  1. L48
    exact hab_witness
18Calculate and transport equalitiesL49–49

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

  1. L49
    rewrite hparts_left
19Use earlier factsL50–50

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

  1. L50
    apply mul_one

Library-wide reading audit

Original defined command ledger · 50 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro hab
  4. 0004intro hba
  5. 0005cases hab
  6. 0006cases hba
  7. 0007specialize zero_or_succ a
  8. 0008cases zero_or_succ
  9. 0009rewrite zero_or_succ_left
  10. 0010rewrite zero_or_succ_left at hab_witness
  11. 0011specialize mul_zero_left x
  12. 0012rewrite mul_zero_left at hab_witness
  13. 0013symm
  14. 0014exact hab_witness
  15. 0015cases zero_or_succ_right
  16. 0016have ha : ~(a = 0)
  17. 0017intro ha0
  18. 0018rewrite zero_or_succ_right_witness at ha0
  19. 0019apply PA1
  20. 0020exact ha0
  21. 0021have hcycle : a = a * (x * x1)
  22. 0022trans b * x1
  23. 0023exact hba_witness
  24. 0024trans (a * x) * x1
  25. 0025congr
  26. 0026exact hab_witness
  27. 0027refl
  28. 0028apply mul_assoc
  29. 0029specialize mul_left_cancel_nonzero a
  30. 0030specialize mul_left_cancel_nonzero 1
  31. 0031specialize mul_left_cancel_nonzero (x * x1)
  32. 0032have hunit : 1 = x * x1
  33. 0033apply mul_left_cancel_nonzero
  34. 0034exact ha
  35. 0035specialize mul_one a
  36. 0036trans a
  37. 0037apply mul_one
  38. 0038exact hcycle
  39. 0039specialize mul_eq_one_components x
  40. 0040specialize mul_eq_one_components x1
  41. 0041have hparts : x = 1 /\ x1 = 1
  42. 0042apply mul_eq_one_components
  43. 0043symm
  44. 0044exact hunit
  45. 0045cases hparts
  46. 0046symm
  47. 0047trans a * x
  48. 0048exact hab_witness
  49. 0049rewrite hparts_left
  50. 0050apply mul_one