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) → (Even(p · q) → Even(q)) ∧ (Even(q) → Even(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_even_product_even. p * q = 2 * pod_even_product_even) -> (exists pod_even_factor_even. q = 2 * pod_even_factor_even)) /\ ((exists pod_even_factor_even. q = 2 * pod_even_factor_even) -> (exists pod_even_product_even. p * q = 2 * pod_even_product_even))))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–10
06Construct an explicit witnessL11–11
Supply the displayed value, then prove that it has the required property.
- L11
exists x
07Use earlier factsL12–12
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L12
exact hqcases_witness_left
08Separate the logical casesL13–13
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L13
exfalso
09Establish hproduct_oddL14–18
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd mul odd.
10Construct an explicit witnessL19–19
Supply the displayed value, then prove that it has the required property.
- L19
exists x
11Use earlier factsL20–24
12Fix variables and assumptionsL25–25
Work with arbitrary variables or the premises of the current implication.
- L25
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
exists x - 0012
exact hqcases_witness_left - 0013
exfalso - 0014
have hproduct_odd : Odd(p · q)Exact native replay line
have hproduct_odd : exists pod_odd_even_iff_contradiction. p * q = 2 * pod_odd_even_iff_contradiction + 1 - 0015
specialize odd_mul_odd p - 0016
specialize odd_mul_odd q - 0017
apply odd_mul_odd - 0018
exact hp - 0019
exists x - 0020
exact hqcases_witness_right - 0021
specialize even_not_odd (p * q) - 0022
apply even_not_odd - 0023
exact hproduct - 0024
exact hproduct_odd - 0025
intro hq - 0026
specialize even_mul_right p - 0027
specialize even_mul_right q - 0028
apply even_mul_right - 0029
exact hq