Exact expanded PA statement
forall p q r n. (exists pod_odd_multiplier. p = 2 * pod_odd_multiplier + 1) -> n = p * q + r -> (((((exists pod_even_division_n_even. n = 2 * pod_even_division_n_even) -> (exists pod_even_division_qr_even. q + r = 2 * pod_even_division_qr_even)) /\ ((exists pod_even_division_qr_even. q + r = 2 * pod_even_division_qr_even) -> (exists pod_even_division_n_even. n = 2 * pod_even_division_n_even)))) /\ ((((exists pod_odd_division_n_odd. n = 2 * pod_odd_division_n_odd + 1) -> (exists pod_odd_division_qr_odd. q + r = 2 * pod_odd_division_qr_odd + 1)) /\ ((exists pod_odd_division_qr_odd. q + r = 2 * pod_odd_division_qr_odd + 1) -> (exists pod_odd_division_n_odd. n = 2 * pod_odd_division_n_odd + 1)))))Structural proof guide
Generated structural guide
An exact quotient-remainder equation with odd coefficient preserves the complete parity classification.
Use the direct prerequisites odd_division_even_iff, odd_division_odd_iff as previously established PA formulas.
The proof proceeds by direct introduction and elimination.
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-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.
- 0001
intro p - 0002
intro q - 0003
intro r - 0004
intro n - 0005
intro hp - 0006
intro hdivision - 0007
split - 0008
specialize odd_division_even_iff p - 0009
specialize odd_division_even_iff q - 0010
specialize odd_division_even_iff r - 0011
specialize odd_division_even_iff n - 0012
apply odd_division_even_iff - 0013
exact hp - 0014
exact hdivision - 0015
specialize odd_division_odd_iff p - 0016
specialize odd_division_odd_iff q - 0017
specialize odd_division_odd_iff r - 0018
specialize odd_division_odd_iff n - 0019
apply odd_division_odd_iff - 0020
exact hp - 0021
exact hdivision