PA00CK · theorem

odd_product_division_mod_two

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

Odd scale and modulus transport an exact division equation to x == q+r modulo two.

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. ∀ a. ∀ x. ∀ q. ∀ r. Odd(p) → Odd(a) → a · x = p · q + r → ModEq(2,x,q + r)

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

PD0008 ModEq PD0010 Odd

3 occurrences

In local proof propositions

PD0009 Even PD0010 Odd

24 occurrences

Exact expanded native-PA statement
forall p a x q r. (exists sdp_odd_prime_like_modulus. p = 2 * sdp_odd_prime_like_modulus + 1) -> (exists sdp_odd_scale. a = 2 * sdp_odd_scale + 1) -> a * x = p * q + r -> (exists sdp_u_product_division_result sdp_v_product_division_result. (x) + 2 * sdp_u_product_division_result = (q + r) + 2 * sdp_v_product_division_result)

Proof neighborhood

Direct theorem prerequisites

PA0057 parity_cases PA00C9 odd_multiplier_parity_iff PA00CG odd_division_parity_iff PA00CJ matching_parity_mod_two

Direct theorem dependents

PA00CN odd_scaled_division_signed_mod_two

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

58 script commands · 18 reading checkpoints · 5 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 (4)
parity casesodd multiplier parity iffodd division parity iffmatching parity mod two
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro x
  4. L4
    intro q
  5. L5
    intro r
  6. L6
    intro hp
  7. L7
    intro ha
  8. L8
    intro hdivision
02Establish hproductL9–13

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

  1. L9
    have hproduct : (Even(a · x) → Even(x)) ∧ (Even(x) → Even(a · x)) ∧ ((Odd(a · x) → Odd(x)) ∧ (Odd(x) → Odd(a · x)))Definitions: Even(a · x)Even(x)Odd(a · x)Odd(x)Original native command in the exact edition
  2. L10
    specialize odd_multiplier_parity_iff a
  3. L11
    specialize odd_multiplier_parity_iff x
  4. L12
    apply odd_multiplier_parity_iff
  5. L13
    exact ha
03Establish hquotientL14–21

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

  1. L14
    have hquotient : (Even(a · x) → Even(q + r)) ∧ (Even(q + r) → Even(a · x)) ∧ ((Odd(a · x) → Odd(q + r)) ∧ (Odd(q + r) → Odd(a · x)))Definitions: Even(a · x)Even(q + r)Odd(a · x)Odd(q + r)Original native command in the exact edition
  2. L15
    specialize odd_division_parity_iff p
  3. L16
    specialize odd_division_parity_iff q
  4. L17
    specialize odd_division_parity_iff r
  5. L18
    specialize odd_division_parity_iff (a * x)
  6. L19
    apply odd_division_parity_iff
  7. L20
    exact hp
  8. L21
    exact hdivision
04Separate the logical casesL22–27

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

  1. L22
    cases hproduct
  2. L23
    cases hproduct_left
  3. L24
    cases hproduct_right
  4. L25
    cases hquotient
  5. L26
    cases hquotient_left
  6. L27
    cases hquotient_right
05Establish hxcasesL28–30

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

  1. L28
    have hxcases : exists k. x = 2 * k \/ x = 2 * k + 1
  2. L29
    specialize parity_cases x
  3. L30
    exact parity_cases
06Separate the logical casesL31–32

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

  1. L31
    cases hxcases
  2. L32
    cases hxcases_witness
07Establish hmatchingL33–33

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

  1. L33
    have hmatching : Even(x) ∧ Even(q + r) ∨ Odd(x) ∧ Odd(q + r)Definitions: Even(x)Even(q + r)Odd(x)Odd(q + r)Original native command in the exact edition
08Separate the logical casesL34–35

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

  1. L34
    left
  2. L35
    split
09Construct an explicit witnessL36–36

Supply the displayed value, then prove that it has the required property.

  1. L36
    exists x1
10Use earlier factsL37–39

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

  1. L37
    exact hxcases_witness_left
  2. L38
    apply hquotient_left_left
  3. L39
    apply hproduct_left_right
11Construct an explicit witnessL40–40

Supply the displayed value, then prove that it has the required property.

  1. L40
    exists x1
12Use earlier factsL41–45

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

  1. L41
    exact hxcases_witness_left
  2. L42
    specialize matching_parity_mod_two x
  3. L43
    specialize matching_parity_mod_two (q + r)
  4. L44
    apply matching_parity_mod_two
  5. L45
    exact hmatching
13Establish hmatchingL46–46

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

  1. L46
    have hmatching : Even(x) ∧ Even(q + r) ∨ Odd(x) ∧ Odd(q + r)Definitions: Even(x)Even(q + r)Odd(x)Odd(q + r)Original native command in the exact edition
14Separate the logical casesL47–48

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

  1. L47
    right
  2. L48
    split
15Construct an explicit witnessL49–49

Supply the displayed value, then prove that it has the required property.

  1. L49
    exists x1
16Use earlier factsL50–52

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

  1. L50
    exact hxcases_witness_right
  2. L51
    apply hquotient_right_left
  3. L52
    apply hproduct_right_right
17Construct an explicit witnessL53–53

Supply the displayed value, then prove that it has the required property.

  1. L53
    exists x1
18Use earlier factsL54–58

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

  1. L54
    exact hxcases_witness_right
  2. L55
    specialize matching_parity_mod_two x
  3. L56
    specialize matching_parity_mod_two (q + r)
  4. L57
    apply matching_parity_mod_two
  5. L58
    exact hmatching

Library-wide reading audit

