PA00CC

odd_division_even_iff

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

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

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_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))))

Structural proof guide

Generated structural guide

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

Use the direct prerequisites odd_multiplier_even_product_iff, odd_multiplier_odd_product_iff, even_sum_iff_same_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 PA00CB even_sum_iff_same_parity

Proof neighborhood

Direct dependencies

PA00C7 odd_multiplier_even_product_iff PA00C8 odd_multiplier_odd_product_iff PA00CB even_sum_iff_same_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 iffeven sum iff same 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 : (Even(p · q + r) → Even(p · q) ∧ Even(r) ∨ Odd(p · q) ∧ Odd(r)) ∧ (Even(p · q) ∧ Even(r) ∨ Odd(p · q) ∧ Odd(r) → Even(p · q + r))Definitions: EvenOdd
  2. L18
    specialize even_sum_iff_same_parity (p * q)
  3. L19
    specialize even_sum_iff_same_parity r
  4. L20
    exact even_sum_iff_same_parity
05Establish hrightL21–24

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

  1. L21
    have hright : (Even(q + r) → Even(q) ∧ Even(r) ∨ Odd(q) ∧ Odd(r)) ∧ (Even(q) ∧ Even(r) ∨ Odd(q) ∧ Odd(r) → Even(q + r))Definitions: EvenOdd
  2. L22
    specialize even_sum_iff_same_parity q
  3. L23
    specialize even_sum_iff_same_parity r
  4. L24
    exact even_sum_iff_same_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_even_proof_pqr_even. p * q + r = 2 * pod_even_proof_pqr_even
  2. L32
    rewrite <- hdivision
  3. L33
    exact hn
  4. L34
    apply hright_right
09Establish hsameL35–37

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

  1. L35
    have hsame : (((exists pod_even_proof_pq_even. p * q = 2 * pod_even_proof_pq_even) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)) \/ ((exists pod_odd_proof_pq_odd. p * q = 2 * pod_odd_proof_pq_odd + 1) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)))
  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 hsame
  2. L39
    cases hsame_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 hsame_left_left
  3. L44
    exact hsame_left_right
12Separate the logical casesL45–47

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

  1. L45
    cases hsame_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 hsame_right_left
  3. L50
    exact hsame_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_even_proof_pqr_even. p * q + r = 2 * pod_even_proof_pqr_even
  2. L53
    apply hleft_right
16Establish hsameL54–56

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

  1. L54
    have hsame : (((exists pod_even_proof_q_even. q = 2 * pod_even_proof_q_even) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)) \/ ((exists pod_odd_proof_q_odd. q = 2 * pod_odd_proof_q_odd + 1) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)))
  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 hsame
  2. L58
    cases hsame_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 hsame_left_left
  3. L63
    exact hsame_left_right
19Separate the logical casesL64–66

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

  1. L64
    cases hsame_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 hsame_right_left
  3. L69
    exact hsame_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_even_proof_pqr_even. p * q + r = 2 * pod_even_proof_pqr_even) -> ((((exists pod_even_proof_pq_even. p * q = 2 * pod_even_proof_pq_even) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)) \/ ((exists pod_odd_proof_pq_odd. p * q = 2 * pod_odd_proof_pq_odd + 1) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1))))) /\ (((((exists pod_even_proof_pq_even. p * q = 2 * pod_even_proof_pq_even) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)) \/ ((exists pod_odd_proof_pq_odd. p * q = 2 * pod_odd_proof_pq_odd + 1) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)))) -> (exists pod_even_proof_pqr_even. p * q + r = 2 * pod_even_proof_pqr_even)))
  18. 0018specialize even_sum_iff_same_parity (p * q)
  19. 0019specialize even_sum_iff_same_parity r
  20. 0020exact even_sum_iff_same_parity
  21. 0021have hright : (((exists pod_even_proof_qr_even. q + r = 2 * pod_even_proof_qr_even) -> ((((exists pod_even_proof_q_even. q = 2 * pod_even_proof_q_even) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)) \/ ((exists pod_odd_proof_q_odd. q = 2 * pod_odd_proof_q_odd + 1) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1))))) /\ (((((exists pod_even_proof_q_even. q = 2 * pod_even_proof_q_even) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)) \/ ((exists pod_odd_proof_q_odd. q = 2 * pod_odd_proof_q_odd + 1) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)))) -> (exists pod_even_proof_qr_even. q + r = 2 * pod_even_proof_qr_even)))
  22. 0022specialize even_sum_iff_same_parity q
  23. 0023specialize even_sum_iff_same_parity r
  24. 0024exact even_sum_iff_same_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_even_proof_pqr_even. p * q + r = 2 * pod_even_proof_pqr_even
  32. 0032rewrite <- hdivision
  33. 0033exact hn
  34. 0034apply hright_right
  35. 0035have hsame : (((exists pod_even_proof_pq_even. p * q = 2 * pod_even_proof_pq_even) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)) \/ ((exists pod_odd_proof_pq_odd. p * q = 2 * pod_odd_proof_pq_odd + 1) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)))
  36. 0036apply hleft_left
  37. 0037exact hpqr
  38. 0038cases hsame
  39. 0039cases hsame_left
  40. 0040left
  41. 0041split
  42. 0042apply hmul_even_left
  43. 0043exact hsame_left_left
  44. 0044exact hsame_left_right
  45. 0045cases hsame_right
  46. 0046right
  47. 0047split
  48. 0048apply hmul_odd_left
  49. 0049exact hsame_right_left
  50. 0050exact hsame_right_right
  51. 0051intro hqr
  52. 0052have hpqr : exists pod_even_proof_pqr_even. p * q + r = 2 * pod_even_proof_pqr_even
  53. 0053apply hleft_right
  54. 0054have hsame : (((exists pod_even_proof_q_even. q = 2 * pod_even_proof_q_even) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)) \/ ((exists pod_odd_proof_q_odd. q = 2 * pod_odd_proof_q_odd + 1) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)))
  55. 0055apply hright_left
  56. 0056exact hqr
  57. 0057cases hsame
  58. 0058cases hsame_left
  59. 0059left
  60. 0060split
  61. 0061apply hmul_even_right
  62. 0062exact hsame_left_left
  63. 0063exact hsame_left_right
  64. 0064cases hsame_right
  65. 0065right
  66. 0066split
  67. 0067apply hmul_odd_right
  68. 0068exact hsame_right_left
  69. 0069exact hsame_right_right
  70. 0070rewrite hdivision
  71. 0071exact hpqr