PA00CF

odd_division_odd_iff

Alpha v34 checked-use theorem · independently closed; not Stable

For odd divisor coefficient p, n=p*q+r is odd exactly when q+r is odd.

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 r n. (exists pod_odd_multiplier. p = 2 * pod_odd_multiplier + 1) -> n = p * q + r -> ((((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

For odd divisor coefficient p, n=p*q+r is odd exactly when q+r is odd.

Use the direct prerequisites odd_multiplier_even_product_iff, odd_multiplier_odd_product_iff, odd_sum_iff_opposite_parity as previously established PA formulas.

The proof proceeds by case analysis (10), intermediate claims (8), equality transport (2).

Referenced ingredients

PA00C7 odd_multiplier_even_product_iff PA00C8 odd_multiplier_odd_product_iff PA00CE odd_sum_iff_opposite_parity

Proof neighborhood

Direct dependencies

PA00C7 odd_multiplier_even_product_iff PA00C8 odd_multiplier_odd_product_iff PA00CE odd_sum_iff_opposite_parity

Direct dependents

PA00CG odd_division_parity_iff

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

71 script commands · 22 reading checkpoints · 8 local claims

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 (3)
odd multiplier even product iffodd multiplier odd product iffodd sum iff opposite parity

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–6

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro r
  4. L4
    intro n
  5. L5
    intro hp
  6. L6
    intro hdivision
02Establish hmul_evenL7–11

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd multiplier even product iff.

  1. L7
    have hmul_even : (((exists pod_even_proof_pq_even. p * q = 2 * pod_even_proof_pq_even) -> (exists pod_even_proof_q_even. q = 2 * pod_even_proof_q_even)) /\ ((exists pod_even_proof_q_even. q = 2 * pod_even_proof_q_even) -> (exists pod_even_proof_pq_even. p * q = 2 * pod_even_proof_pq_even)))
  2. L8
    specialize odd_multiplier_even_product_iff p
  3. L9
    specialize odd_multiplier_even_product_iff q
  4. L10
    apply odd_multiplier_even_product_iff
  5. L11
    exact hp
03Establish hmul_oddL12–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd multiplier odd product iff.

  1. L12
    have hmul_odd : (((exists pod_odd_proof_pq_odd. p * q = 2 * pod_odd_proof_pq_odd + 1) -> (exists pod_odd_proof_q_odd. q = 2 * pod_odd_proof_q_odd + 1)) /\ ((exists pod_odd_proof_q_odd. q = 2 * pod_odd_proof_q_odd + 1) -> (exists pod_odd_proof_pq_odd. p * q = 2 * pod_odd_proof_pq_odd + 1)))
  2. L13
    specialize odd_multiplier_odd_product_iff p
  3. L14
    specialize odd_multiplier_odd_product_iff q
  4. L15
    apply odd_multiplier_odd_product_iff
  5. L16
    exact hp
04Establish hleftL17–20

Establish this local claim before using it. It is not an additional assumption.

  1. L17
    have hleft : (Odd(p · q + r) → Even(p · q) ∧ Odd(r) ∨ Odd(p · q) ∧ Even(r)) ∧ (Even(p · q) ∧ Odd(r) ∨ Odd(p · q) ∧ Even(r) → Odd(p · q + r))Definitions: EvenOdd
  2. L18
    specialize odd_sum_iff_opposite_parity (p * q)
  3. L19
    specialize odd_sum_iff_opposite_parity r
  4. L20
    exact odd_sum_iff_opposite_parity
05Establish hrightL21–24

Establish this local claim before using it. It is not an additional assumption.

  1. L21
    have hright : (Odd(q + r) → Even(q) ∧ Odd(r) ∨ Odd(q) ∧ Even(r)) ∧ (Even(q) ∧ Odd(r) ∨ Odd(q) ∧ Even(r) → Odd(q + r))Definitions: EvenOdd
  2. L22
    specialize odd_sum_iff_opposite_parity q
  3. L23
    specialize odd_sum_iff_opposite_parity r
  4. L24
    exact odd_sum_iff_opposite_parity
06Separate the logical casesL25–29

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L25
    cases hmul_even
  2. L26
    cases hmul_odd
  3. L27
    cases hleft
  4. L28
    cases hright
  5. L29
    split
07Fix variables and assumptionsL30–30

Work with arbitrary variables or the premises of the current implication.

  1. L30
    intro hn
08Establish hpqrL31–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hright right.

  1. L31
    have hpqr : exists pod_odd_proof_pqr_odd. p * q + r = 2 * pod_odd_proof_pqr_odd + 1
  2. L32
    rewrite <- hdivision
  3. L33
    exact hn
  4. L34
    apply hright_right
09Establish hoppositeL35–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hleft left.

  1. L35
    have hopposite : (((exists pod_even_proof_pq_even. p * q = 2 * pod_even_proof_pq_even) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)) \/ ((exists pod_odd_proof_pq_odd. p * q = 2 * pod_odd_proof_pq_odd + 1) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)))
  2. L36
    apply hleft_left
  3. L37
    exact hpqr
10Separate the logical casesL38–41

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L38
    cases hopposite
  2. L39
    cases hopposite_left
  3. L40
    left
  4. L41
    split
11Use earlier factsL42–44

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L42
    apply hmul_even_left
  2. L43
    exact hopposite_left_left
  3. L44
    exact hopposite_left_right
12Separate the logical casesL45–47

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L45
    cases hopposite_right
  2. L46
    right
  3. L47
    split
13Use earlier factsL48–50

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L48
    apply hmul_odd_left
  2. L49
    exact hopposite_right_left
  3. L50
    exact hopposite_right_right
14Fix variables and assumptionsL51–51

Work with arbitrary variables or the premises of the current implication.

  1. L51
    intro hqr
15Establish hpqrL52–53

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hleft right.

  1. L52
    have hpqr : exists pod_odd_proof_pqr_odd. p * q + r = 2 * pod_odd_proof_pqr_odd + 1
  2. L53
    apply hleft_right
16Establish hoppositeL54–56

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hright left.

  1. L54
    have hopposite : (((exists pod_even_proof_q_even. q = 2 * pod_even_proof_q_even) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)) \/ ((exists pod_odd_proof_q_odd. q = 2 * pod_odd_proof_q_odd + 1) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)))
  2. L55
    apply hright_left
  3. L56
    exact hqr
