PA00FU · theorem

qres_opposite_status_from_mod_four_three

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

Two three-mod-four inputs force opposite cross-residue status.

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. ∀ e. ∀ f. ∀ h. ∀ k. p = 2 · h + 1 → q = 2 · k + 1 → (QRes(p,q) → Even(e)) ∧ (Even(e) → QRes(p,q)) ∧ ((¬QRes(p,q) → Odd(e)) ∧ (Odd(e) → ¬QRes(p,q))) → (QRes(q,p) → Even(f)) ∧ (Even(f) → QRes(q,p)) ∧ ((¬QRes(q,p) → Odd(f)) ∧ (Odd(f) → ¬QRes(q,p))) → ModEq(2,e + f,h · k) → Mod4Three(p) ∧ Mod4Three(q) → QRes(p,q) ∧ ¬QRes(q,p) ∨ ¬QRes(p,q) ∧ QRes(q,p)

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 PD0009 Even PD0010 Odd PD0012 Mod4Three PD0021 QRes

23 occurrences

In local proof propositions

PD0010 Odd PD0012 Mod4Three

11 occurrences

Exact expanded native-PA statement
forall p q e f h k. p = 2 * h + 1 -> q = 2 * k + 1 -> (((((exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq) -> (exists qrp_even_e_even. e = 2 * qrp_even_e_even)) /\ ((exists qrp_even_e_even. e = 2 * qrp_even_e_even) -> (exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq))) /\ (((~(exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq)) -> (exists qrp_odd_e_odd. e = 2 * qrp_odd_e_odd + 1)) /\ ((exists qrp_odd_e_odd. e = 2 * qrp_odd_e_odd + 1) -> ~(exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq))))) -> (((((exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp) -> (exists qrp_even_f_even. f = 2 * qrp_even_f_even)) /\ ((exists qrp_even_f_even. f = 2 * qrp_even_f_even) -> (exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp))) /\ (((~(exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp)) -> (exists qrp_odd_f_odd. f = 2 * qrp_odd_f_odd + 1)) /\ ((exists qrp_odd_f_odd. f = 2 * qrp_odd_f_odd + 1) -> ~(exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp))))) -> (exists qrp_u_count_product qrp_v_count_product. e + f + 2 * qrp_u_count_product = h * k + 2 * qrp_v_count_product) -> ((exists qrp_three_p. p = 4 * qrp_three_p + 3) /\ (exists qrp_three_q. q = 4 * qrp_three_q + 3)) -> ((((exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq) /\ ~(exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp)) \/ (~(exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq) /\ (exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp))))

Proof neighborhood

Direct theorem prerequisites

PA00FR odd_half_odd_iff_mod4_three PA006D odd_mul_odd PA00FT qres_opposite_status_from_odd_half_product_mod_two

Direct theorem dependents

PA00FV conditional_qres_opposite_status_from_oriented_gauss_counts

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

48 script commands · 11 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 (3)
odd half odd iff mod4 threeodd mul oddqres opposite status from odd half product mod two
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro e
  4. L4
    intro f
  5. L5
    intro h
  6. L6
    intro k
  7. L7
    intro hp
  8. L8
    intro hq
  9. L9
    intro heclass
  10. L10
    intro hfclass
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hmod
  2. L12
    intro hthree
03Separate the logical casesL13–13

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

  1. L13
    cases hthree
04Establish hpbridgeL14–18

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

  1. L14
    have hpbridge : (Odd(h) → Mod4Three(p)) ∧ (Mod4Three(p) → Odd(h))Definitions: Odd(h)Mod4Three(p)Original native command in the exact edition
  2. L15
    specialize odd_half_odd_iff_mod4_three p
  3. L16
    specialize odd_half_odd_iff_mod4_three h
  4. L17
    apply odd_half_odd_iff_mod4_three
  5. L18
    exact hp
05Separate the logical casesL19–19

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

  1. L19
    cases hpbridge
06Establish hpoddL20–22

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

  1. L20
  2. L21
    apply hpbridge_right
  3. L22
    exact hthree_left
07Establish hqbridgeL23–27

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

  1. L23
    have hqbridge : (Odd(k) → Mod4Three(q)) ∧ (Mod4Three(q) → Odd(k))Definitions: Odd(k)Mod4Three(q)Original native command in the exact edition
  2. L24
    specialize odd_half_odd_iff_mod4_three q
  3. L25
    specialize odd_half_odd_iff_mod4_three k
  4. L26
    apply odd_half_odd_iff_mod4_three
  5. L27
    exact hq
08Separate the logical casesL28–28

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

  1. L28
    cases hqbridge
