BT0020 · Bertrand theorem

mul_eq_one_components

Stable checked-use theorem · independently kernel verified

A product is one only when both natural factors are one.

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. a * b = 1 -> a = 1 /\ b = 1

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. a * b = 1 -> a = 1 /\ b = 1

Proof neighborhood

Direct theorem prerequisites

BT0004 mul_zero_left BT000L add_eq_zero_right BT0009 one_mul

Direct theorem dependents

BT002E divisor_one BT002F multiple_antisymm BT006N prime_three BT00RL prime_power_valuation_one_zero

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

39 script commands · 23 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 (3)
mul zero leftadd eq zero rightone mul
01Fix variables and assumptionsL1–1

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

  1. L1
    intro a
02Induction on aL2–6

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

  1. L2
    induction a
  2. L3
    intro b
  3. L4
    intro h
  4. L5
    specialize mul_zero_left b
  5. L6
    rewrite mul_zero_left at h
03Separate the logical casesL7–7

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

  1. L7
    exfalso
04Use earlier factsL8–8

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

  1. L8
    apply PA1
05Calculate and transport equalitiesL9–9

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

  1. L9
    symm
06Use earlier factsL10–10

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

  1. L10
    exact h
07Fix variables and assumptionsL11–11

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

  1. L11
    intro b
08Induction on bL12–14

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

  1. L12
    induction b
  2. L13
    intro h
  3. L14
    rewrite PA5 at h
09Separate the logical casesL15–15

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

  1. L15
    exfalso
10Use earlier factsL16–16

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

  1. L16
    apply PA1
11Calculate and transport equalitiesL17–17

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

  1. L17
    symm
12Use earlier factsL18–18

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

  1. L18
    exact h
13Fix variables and assumptionsL19–19

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

  1. L19
    intro h
14Calculate and transport equalitiesL20–21

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

  1. L20
    rewrite PA6 at h
  2. L21
    rewrite PA4 at h
15Establish hzL22–26

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

  1. L22
    have hz : S a * b + a = 0
  2. L23
    apply PA2
  3. L24
    exact h
  4. L25
    specialize add_eq_zero_right (S a * b)
  5. L26
    specialize add_eq_zero_right a
16Establish ha0L27–29

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

  1. L27
    have ha0 : a = 0
  2. L28
    apply add_eq_zero_right
  3. L29
    exact hz
17Separate the logical casesL30–30

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

  1. L30
    split
18Calculate and transport equalitiesL31–31

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

  1. L31
    congr
19Use earlier factsL32–32

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

  1. L32
    exact ha0
20Calculate and transport equalitiesL33–35

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

  1. L33
    rewrite ha0 at hz
  2. L34
    rewrite ha0 at hz
  3. L35
    rewrite PA3 at hz
21Use earlier factsL36–36

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

  1. L36
    specialize one_mul b
22Calculate and transport equalitiesL37–38

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

  1. L37
    rewrite one_mul at hz
  2. L38
    congr
23Use earlier factsL39–39

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

  1. L39
    exact hz

Library-wide reading audit

Original defined command ledger · 39 lines
  1. 0001intro a
  2. 0002induction a
  3. 0003intro b
  4. 0004intro h
  5. 0005specialize mul_zero_left b
  6. 0006rewrite mul_zero_left at h
  7. 0007exfalso
  8. 0008apply PA1
  9. 0009symm
  10. 0010exact h
  11. 0011intro b
  12. 0012induction b
  13. 0013intro h
  14. 0014rewrite PA5 at h
  15. 0015exfalso
  16. 0016apply PA1
  17. 0017symm
  18. 0018exact h
  19. 0019intro h
  20. 0020rewrite PA6 at h
  21. 0021rewrite PA4 at h
  22. 0022have hz : S a * b + a = 0
  23. 0023apply PA2
  24. 0024exact h
  25. 0025specialize add_eq_zero_right (S a * b)
  26. 0026specialize add_eq_zero_right a
  27. 0027have ha0 : a = 0
  28. 0028apply add_eq_zero_right
  29. 0029exact hz
  30. 0030split
  31. 0031congr
  32. 0032exact ha0
  33. 0033rewrite ha0 at hz
  34. 0034rewrite ha0 at hz
  35. 0035rewrite PA3 at hz
  36. 0036specialize one_mul b
  37. 0037rewrite one_mul at hz
  38. 0038congr
  39. 0039exact hz