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_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))))Structural proof guide
Generated structural guide
Multiplication by an odd natural preserves and reflects oddness.
Use the direct prerequisites parity_cases, even_mul_right, odd_not_even, odd_mul_odd 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–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.
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 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
exfalso - 0012
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