PA009B

scaled_inverse_symmetric

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

The scaled-inverse relation is symmetric.

Exact expanded PA statement

forall p a x y. ((((~(x = 0) /\ (exists esi_strict_gap_symmetric_source_left_bound. esi_strict_gap_symmetric_source_left_bound + S x = p))) /\ (((~(y = 0) /\ (exists esi_strict_gap_symmetric_source_right_bound. esi_strict_gap_symmetric_source_right_bound + S y = p))) /\ (exists esi_mod_left_symmetric_source_mod esi_mod_right_symmetric_source_mod. (x * y) + p * esi_mod_left_symmetric_source_mod = (a) + p * esi_mod_right_symmetric_source_mod)))) -> ((((~(y = 0) /\ (exists esi_strict_gap_symmetric_target_left_bound. esi_strict_gap_symmetric_target_left_bound + S y = p))) /\ (((~(x = 0) /\ (exists esi_strict_gap_symmetric_target_right_bound. esi_strict_gap_symmetric_target_right_bound + S x = p))) /\ (exists esi_mod_left_symmetric_target_mod esi_mod_right_symmetric_target_mod. (y * x) + p * esi_mod_left_symmetric_target_mod = (a) + p * esi_mod_right_symmetric_target_mod))))

Structural proof guide

Generated structural guide

The scaled-inverse relation is symmetric.

Use the direct prerequisites mul_comm as previously established PA formulas.

The proof proceeds by case analysis (4), intermediate claims (1), equality transport (1).

Referenced ingredients

PA000H mul_comm

Proof neighborhood

Direct dependencies

PA000H mul_comm

Direct dependents

PA009E scaled_inverse_prefix_involutive

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 a
  3. 0003intro x
  4. 0004intro y
  5. 0005intro hxy
  6. 0006cases hxy
  7. 0007cases hxy_left
  8. 0008cases hxy_right
  9. 0009cases hxy_right_left
  10. 0010split
  11. 0011split
  12. 0012exact hxy_right_left_left
  13. 0013exact hxy_right_left_right
  14. 0014split
  15. 0015split
  16. 0016exact hxy_left_left
  17. 0017exact hxy_left_right
  18. 0018have hcomm : x * y = y * x
  19. 0019apply mul_comm
  20. 0020rewrite hcomm at hxy_right_right
  21. 0021exact hxy_right_right