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. Coprime(a,b) → Dvd(a,a · b) ∧ Dvd(b,a · b) ∧ (∀ x. Dvd(a,x) → Dvd(b,x) → Dvd(a · b,x))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
6 occurrences
In local proof propositions
2 occurrences
Exact expanded native-PA statement
forall a b. (forall d. (exists u. a = d * u) -> (exists v. b = d * v) -> d = 1) -> ((((exists hlcm_left_factor_coprime_product. a * b = a * hlcm_left_factor_coprime_product) /\ (exists hlcm_right_factor_coprime_product. a * b = b * hlcm_right_factor_coprime_product)) /\ forall hlcm_common_coprime_product. (exists hlcm_left_common_coprime_product. hlcm_common_coprime_product = a * hlcm_left_common_coprime_product) -> (exists hlcm_right_common_coprime_product. hlcm_common_coprime_product = b * hlcm_right_common_coprime_product) -> exists hlcm_least_factor_coprime_product. hlcm_common_coprime_product = a * b * hlcm_least_factor_coprime_product))Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
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
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.
Named ingredients (3)
01Fix variables and assumptionsL1–3
02Separate the logical casesL4–5
03Construct an explicit witnessL6–6
Supply the displayed value, then prove that it has the required property.
- L6
exists b
04Calculate and transport equalitiesL7–7
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L7
refl
05Construct an explicit witnessL8–8
Supply the displayed value, then prove that it has the required property.
- L8
exists a
06Use earlier factsL9–9
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L9
apply mul_comm
07Fix variables and assumptionsL10–12
08Separate the logical casesL13–14
09Establish hdivL15–15
Establish this local claim before using it. It is not an additional assumption.
10Construct an explicit witnessL16–16
Supply the displayed value, then prove that it has the required property.
- L16
exists x
11Calculate and transport equalitiesL17–18
12Use earlier factsL19–20
13Establish hfactorL21–27
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gauss coprime cancel.
14Separate the logical casesL28–28
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L28
cases hfactor
15Construct an explicit witnessL29–29
Supply the displayed value, then prove that it has the required property.
- L29
exists x2
16Calculate and transport equalitiesL30–30
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L30
trans b * x1
17Use earlier factsL31–31
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L31
exact hb_witness
18Calculate and transport equalitiesL32–36
19Use earlier factsL37–37
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L37
apply mul_assoc
20Calculate and transport equalitiesL38–38
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L38
congr
21Use earlier factsL39–39
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L39
apply mul_comm
22Calculate and transport equalitiesL40–40
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L40
refl
Original defined command ledger · 40 lines
- 0001
intro a - 0002
intro b - 0003
intro hcop - 0004
split - 0005
split - 0006
exists b - 0007
refl - 0008
exists a - 0009
apply mul_comm - 0010
intro c - 0011
intro ha - 0012
intro hb - 0013
cases ha - 0014
cases hb - 0015
have hdiv : Dvd(a,b · x1)Exact native replay line
have hdiv : exists q. b * x1 = a * q - 0016
exists x - 0017
trans c - 0018
symm - 0019
exact hb_witness - 0020
exact ha_witness - 0021
have hfactor : Dvd(a,x1)Exact native replay line
have hfactor : exists w. x1 = a * w - 0022
specialize gauss_coprime_cancel a - 0023
specialize gauss_coprime_cancel b - 0024
specialize gauss_coprime_cancel x1 - 0025
apply gauss_coprime_cancel - 0026
exact hcop - 0027
exact hdiv - 0028
cases hfactor - 0029
exists x2 - 0030
trans b * x1 - 0031
exact hb_witness - 0032
trans b * (a * x2) - 0033
rewrite hfactor_witness - 0034
refl - 0035
trans (b * a) * x2 - 0036
symm - 0037
apply mul_assoc - 0038
congr - 0039
apply mul_comm - 0040
refl