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
∀ p. ∀ q. Odd(p) → (Odd(p · q) → Odd(q)) ∧ (Odd(q) → Odd(p · q))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
5 occurrences
In local proof propositions
1 occurrences
Exact expanded native-PA statement
forall p q. (exists pod_odd_multiplier. p = 2 * pod_odd_multiplier + 1) -> ((((exists pod_odd_product_odd. p * q = 2 * pod_odd_product_odd + 1) -> (exists pod_odd_factor_odd. q = 2 * pod_odd_factor_odd + 1)) /\ ((exists pod_odd_factor_odd. q = 2 * pod_odd_factor_odd + 1) -> (exists pod_odd_product_odd. p * q = 2 * pod_odd_product_odd + 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 (4)
01Fix variables and assumptionsL1–3
02Separate the logical casesL4–4
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L4
split
03Fix variables and assumptionsL5–5
Work with arbitrary variables or the premises of the current implication.
- L5
intro hproduct
04Establish hqcasesL6–8
05Separate the logical casesL9–11
06Establish hproduct_evenL12–15
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply even mul right.
- L12
have hproduct_even : Even(p · q)Definitions: Even(p · q)Original native command in the exact edition - L13
specialize even_mul_right p - L14
specialize even_mul_right q - L15
apply even_mul_right
07Construct an explicit witnessL16–16
Supply the displayed value, then prove that it has the required property.
- L16
exists x
08Use earlier factsL17–21
09Construct an explicit witnessL22–22
Supply the displayed value, then prove that it has the required property.
- L22
exists x
10Use earlier factsL23–23
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L23
exact hqcases_witness_right
11Fix variables and assumptionsL24–24
Work with arbitrary variables or the premises of the current implication.
- L24
intro hq
Original defined command ledger · 29 lines
- 0001
intro p - 0002
intro q - 0003
intro hp - 0004
split - 0005
intro hproduct - 0006
have hqcases : exists k. q = 2 * k \/ q = 2 * k + 1 - 0007
specialize parity_cases q - 0008
exact parity_cases - 0009
cases hqcases - 0010
cases hqcases_witness - 0011
exfalso - 0012
have hproduct_even : Even(p · q)Exact native replay line
have hproduct_even : exists pod_even_odd_iff_contradiction. p * q = 2 * pod_even_odd_iff_contradiction - 0013
specialize even_mul_right p - 0014
specialize even_mul_right q - 0015
apply even_mul_right - 0016
exists x - 0017
exact hqcases_witness_left - 0018
specialize odd_not_even (p * q) - 0019
apply odd_not_even - 0020
exact hproduct - 0021
exact hproduct_even - 0022
exists x - 0023
exact hqcases_witness_right - 0024
intro hq - 0025
specialize odd_mul_odd p - 0026
specialize odd_mul_odd q - 0027
apply odd_mul_odd - 0028
exact hp - 0029
exact hq