PA001N

balanced_combination_scale_right

Stable checked-use theorem · independently closed

Scale a balanced natural combination on the right.

Exact expanded PA statement

forall a b d xp yp xn yn z. a * xp + b * yp = d + (a * xn + b * yn) -> a * (xp * z) + (b * z) * yp = d * z + (a * (xn * z) + (b * z) * yn)

Structural proof guide

Generated structural guide

Scale a balanced natural combination on the right.

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

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA000B mul_assoc PA000H mul_comm PA0016 add_mul

Proof neighborhood

Direct dependencies

PA000B mul_assoc PA000H mul_comm PA0016 add_mul

Direct dependents

PA001P gauss_coprime_cancel

Formal native tactic body

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

  1. 0001intro a
  2. 0002intro b
  3. 0003intro d
  4. 0004intro xp
  5. 0005intro yp
  6. 0006intro xn
  7. 0007intro yn
  8. 0008intro z
  9. 0009intro h
  10. 0010trans (a * xp) * z + (b * z) * yp
  11. 0011congr
  12. 0012symm
  13. 0013apply mul_assoc
  14. 0014refl
  15. 0015trans (a * xp) * z + (b * yp) * z
  16. 0016congr
  17. 0017refl
  18. 0018trans b * (z * yp)
  19. 0019apply mul_assoc
  20. 0020trans b * (yp * z)
  21. 0021congr
  22. 0022refl
  23. 0023apply mul_comm
  24. 0024symm
  25. 0025apply mul_assoc
  26. 0026trans (a * xp + b * yp) * z
  27. 0027symm
  28. 0028apply add_mul
  29. 0029trans (d + (a * xn + b * yn)) * z
  30. 0030congr
  31. 0031exact h
  32. 0032refl
  33. 0033trans d * z + (a * xn + b * yn) * z
  34. 0034apply add_mul
  35. 0035trans d * z + ((a * xn) * z + (b * yn) * z)
  36. 0036congr
  37. 0037refl
  38. 0038apply add_mul
  39. 0039trans d * z + (a * (xn * z) + (b * yn) * z)
  40. 0040congr
  41. 0041refl
  42. 0042congr
  43. 0043apply mul_assoc
  44. 0044refl
  45. 0045congr
  46. 0046refl
  47. 0047congr
  48. 0048refl
  49. 0049trans b * (yn * z)
  50. 0050apply mul_assoc
  51. 0051trans b * (z * yn)
  52. 0052congr
  53. 0053refl
  54. 0054apply mul_comm
  55. 0055symm
  56. 0056apply mul_assoc