PA00CM · theorem

signed_remainder_sum_mod_two

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

A lower/reflected signed remainder changes q+r to q+m+s only by an even amount.

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. ∀ m. ∀ s. Odd(p) → s = 0 ∧ r = m ∨ s = 1 ∧ r + m = p → ModEq(2,q + r,q + m + s)

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

2 occurrences

In local proof propositions

PD0008 ModEq

3 occurrences

Exact expanded native-PA statement
forall p q r m s. (exists sdp_odd_prime_like_modulus. p = 2 * sdp_odd_prime_like_modulus + 1) -> (((s = 0 /\ r = m) \/ (s = 1 /\ r + m = p))) -> (exists sdp_u_signed_sum_result sdp_v_signed_sum_result. (q + r) + 2 * sdp_u_signed_sum_result = (q + m + s) + 2 * sdp_v_signed_sum_result)

Proof neighborhood

Direct theorem prerequisites

PA00CL odd_reflected_remainder_mod_two PA0023 mod_eq_refl PA0022 mod_eq_add PA0009 add_assoc

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

44 script commands · 13 reading checkpoints · 3 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)
odd reflected remainder mod twomod eq reflmod eq addadd assoc
01Fix variables and assumptionsL1–7

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 m
  5. L5
    intro s
  6. L6
    intro hp
  7. L7
    intro hbranch
02Separate the logical casesL8–9

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

  1. L8
    cases hbranch
  2. L9
    cases hbranch_left
03Calculate and transport equalitiesL10–11

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

  1. L10
    rewrite hbranch_left_left
  2. L11
    rewrite hbranch_left_right
04Construct an explicit witnessL12–13

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

  1. L12
    exists 0
  2. L13
    exists 0
05Calculate and transport equalitiesL14–16

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

  1. L14
    rewrite PA5
  2. L15
    rewrite PA5
  3. L16
    symm
06Use earlier factsL17–17

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

  1. L17
    apply PA3
07Separate the logical casesL18–18

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

  1. L18
    cases hbranch_right
08Establish hrmodL19–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd reflected remainder mod two.

  1. L19
    have hrmod : ModEq(2,r,m + 1)Definitions: ModEq(2,r,m + 1)Original native command in the exact edition
  2. L20
    specialize odd_reflected_remainder_mod_two p
  3. L21
    specialize odd_reflected_remainder_mod_two r
  4. L22
    specialize odd_reflected_remainder_mod_two m
  5. L23
    apply odd_reflected_remainder_mod_two
  6. L24
    exact hp
  7. L25
    exact hbranch_right_right
09Establish hqmodL26–29

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

  1. L26
    have hqmod : ModEq(2,q,q)Definitions: ModEq(2,q,q)Original native command in the exact edition
  2. L27
    specialize mod_eq_refl 2
  3. L28
    specialize mod_eq_refl q
  4. L29
    exact mod_eq_refl
10Establish hsumL30–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq add.

  1. L30
    have hsum : ModEq(2,q + r,q + (m + 1))Definitions: ModEq(2,q + r,q + (m + 1))Original native command in the exact edition
  2. L31
    specialize mod_eq_add 2
  3. L32
    specialize mod_eq_add q
  4. L33
    specialize mod_eq_add q
  5. L34
    specialize mod_eq_add r
  6. L35
    specialize mod_eq_add (m + 1)
  7. L36
    apply mod_eq_add
  8. L37
    exact hqmod
  9. L38
    exact hrmod
  10. L39
    rewrite hbranch_right_left
11Use earlier factsL40–42

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

  1. L40
    specialize add_assoc q
  2. L41
    specialize add_assoc m
  3. L42
    specialize add_assoc 1
12Calculate and transport equalitiesL43–43

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

  1. L43
    rewrite add_assoc
13Use earlier factsL44–44

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

  1. L44
    exact hsum

Library-wide reading audit

Original defined command ledger · 44 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro r
  4. 0004intro m
  5. 0005intro s
  6. 0006intro hp
  7. 0007intro hbranch
  8. 0008cases hbranch
  9. 0009cases hbranch_left
  10. 0010rewrite hbranch_left_left
  11. 0011rewrite hbranch_left_right
  12. 0012exists 0
  13. 0013exists 0
  14. 0014rewrite PA5
  15. 0015rewrite PA5
  16. 0016symm
  17. 0017apply PA3
  18. 0018cases hbranch_right
  19. 0019have hrmod : ModEq(2,r,m + 1)
    Exact native replay linehave hrmod : exists sdp_u_proof_r_reflected sdp_v_proof_r_reflected. (r) + 2 * sdp_u_proof_r_reflected = (m + 1) + 2 * sdp_v_proof_r_reflected
  20. 0020specialize odd_reflected_remainder_mod_two p
  21. 0021specialize odd_reflected_remainder_mod_two r
  22. 0022specialize odd_reflected_remainder_mod_two m
  23. 0023apply odd_reflected_remainder_mod_two
  24. 0024exact hp
  25. 0025exact hbranch_right_right
  26. 0026have hqmod : ModEq(2,q,q)
    Exact native replay linehave hqmod : exists sdp_u_proof_q_refl sdp_v_proof_q_refl. (q) + 2 * sdp_u_proof_q_refl = (q) + 2 * sdp_v_proof_q_refl
  27. 0027specialize mod_eq_refl 2
  28. 0028specialize mod_eq_refl q
  29. 0029exact mod_eq_refl
  30. 0030have hsum : ModEq(2,q + r,q + (m + 1))
    Exact native replay linehave hsum : exists sdp_u_proof_signed_upper sdp_v_proof_signed_upper. (q + r) + 2 * sdp_u_proof_signed_upper = (q + (m + 1)) + 2 * sdp_v_proof_signed_upper
  31. 0031specialize mod_eq_add 2
  32. 0032specialize mod_eq_add q
  33. 0033specialize mod_eq_add q
  34. 0034specialize mod_eq_add r
  35. 0035specialize mod_eq_add (m + 1)
  36. 0036apply mod_eq_add
  37. 0037exact hqmod
  38. 0038exact hrmod
  39. 0039rewrite hbranch_right_left
  40. 0040specialize add_assoc q
  41. 0041specialize add_assoc m
  42. 0042specialize add_assoc 1
  43. 0043rewrite add_assoc
  44. 0044exact hsum