BT0037

common_divisor_divides_balanced_result

Stable · empty-context checked

Every common divisor of two inputs divides the result of a balanced natural combination.

Exact expanded PA statement

forall c a b d xp yp xn yn. (exists u. a = c * u) -> (exists v. b = c * v) -> a * xp + b * yp = d + (a * xn + b * yn) -> exists w. d = c * w

Structural proof guide

Every common divisor of two inputs divides the result of a balanced natural combination.

Direct prerequisites: mul_assoc, mul_add, add_comm, factor_difference. The authored body proceeds by case analysis (2), equality transport (4).

Proof neighborhood

Direct dependencies

BT0008 mul_assoc BT0007 mul_add BT0002 add_comm BT002G factor_difference

Direct dependents

BT0039 gauss_coprime_cancel

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro c
  2. 0002intro a
  3. 0003intro b
  4. 0004intro d
  5. 0005intro xp
  6. 0006intro yp
  7. 0007intro xn
  8. 0008intro yn
  9. 0009intro ha
  10. 0010intro hb
  11. 0011intro h
  12. 0012cases ha
  13. 0013cases hb
  14. 0014specialize factor_difference c
  15. 0015specialize factor_difference (x * xp + x1 * yp)
  16. 0016specialize factor_difference (x * xn + x1 * yn)
  17. 0017specialize factor_difference d
  18. 0018apply factor_difference
  19. 0019trans c * (x * xp) + c * (x1 * yp)
  20. 0020apply mul_add
  21. 0021trans (c * x) * xp + (c * x1) * yp
  22. 0022congr
  23. 0023symm
  24. 0024apply mul_assoc
  25. 0025symm
  26. 0026apply mul_assoc
  27. 0027trans a * xp + b * yp
  28. 0028rewrite ha_witness
  29. 0029rewrite hb_witness
  30. 0030refl
  31. 0031trans d + (a * xn + b * yn)
  32. 0032exact h
  33. 0033trans (a * xn + b * yn) + d
  34. 0034apply add_comm
  35. 0035trans ((c * x) * xn + (c * x1) * yn) + d
  36. 0036rewrite ha_witness
  37. 0037rewrite hb_witness
  38. 0038refl
  39. 0039trans (c * (x * xn) + c * (x1 * yn)) + d
  40. 0040congr
  41. 0041congr
  42. 0042apply mul_assoc
  43. 0043apply mul_assoc
  44. 0044refl
  45. 0045congr
  46. 0046symm
  47. 0047apply mul_add
  48. 0048refl