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
∀ n. ModEq(2,n,1) → Odd(n)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
2 occurrences
In local proof propositions
0 occurrences
Exact expanded native-PA statement
forall n. (exists pmt_u_n_one pmt_v_n_one. n + 2 * pmt_u_n_one = 1 + 2 * pmt_v_n_one) -> (exists pmt_odd_n. n = 2 * pmt_odd_n + 1)Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
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
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 (2)
01Fix variables and assumptionsL1–2
02Establish hdecompL3–10
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq to remainder decomposition.
03Construct an explicit witnessL11–11
Supply the displayed value, then prove that it has the required property.
- L11
exists 0
04Calculate and transport equalitiesL12–12
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L12
norm_num
05Use earlier factsL13–13
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L13
exact hone
06Separate the logical casesL14–14
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L14
cases hdecomp
07Construct an explicit witnessL15–15
Supply the displayed value, then prove that it has the required property.
- L15
exists x
08Calculate and transport equalitiesL16–16
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L16
trans x * 2 + 1
09Use earlier factsL17–17
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L17
exact hdecomp_witness
10Calculate and transport equalitiesL18–18
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L18
congr
11Use earlier factsL19–19
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L19
apply mul_comm
12Calculate and transport equalitiesL20–20
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L20
refl
Original defined command ledger · 20 lines
- 0001
intro n - 0002
intro hone - 0003
have hdecomp : exists q. n = q * 2 + 1 - 0004
specialize mod_eq_to_remainder_decomposition 2 - 0005
specialize mod_eq_to_remainder_decomposition n - 0006
specialize mod_eq_to_remainder_decomposition 1 - 0007
apply mod_eq_to_remainder_decomposition - 0008
intro htwo - 0009
apply PA1 - 0010
exact htwo - 0011
exists 0 - 0012
norm_num - 0013
exact hone - 0014
cases hdecomp - 0015
exists x - 0016
trans x * 2 + 1 - 0017
exact hdecomp_witness - 0018
congr - 0019
apply mul_comm - 0020
refl