PA000N · theorem

mul_eq_one_components

Stable checked-use theorem · independently closed

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. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

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

PA000D mul_zero_left PA0004 add_eq_zero_right PA000M one_mul

Direct theorem dependents

PA000O divisor_one

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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