PA00FT

qres_opposite_status_from_odd_half_product_mod_two

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

Modulo-two equality with an odd half product gives opposite residue status.

Exact expanded PA statement

forall p q e f h k. (((((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_odd_half_product. h * k = 2 * qrp_odd_half_product + 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 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))))

Structural proof guide

Generated structural guide

Modulo-two equality with an odd half product gives opposite residue status.

Use the direct prerequisites mod_two_preserves_parity, qres_opposite_status_from_odd_count_sum as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (2).

Referenced ingredients

PA00FL mod_two_preserves_parity PA00FS qres_opposite_status_from_odd_count_sum

Proof neighborhood

Direct dependencies

PA00FL mod_two_preserves_parity PA00FS qres_opposite_status_from_odd_count_sum

Direct dependents

PA00FU qres_opposite_status_from_mod_four_three

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro p
  2. 0002intro q
  3. 0003intro e
  4. 0004intro f
  5. 0005intro h
  6. 0006intro k
  7. 0007intro heclass
  8. 0008intro hfclass
  9. 0009intro hmod
  10. 0010intro hproduct
  11. 0011have htransport : (((((exists qrp_even_transport_count. e + f = 2 * qrp_even_transport_count) -> (exists qrp_even_transport_product. h * k = 2 * qrp_even_transport_product)) /\ ((exists qrp_even_transport_product. h * k = 2 * qrp_even_transport_product) -> (exists qrp_even_transport_count. e + f = 2 * qrp_even_transport_count)))) /\ ((((exists qrp_odd_transport_count. e + f = 2 * qrp_odd_transport_count + 1) -> (exists qrp_odd_transport_product. h * k = 2 * qrp_odd_transport_product + 1)) /\ ((exists qrp_odd_transport_product. h * k = 2 * qrp_odd_transport_product + 1) -> (exists qrp_odd_transport_count. e + f = 2 * qrp_odd_transport_count + 1)))))
  12. 0012specialize mod_two_preserves_parity (e + f)
  13. 0013specialize mod_two_preserves_parity (h * k)
  14. 0014apply mod_two_preserves_parity
  15. 0015exact hmod
  16. 0016cases htransport
  17. 0017cases htransport_right
  18. 0018have hcount : exists qrp_odd_transport_count. e + f = 2 * qrp_odd_transport_count + 1
  19. 0019apply htransport_right_right
  20. 0020exact hproduct
  21. 0021specialize qres_opposite_status_from_odd_count_sum p
  22. 0022specialize qres_opposite_status_from_odd_count_sum q
  23. 0023specialize qres_opposite_status_from_odd_count_sum e
  24. 0024specialize qres_opposite_status_from_odd_count_sum f
  25. 0025apply qres_opposite_status_from_odd_count_sum
  26. 0026exact heclass
  27. 0027exact hfclass
  28. 0028exact hcount