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.
Exact expanded 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))))Structural proof guide
Generated structural guide
Multiplication by an odd natural preserves and reflects evenness.
Use the direct prerequisites parity_cases, odd_mul_odd, even_not_odd, even_mul_right as previously established PA formulas.
The proof proceeds by case analysis (2), intermediate claims (2).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.
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 exact 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 : 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