Original defined command ledger · 58 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro x
  4. 0004intro q
  5. 0005intro r
  6. 0006intro hp
  7. 0007intro ha
  8. 0008intro hdivision
  9. 0009have hproduct : (Even(a · x) → Even(x)) ∧ (Even(x) → Even(a · x)) ∧ ((Odd(a · x) → Odd(x)) ∧ (Odd(x) → Odd(a · x)))
    Exact native replay linehave hproduct : ((((exists sdp_even_proof_ax_even. a * x = 2 * sdp_even_proof_ax_even) -> (exists sdp_even_proof_x_even. x = 2 * sdp_even_proof_x_even)) /\ ((exists sdp_even_proof_x_even. x = 2 * sdp_even_proof_x_even) -> (exists sdp_even_proof_ax_even. a * x = 2 * sdp_even_proof_ax_even))) /\ (((exists sdp_odd_proof_ax_odd. a * x = 2 * sdp_odd_proof_ax_odd + 1) -> (exists sdp_odd_proof_x_odd. x = 2 * sdp_odd_proof_x_odd + 1)) /\ ((exists sdp_odd_proof_x_odd. x = 2 * sdp_odd_proof_x_odd + 1) -> (exists sdp_odd_proof_ax_odd. a * x = 2 * sdp_odd_proof_ax_odd + 1))))
  10. 0010specialize odd_multiplier_parity_iff a
  11. 0011specialize odd_multiplier_parity_iff x
  12. 0012apply odd_multiplier_parity_iff
  13. 0013exact ha
  14. 0014have hquotient : (Even(a · x) → Even(q + r)) ∧ (Even(q + r) → Even(a · x)) ∧ ((Odd(a · x) → Odd(q + r)) ∧ (Odd(q + r) → Odd(a · x)))
    Exact native replay linehave hquotient : ((((exists sdp_even_proof_ax_even. a * x = 2 * sdp_even_proof_ax_even) -> (exists sdp_even_proof_qr_even. q + r = 2 * sdp_even_proof_qr_even)) /\ ((exists sdp_even_proof_qr_even. q + r = 2 * sdp_even_proof_qr_even) -> (exists sdp_even_proof_ax_even. a * x = 2 * sdp_even_proof_ax_even))) /\ (((exists sdp_odd_proof_ax_odd. a * x = 2 * sdp_odd_proof_ax_odd + 1) -> (exists sdp_odd_proof_qr_odd. q + r = 2 * sdp_odd_proof_qr_odd + 1)) /\ ((exists sdp_odd_proof_qr_odd. q + r = 2 * sdp_odd_proof_qr_odd + 1) -> (exists sdp_odd_proof_ax_odd. a * x = 2 * sdp_odd_proof_ax_odd + 1))))
  15. 0015specialize odd_division_parity_iff p
  16. 0016specialize odd_division_parity_iff q
  17. 0017specialize odd_division_parity_iff r
  18. 0018specialize odd_division_parity_iff (a * x)
  19. 0019apply odd_division_parity_iff
  20. 0020exact hp
  21. 0021exact hdivision
  22. 0022cases hproduct
  23. 0023cases hproduct_left
  24. 0024cases hproduct_right
  25. 0025cases hquotient
  26. 0026cases hquotient_left
  27. 0027cases hquotient_right
  28. 0028have hxcases : exists k. x = 2 * k \/ x = 2 * k + 1
  29. 0029specialize parity_cases x
  30. 0030exact parity_cases
  31. 0031cases hxcases
  32. 0032cases hxcases_witness
  33. 0033have hmatching : Even(x) ∧ Even(q + r) ∨ Odd(x) ∧ Odd(q + r)
    Exact native replay linehave hmatching : (((exists sdp_even_proof_x_even. x = 2 * sdp_even_proof_x_even) /\ (exists sdp_even_proof_qr_even. q + r = 2 * sdp_even_proof_qr_even)) \/ ((exists sdp_odd_proof_x_odd. x = 2 * sdp_odd_proof_x_odd + 1) /\ (exists sdp_odd_proof_qr_odd. q + r = 2 * sdp_odd_proof_qr_odd + 1)))
  34. 0034left
  35. 0035split
  36. 0036exists x1
  37. 0037exact hxcases_witness_left
  38. 0038apply hquotient_left_left
  39. 0039apply hproduct_left_right
  40. 0040exists x1
  41. 0041exact hxcases_witness_left
  42. 0042specialize matching_parity_mod_two x
  43. 0043specialize matching_parity_mod_two (q + r)
  44. 0044apply matching_parity_mod_two
  45. 0045exact hmatching
  46. 0046have hmatching : Even(x) ∧ Even(q + r) ∨ Odd(x) ∧ Odd(q + r)
    Exact native replay linehave hmatching : (((exists sdp_even_proof_x_even. x = 2 * sdp_even_proof_x_even) /\ (exists sdp_even_proof_qr_even. q + r = 2 * sdp_even_proof_qr_even)) \/ ((exists sdp_odd_proof_x_odd. x = 2 * sdp_odd_proof_x_odd + 1) /\ (exists sdp_odd_proof_qr_odd. q + r = 2 * sdp_odd_proof_qr_odd + 1)))
  47. 0047right
  48. 0048split
  49. 0049exists x1
  50. 0050exact hxcases_witness_right
  51. 0051apply hquotient_right_left
  52. 0052apply hproduct_right_right
  53. 0053exists x1
  54. 0054exact hxcases_witness_right
  55. 0055specialize matching_parity_mod_two x
  56. 0056specialize matching_parity_mod_two (q + r)
  57. 0057apply matching_parity_mod_two
  58. 0058exact hmatching