17Separate the logical casesL57–60

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L57
    cases hopposite
  2. L58
    cases hopposite_left
  3. L59
    left
  4. L60
    split
18Use earlier factsL61–63

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L61
    apply hmul_even_right
  2. L62
    exact hopposite_left_left
  3. L63
    exact hopposite_left_right
19Separate the logical casesL64–66

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L64
    cases hopposite_right
  2. L65
    right
  3. L66
    split
20Use earlier factsL67–69

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L67
    apply hmul_odd_right
  2. L68
    exact hopposite_right_left
  3. L69
    exact hopposite_right_right
21Calculate and transport equalitiesL70–70

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L70
    rewrite hdivision
22Use earlier factsL71–71

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L71
    exact hpqr

Library-wide reading audit

Original exact command ledger · 71 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro r
  4. 0004intro n
  5. 0005intro hp
  6. 0006intro hdivision
  7. 0007have hmul_even : (((exists pod_even_proof_pq_even. p * q = 2 * pod_even_proof_pq_even) -> (exists pod_even_proof_q_even. q = 2 * pod_even_proof_q_even)) /\ ((exists pod_even_proof_q_even. q = 2 * pod_even_proof_q_even) -> (exists pod_even_proof_pq_even. p * q = 2 * pod_even_proof_pq_even)))
  8. 0008specialize odd_multiplier_even_product_iff p
  9. 0009specialize odd_multiplier_even_product_iff q
  10. 0010apply odd_multiplier_even_product_iff
  11. 0011exact hp
  12. 0012have hmul_odd : (((exists pod_odd_proof_pq_odd. p * q = 2 * pod_odd_proof_pq_odd + 1) -> (exists pod_odd_proof_q_odd. q = 2 * pod_odd_proof_q_odd + 1)) /\ ((exists pod_odd_proof_q_odd. q = 2 * pod_odd_proof_q_odd + 1) -> (exists pod_odd_proof_pq_odd. p * q = 2 * pod_odd_proof_pq_odd + 1)))
  13. 0013specialize odd_multiplier_odd_product_iff p
  14. 0014specialize odd_multiplier_odd_product_iff q
  15. 0015apply odd_multiplier_odd_product_iff
  16. 0016exact hp
  17. 0017have hleft : (((exists pod_odd_proof_pqr_odd. p * q + r = 2 * pod_odd_proof_pqr_odd + 1) -> ((((exists pod_even_proof_pq_even. p * q = 2 * pod_even_proof_pq_even) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)) \/ ((exists pod_odd_proof_pq_odd. p * q = 2 * pod_odd_proof_pq_odd + 1) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even))))) /\ (((((exists pod_even_proof_pq_even. p * q = 2 * pod_even_proof_pq_even) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)) \/ ((exists pod_odd_proof_pq_odd. p * q = 2 * pod_odd_proof_pq_odd + 1) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)))) -> (exists pod_odd_proof_pqr_odd. p * q + r = 2 * pod_odd_proof_pqr_odd + 1)))
  18. 0018specialize odd_sum_iff_opposite_parity (p * q)
  19. 0019specialize odd_sum_iff_opposite_parity r
  20. 0020exact odd_sum_iff_opposite_parity
  21. 0021have hright : (((exists pod_odd_proof_qr_odd. q + r = 2 * pod_odd_proof_qr_odd + 1) -> ((((exists pod_even_proof_q_even. q = 2 * pod_even_proof_q_even) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)) \/ ((exists pod_odd_proof_q_odd. q = 2 * pod_odd_proof_q_odd + 1) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even))))) /\ (((((exists pod_even_proof_q_even. q = 2 * pod_even_proof_q_even) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)) \/ ((exists pod_odd_proof_q_odd. q = 2 * pod_odd_proof_q_odd + 1) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)))) -> (exists pod_odd_proof_qr_odd. q + r = 2 * pod_odd_proof_qr_odd + 1)))
  22. 0022specialize odd_sum_iff_opposite_parity q
  23. 0023specialize odd_sum_iff_opposite_parity r
  24. 0024exact odd_sum_iff_opposite_parity
  25. 0025cases hmul_even
  26. 0026cases hmul_odd
  27. 0027cases hleft
  28. 0028cases hright
  29. 0029split
  30. 0030intro hn
  31. 0031have hpqr : exists pod_odd_proof_pqr_odd. p * q + r = 2 * pod_odd_proof_pqr_odd + 1
  32. 0032rewrite <- hdivision
  33. 0033exact hn
  34. 0034apply hright_right
  35. 0035have hopposite : (((exists pod_even_proof_pq_even. p * q = 2 * pod_even_proof_pq_even) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)) \/ ((exists pod_odd_proof_pq_odd. p * q = 2 * pod_odd_proof_pq_odd + 1) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)))
  36. 0036apply hleft_left
  37. 0037exact hpqr
  38. 0038cases hopposite
  39. 0039cases hopposite_left
  40. 0040left
  41. 0041split
  42. 0042apply hmul_even_left
  43. 0043exact hopposite_left_left
  44. 0044exact hopposite_left_right
  45. 0045cases hopposite_right
  46. 0046right
  47. 0047split
  48. 0048apply hmul_odd_left
  49. 0049exact hopposite_right_left
  50. 0050exact hopposite_right_right
  51. 0051intro hqr
  52. 0052have hpqr : exists pod_odd_proof_pqr_odd. p * q + r = 2 * pod_odd_proof_pqr_odd + 1
  53. 0053apply hleft_right
  54. 0054have hopposite : (((exists pod_even_proof_q_even. q = 2 * pod_even_proof_q_even) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)) \/ ((exists pod_odd_proof_q_odd. q = 2 * pod_odd_proof_q_odd + 1) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)))
  55. 0055apply hright_left
  56. 0056exact hqr
  57. 0057cases hopposite
  58. 0058cases hopposite_left
  59. 0059left
  60. 0060split
  61. 0061apply hmul_even_right
  62. 0062exact hopposite_left_left
  63. 0063exact hopposite_left_right
  64. 0064cases hopposite_right
  65. 0065right
  66. 0066split
  67. 0067apply hmul_odd_right
  68. 0068exact hopposite_right_left
  69. 0069exact hopposite_right_right
  70. 0070rewrite hdivision
  71. 0071exact hpqr