PA00CF · theorem

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.

Statement with defined notation

∀ p. ∀ q. ∀ r. ∀ n. Odd(p) → n = p · q + r → (Odd(n) → Odd(q + r)) ∧ (Odd(q + r) → Odd(n))

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0010 Odd

5 occurrences

In local proof propositions

PD0009 Even PD0010 Odd

38 occurrences

Exact expanded native-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))))

Proof neighborhood

Direct theorem prerequisites

PA00C7 odd_multiplier_even_product_iff PA00C8 odd_multiplier_odd_product_iff PA00CE odd_sum_iff_opposite_parity

Direct theorem dependents

PA00CG odd_division_parity_iff

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (3)
odd multiplier even product iffodd multiplier odd product iffodd sum iff opposite parity
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 : (Even(p · q) → Even(q)) ∧ (Even(q) → Even(p · q))Definitions: Even(p · q)Even(q)Original native command in the exact edition
  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 : (Odd(p · q) → Odd(q)) ∧ (Odd(q) → Odd(p · q))Definitions: Odd(p · q)Odd(q)Original native command in the exact edition
  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: Odd(p · q + r)Even(p · q)Odd(r)Odd(p · q)Even(r)Original native command in the exact edition
  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: Odd(q + r)Even(q)Odd(r)Odd(q)Even(r)Original native command in the exact edition
  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 : Odd(p · q + r)Definitions: Odd(p · q + r)Original native command in the exact edition
  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 : Even(p · q) ∧ Odd(r) ∨ Odd(p · q) ∧ Even(r)Definitions: Even(p · q)Odd(r)Odd(p · q)Even(r)Original native command in the exact edition
  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 : Odd(p · q + r)Definitions: Odd(p · q + r)Original native command in the exact edition
  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 : Even(q) ∧ Odd(r) ∨ Odd(q) ∧ Even(r)Definitions: Even(q)Odd(r)Odd(q)Even(r)Original native command in the exact edition
  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 defined 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 : (Even(p · q) → Even(q)) ∧ (Even(q) → Even(p · q))
    Exact native replay linehave 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 : (Odd(p · q) → Odd(q)) ∧ (Odd(q) → Odd(p · q))
    Exact native replay linehave 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 : (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))
    Exact native replay linehave 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 : (Odd(q + r) → Even(q) ∧ Odd(r) ∨ Odd(q) ∧ Even(r)) ∧ (Even(q) ∧ Odd(r) ∨ Odd(q) ∧ Even(r) → Odd(q + r))
    Exact native replay linehave 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 : Odd(p · q + r)
    Exact native replay linehave 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 : Even(p · q) ∧ Odd(r) ∨ Odd(p · q) ∧ Even(r)
    Exact native replay linehave 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 : Odd(p · q + r)
    Exact native replay linehave hpqr : exists pod_odd_proof_pqr_odd. p * q + r = 2 * pod_odd_proof_pqr_odd + 1
  53. 0053apply hleft_right
  54. 0054have hopposite : Even(q) ∧ Odd(r) ∨ Odd(q) ∧ Even(r)
    Exact native replay linehave 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