PA000I

bounded_common_multiple_step

Stable checked-use theorem · independently closed

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

Generated structural guide

Extend a nonzero common multiple through the next positive natural.

Use the direct prerequisites mul_eq_zero, succ_ne_zero, zero_or_succ, multiple_mul_right, mul_comm as previously established PA formulas.

The proof proceeds by case analysis (4), intermediate claims (6), equality transport (6).

Referenced ingredients

PA0007 mul_eq_zero PA0005 succ_ne_zero PA0008 zero_or_succ PA000C multiple_mul_right PA000H mul_comm

Proof neighborhood

Direct dependencies

PA0007 mul_eq_zero PA0005 succ_ne_zero PA0008 zero_or_succ PA000C multiple_mul_right PA000H mul_comm

Direct dependents

PA000K bounded_common_multiple_exists

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 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