PA008N

scaled_inverse_from_unit_inverse

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

Multiplying an ordinary inverse by the target gives a scaled inverse.

Exact expanded PA statement

forall p a x z. (exists esi_mod_left_from_unit_source esi_mod_right_from_unit_source. (x * z) + p * esi_mod_left_from_unit_source = (1) + p * esi_mod_right_from_unit_source) -> (exists esi_mod_left_from_unit_result esi_mod_right_from_unit_result. (x * (a * z)) + p * esi_mod_left_from_unit_result = (a) + p * esi_mod_right_from_unit_result)

Structural proof guide

Generated structural guide

Multiplying an ordinary inverse by the target gives a scaled inverse.

Use the direct prerequisites mod_eq_mul_left, mul_assoc, mul_comm, mul_one as previously established PA formulas.

The proof proceeds by intermediate claims (3), equality transport (2).

Referenced ingredients

PA0020 mod_eq_mul_left PA000B mul_assoc PA000H mul_comm PA0002 mul_one

Proof neighborhood

Direct dependencies

PA0020 mod_eq_mul_left PA000B mul_assoc PA000H mul_comm PA0002 mul_one

Direct dependents

PA008Q prime_scaled_inverse_exists

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 z
  5. 0005intro hxz
  6. 0006have hscaled : exists esi_mod_left_from_unit_scaled esi_mod_right_from_unit_scaled. (a * (x * z)) + p * esi_mod_left_from_unit_scaled = (a * 1) + p * esi_mod_right_from_unit_scaled
  7. 0007specialize mod_eq_mul_left p
  8. 0008specialize mod_eq_mul_left (x * z)
  9. 0009specialize mod_eq_mul_left 1
  10. 0010specialize mod_eq_mul_left a
  11. 0011apply mod_eq_mul_left
  12. 0012exact hxz
  13. 0013have hleft : a * (x * z) = x * (a * z)
  14. 0014trans (a * x) * z
  15. 0015symm
  16. 0016specialize mul_assoc a
  17. 0017specialize mul_assoc x
  18. 0018specialize mul_assoc z
  19. 0019apply mul_assoc
  20. 0020trans (x * a) * z
  21. 0021congr
  22. 0022apply mul_comm
  23. 0023refl
  24. 0024specialize mul_assoc x
  25. 0025specialize mul_assoc a
  26. 0026specialize mul_assoc z
  27. 0027apply mul_assoc
  28. 0028have hright : a * 1 = a
  29. 0029specialize mul_one a
  30. 0030exact mul_one
  31. 0031rewrite hleft at hscaled
  32. 0032rewrite hright at hscaled
  33. 0033exact hscaled