BT004M

bounded_common_multiple_step

Stable · empty-context checked

Extend a nonzero common multiple through the next positive natural.

Exact expanded PA statement

forall B c. ~(c = 0) -> (forall t. (exists h. S t + S h = S B) -> exists k. c = S t * k) -> exists c2. (~(c2 = 0) /\ forall t. (exists h. S t + S h = S (S B)) -> exists k. c2 = S t * k)

Structural proof guide

Extend a nonzero common multiple through the next positive natural.

Direct prerequisites: mul_eq_zero, succ_ne_zero, zero_or_succ, multiple_mul_right, mul_comm. The authored body proceeds by case analysis (4), intermediate claims (6), equality transport (6).

Proof neighborhood

Direct dependencies

BT000M mul_eq_zero BT000C succ_ne_zero BT000Q zero_or_succ BT002A multiple_mul_right BT0006 mul_comm

Direct dependents

BT004N bounded_common_multiple_exists

Formal native tactic body

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

  1. 0001intro B
  2. 0002intro c
  3. 0003intro hc
  4. 0004intro hall
  5. 0005exists c * S B
  6. 0006split
  7. 0007have hSB : ~(S B = 0)
  8. 0008specialize succ_ne_zero B
  9. 0009exact succ_ne_zero
  10. 0010have hprod : ~(c * S B = 0)
  11. 0011intro hzero
  12. 0012have hz : c = 0 \/ S B = 0
  13. 0013specialize mul_eq_zero c
  14. 0014specialize mul_eq_zero (S B)
  15. 0015apply mul_eq_zero
  16. 0016exact hzero
  17. 0017cases hz
  18. 0018apply hc
  19. 0019exact hz_left
  20. 0020apply hSB
  21. 0021exact hz_right
  22. 0022exact hprod
  23. 0023intro t
  24. 0024intro ht
  25. 0025cases ht
  26. 0026specialize zero_or_succ x
  27. 0027cases zero_or_succ
  28. 0028rewrite zero_or_succ_left at ht_witness
  29. 0029have hteq : S t = S B
  30. 0030rewrite PA4 at ht_witness
  31. 0031rewrite PA3 at ht_witness
  32. 0032apply PA2
  33. 0033exact ht_witness
  34. 0034exists c
  35. 0035rewrite hteq
  36. 0036apply mul_comm
  37. 0037cases zero_or_succ_right
  38. 0038have hprev : exists h. S t + S h = S B
  39. 0039exists x1
  40. 0040rewrite zero_or_succ_right_witness at ht_witness
  41. 0041rewrite PA4 at ht_witness
  42. 0042apply PA2
  43. 0043exact ht_witness
  44. 0044have hdivc : exists k. c = S t * k
  45. 0045specialize hall t
  46. 0046apply hall
  47. 0047exact hprev
  48. 0048specialize multiple_mul_right (S t)
  49. 0049specialize multiple_mul_right c
  50. 0050specialize multiple_mul_right (S B)
  51. 0051apply multiple_mul_right
  52. 0052exact hdivc