09Establish hqoddL29–31

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

  1. L29
  2. L30
    apply hqbridge_right
  3. L31
    exact hthree_right
10Establish hproductL32–41

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

  1. L32
    have hproduct : Odd(h · k)Definitions: Odd(h · k)Original native command in the exact edition
  2. L33
    specialize odd_mul_odd h
  3. L34
    specialize odd_mul_odd k
  4. L35
    apply odd_mul_odd
  5. L36
    exact hpodd
  6. L37
    exact hqodd
  7. L38
    specialize qres_opposite_status_from_odd_half_product_mod_two p
  8. L39
    specialize qres_opposite_status_from_odd_half_product_mod_two q
  9. L40
    specialize qres_opposite_status_from_odd_half_product_mod_two e
  10. L41
    specialize qres_opposite_status_from_odd_half_product_mod_two f
11Use earlier factsL42–48

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

  1. L42
    specialize qres_opposite_status_from_odd_half_product_mod_two h
  2. L43
    specialize qres_opposite_status_from_odd_half_product_mod_two k
  3. L44
    apply qres_opposite_status_from_odd_half_product_mod_two
  4. L45
    exact heclass
  5. L46
    exact hfclass
  6. L47
    exact hmod
  7. L48
    exact hproduct

Library-wide reading audit

Original defined command ledger · 48 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro e
  4. 0004intro f
  5. 0005intro h
  6. 0006intro k
  7. 0007intro hp
  8. 0008intro hq
  9. 0009intro heclass
  10. 0010intro hfclass
  11. 0011intro hmod
  12. 0012intro hthree
  13. 0013cases hthree
  14. 0014have hpbridge : (Odd(h) → Mod4Three(p)) ∧ (Mod4Three(p) → Odd(h))
    Exact native replay linehave hpbridge : (((exists qrp_odd_h. h = 2 * qrp_odd_h + 1) -> (exists qrp_three_p. p = 4 * qrp_three_p + 3)) /\ ((exists qrp_three_p. p = 4 * qrp_three_p + 3) -> (exists qrp_odd_h. h = 2 * qrp_odd_h + 1)))
  15. 0015specialize odd_half_odd_iff_mod4_three p
  16. 0016specialize odd_half_odd_iff_mod4_three h
  17. 0017apply odd_half_odd_iff_mod4_three
  18. 0018exact hp
  19. 0019cases hpbridge
  20. 0020have hpodd : Odd(h)
    Exact native replay linehave hpodd : exists qrp_odd_h. h = 2 * qrp_odd_h + 1
  21. 0021apply hpbridge_right
  22. 0022exact hthree_left
  23. 0023have hqbridge : (Odd(k) → Mod4Three(q)) ∧ (Mod4Three(q) → Odd(k))
    Exact native replay linehave hqbridge : (((exists qrp_odd_k. k = 2 * qrp_odd_k + 1) -> (exists qrp_three_q. q = 4 * qrp_three_q + 3)) /\ ((exists qrp_three_q. q = 4 * qrp_three_q + 3) -> (exists qrp_odd_k. k = 2 * qrp_odd_k + 1)))
  24. 0024specialize odd_half_odd_iff_mod4_three q
  25. 0025specialize odd_half_odd_iff_mod4_three k
  26. 0026apply odd_half_odd_iff_mod4_three
  27. 0027exact hq
  28. 0028cases hqbridge
  29. 0029have hqodd : Odd(k)
    Exact native replay linehave hqodd : exists qrp_odd_k. k = 2 * qrp_odd_k + 1
  30. 0030apply hqbridge_right
  31. 0031exact hthree_right
  32. 0032have hproduct : Odd(h · k)
    Exact native replay linehave hproduct : exists qrp_odd_half_product. h * k = 2 * qrp_odd_half_product + 1
  33. 0033specialize odd_mul_odd h
  34. 0034specialize odd_mul_odd k
  35. 0035apply odd_mul_odd
  36. 0036exact hpodd
  37. 0037exact hqodd
  38. 0038specialize qres_opposite_status_from_odd_half_product_mod_two p
  39. 0039specialize qres_opposite_status_from_odd_half_product_mod_two q
  40. 0040specialize qres_opposite_status_from_odd_half_product_mod_two e
  41. 0041specialize qres_opposite_status_from_odd_half_product_mod_two f
  42. 0042specialize qres_opposite_status_from_odd_half_product_mod_two h
  43. 0043specialize qres_opposite_status_from_odd_half_product_mod_two k
  44. 0044apply qres_opposite_status_from_odd_half_product_mod_two
  45. 0045exact heclass
  46. 0046exact hfclass
  47. 0047exact hmod
  48. 0048exact hproduct