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 b m n. ~(b = 0) -> b = 2 * (m * n) -> (~(m = 0) /\ ~(n = 0))Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.
Definitions used by this theorem
In the theorem statement
In local proof propositions
Exact expanded first-order statement
forall b m n. ~(b = 0) -> b = 2 * (m * n) -> (~(m = 0) /\ ~(n = 0))Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
Definition-aware tactic body
Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.
Read the argument
Proof checkpoints
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.
01Fix variables and assumptionsL1–5
02Establish hproductL6–14
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor nonzero right.
03Separate the logical casesL15–15
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L15
split
04Fix variables and assumptionsL16–16
Work with arbitrary variables or the premises of the current implication.
- L16
intro hm
05Use earlier factsL17–17
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L17
apply hproduct
06Calculate and transport equalitiesL18–18
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L18
rewrite hm
07Use earlier factsL19–19
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L19
apply mul_zero_left
08Fix variables and assumptionsL20–20
Work with arbitrary variables or the premises of the current implication.
- L20
intro hn
09Use earlier factsL21–21
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L21
apply hproduct
Original defined command ledger · 23 lines
- 0001
intro b - 0002
intro m - 0003
intro n - 0004
intro hb - 0005
intro heq - 0006
have hproduct : ~(m * n = 0) - 0007
intro hzero - 0008
specialize factor_nonzero_right b - 0009
specialize factor_nonzero_right 2 - 0010
specialize factor_nonzero_right (m * n) - 0011
apply factor_nonzero_right - 0012
exact hb - 0013
exact heq - 0014
exact hzero - 0015
split - 0016
intro hm - 0017
apply hproduct - 0018
rewrite hm - 0019
apply mul_zero_left - 0020
intro hn - 0021
apply hproduct - 0022
rewrite hn - 0023
simp