PA001U

beta_exclusive_accumulated_product_step

Stable checked-use theorem · independently closed

Extend the accumulated target-modulus product for an exclusive prefix.

Exact expanded PA statement

forall N c k P. (forall t. (exists h. S t + S h = S N) -> exists q. c = S t * q) -> (exists h. h + S k = N) -> ~(P = 0) -> (forall i. (exists h. h + S i = k) -> exists q. P = S ((S i) * c) * q) -> (forall j. (exists g. g + k = j) -> (exists h. h + j = N) -> forall d. (exists u. P = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1) -> (~(P * S ((S k) * c) = 0) /\ ((forall i. (exists h. h + S i = S k) -> exists q. P * S ((S k) * c) = S ((S i) * c) * q) /\ forall j. (exists g. g + S k = j) -> (exists h. h + j = N) -> forall d. (exists u. P * S ((S k) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1))

Structural proof guide

Generated structural guide

Extend the accumulated target-modulus product for an exclusive prefix.

Use the direct prerequisites mul_ne_zero, right_factor_divides_product, beta_modulus_nonzero, le_of_succ_le_succ, le_eq_or_lt, multiple_mul_right, le_succ_self, le_trans, lt_to_le, lt_irrefl_expanded, beta_moduli_pairwise_coprime_bounded, coprime_mul_left as previously established PA formulas.

The proof proceeds by case analysis (1), intermediate claims (11), equality transport (2).

Referenced ingredients

PA000S mul_ne_zero PA000T right_factor_divides_product PA000U beta_modulus_nonzero PA000V le_of_succ_le_succ PA000W le_eq_or_lt PA000C multiple_mul_right PA000Q le_succ_self PA000R le_trans PA000X lt_to_le PA0010 lt_irrefl_expanded PA001S beta_moduli_pairwise_coprime_bounded PA001T coprime_mul_left

Proof neighborhood

Direct dependencies

PA000S mul_ne_zero PA000T right_factor_divides_product PA000U beta_modulus_nonzero PA000V le_of_succ_le_succ PA000W le_eq_or_lt PA000C multiple_mul_right PA000Q le_succ_self PA000R le_trans PA000X lt_to_le PA0010 lt_irrefl_expanded PA001S beta_moduli_pairwise_coprime_bounded PA001T coprime_mul_left

Direct dependents

PA002H beta_exclusive_recode_invariant_step

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 N
  2. 0002intro c
  3. 0003intro k
  4. 0004intro P
  5. 0005intro hcm
  6. 0006intro hkN
  7. 0007intro hP
  8. 0008intro hdiv
  9. 0009intro hfuture
  10. 0010have hnew : ~(S ((S k) * c) = 0)
  11. 0011specialize beta_modulus_nonzero c
  12. 0012specialize beta_modulus_nonzero k
  13. 0013exact beta_modulus_nonzero
  14. 0014split
  15. 0015specialize mul_ne_zero P
  16. 0016specialize mul_ne_zero (S ((S k) * c))
  17. 0017intro hzero
  18. 0018apply mul_ne_zero
  19. 0019exact hP
  20. 0020exact hnew
  21. 0021exact hzero
  22. 0022split
  23. 0023intro i
  24. 0024intro hi
  25. 0025have hik : exists r. r + i = k
  26. 0026specialize le_of_succ_le_succ i
  27. 0027specialize le_of_succ_le_succ k
  28. 0028apply le_of_succ_le_succ
  29. 0029exact hi
  30. 0030have hsplit : i = k \/ exists r. r + S i = k
  31. 0031specialize le_eq_or_lt i
  32. 0032specialize le_eq_or_lt k
  33. 0033apply le_eq_or_lt
  34. 0034exact hik
  35. 0035cases hsplit
  36. 0036rewrite hsplit_left
  37. 0037specialize right_factor_divides_product P
  38. 0038specialize right_factor_divides_product (S ((S k) * c))
  39. 0039exact right_factor_divides_product
  40. 0040have hiP : exists q. P = S ((S i) * c) * q
  41. 0041specialize hdiv i
  42. 0042apply hdiv
  43. 0043exact hsplit_right
  44. 0044specialize multiple_mul_right (S ((S i) * c))
  45. 0045specialize multiple_mul_right P
  46. 0046specialize multiple_mul_right (S ((S k) * c))
  47. 0047apply multiple_mul_right
  48. 0048exact hiP
  49. 0049intro j
  50. 0050intro hSkj
  51. 0051intro hjN
  52. 0052have hkj : exists r. r + k = j
  53. 0053have hkSk : exists r. r + k = S k
  54. 0054specialize le_succ_self k
  55. 0055exact le_succ_self
  56. 0056specialize le_trans k
  57. 0057specialize le_trans (S k)
  58. 0058specialize le_trans j
  59. 0059apply le_trans
  60. 0060exact hkSk
  61. 0061exact hSkj
  62. 0062have hPj : forall d. (exists u. P = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1
  63. 0063specialize hfuture j
  64. 0064apply hfuture
  65. 0065exact hkj
  66. 0066exact hjN
  67. 0067have hneq : ~(k = j)
  68. 0068intro heq
  69. 0069rewrite <- heq at hSkj
  70. 0070specialize lt_irrefl_expanded k
  71. 0071apply lt_irrefl_expanded
  72. 0072exact hSkj
  73. 0073have hkbound : exists r. r + k = N
  74. 0074specialize lt_to_le k
  75. 0075specialize lt_to_le N
  76. 0076apply lt_to_le
  77. 0077exact hkN
  78. 0078have hpairs : forall i j. ~(i = j) -> (exists hi. hi + i = N) -> (exists hj. hj + j = N) -> forall d. (exists u. S ((S i) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1
  79. 0079specialize beta_moduli_pairwise_coprime_bounded N
  80. 0080specialize beta_moduli_pairwise_coprime_bounded c
  81. 0081apply beta_moduli_pairwise_coprime_bounded
  82. 0082exact hcm
  83. 0083have hnewj : forall d. (exists u. S ((S k) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1
  84. 0084specialize hpairs k
  85. 0085specialize hpairs j
  86. 0086apply hpairs
  87. 0087exact hneq
  88. 0088exact hkbound
  89. 0089exact hjN
  90. 0090specialize coprime_mul_left P
  91. 0091specialize coprime_mul_left (S ((S k) * c))
  92. 0092specialize coprime_mul_left (S ((S j) * c))
  93. 0093apply coprime_mul_left
  94. 0094exact hPj
  95. 0095exact hnewj