PA0013

factor_difference

Stable checked-use theorem · independently closed

A common-factor difference is itself a multiple of that factor.

Exact expanded PA statement

forall c u v r. c * u = c * v + r -> exists w. r = c * w

Structural proof guide

Generated structural guide

A common-factor difference is itself a multiple of that factor.

Use the direct prerequisites zero_add, add_eq_zero_right, add_right_cancel, add_assoc, add_comm as previously established PA formulas.

The proof proceeds by structural induction (2), intermediate claims (2), equality transport (7).

Referenced ingredients

PA0001 zero_add PA0004 add_eq_zero_right PA0012 add_right_cancel PA0009 add_assoc PA000F add_comm

Proof neighborhood

Direct dependencies

PA0001 zero_add PA0004 add_eq_zero_right PA0012 add_right_cancel PA0009 add_assoc PA000F add_comm

Direct dependents

PA0014 divides_remainder PA001O common_divisor_divides_balanced_result PA00AG prime_bounded_square_one_cases

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 c
  2. 0002induction u
  3. 0003intro v
  4. 0004intro r
  5. 0005intro h
  6. 0006rewrite PA5 at h
  7. 0007have hr : r = 0
  8. 0008apply add_eq_zero_right
  9. 0009symm
  10. 0010exact h
  11. 0011exists 0
  12. 0012rewrite hr
  13. 0013rewrite PA5
  14. 0014refl
  15. 0015intro v
  16. 0016induction v
  17. 0017intro r
  18. 0018intro h
  19. 0019exists S u
  20. 0020rewrite PA5 at h
  21. 0021specialize zero_add r
  22. 0022rewrite zero_add at h
  23. 0023symm
  24. 0024exact h
  25. 0025intro r
  26. 0026intro h
  27. 0027have hred : c * u = c * v + r
  28. 0028specialize add_right_cancel (c * u)
  29. 0029specialize add_right_cancel (c * v + r)
  30. 0030specialize add_right_cancel c
  31. 0031apply add_right_cancel
  32. 0032rewrite PA6 at h
  33. 0033rewrite PA6 at h
  34. 0034trans (c * v + c) + r
  35. 0035exact h
  36. 0036trans c * v + (c + r)
  37. 0037apply add_assoc
  38. 0038trans c * v + (r + c)
  39. 0039congr
  40. 0040refl
  41. 0041apply add_comm
  42. 0042symm
  43. 0043apply add_assoc
  44. 0044specialize IH v
  45. 0045specialize IH r
  46. 0046apply IH
  47. 0047exact hred