BT005J

beta_product_succ_decompose

Stable · empty-context checked

A successor product decomposes into its prefix product and final decoded factor.

Exact expanded PA statement

forall b c l n. (exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S n = S ((S S l) * v)) /\ exists q. u = q * S ((S S l) * v) + n) /\ forall i. (exists h. h + S i = S l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p)))))) -> exists p r. (((exists h. h + S p = S ((S l) * c)) /\ exists q. b = q * S ((S l) * c) + p) /\ ((exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S r = S ((S l) * v)) /\ exists q. u = q * S ((S l) * v) + r) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p)))))) /\ n = r * p))

Structural proof guide

A successor product decomposes into its prefix product and final decoded factor.

Direct prerequisites: le_refl, le_succ, beta_at_unique. The authored body proceeds by case analysis (10), intermediate claims (2).

Proof neighborhood

Direct dependencies

BT000E le_refl BT0018 le_succ BT0042 beta_at_unique

Direct dependents

BT0069 beta_factor_divides_product BT0083 pow_successor_decompose BT0092 factorial_succ_decompose BT00DH beta_product_pointwise_coprime BT00UD primorial_succ_decompose BT00UQ beta_product_prefix_suffix_split BT00VD beta_pairwise_coprime_product_divides_common_multiple BT00X9 beta_product_pointwise_le BT010U beta_product_all_one_exact

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 l
  4. 0004intro n
  5. 0005intro hproduct
  6. 0006cases hproduct
  7. 0007cases hproduct_witness
  8. 0008cases hproduct_witness_witness
  9. 0009cases hproduct_witness_witness_right
  10. 0010have hstep : exists p r s. (((exists h. h + S p = S ((S l) * c)) /\ exists q. b = q * S ((S l) * c) + p) /\ (((exists h. h + S r = S ((S l) * x1)) /\ exists q. x = q * S ((S l) * x1) + r) /\ (((exists h. h + S s = S ((S S l) * x1)) /\ exists q. x = q * S ((S S l) * x1) + s) /\ s = r * p)))
  11. 0011specialize hproduct_witness_witness_right_right l
  12. 0012apply hproduct_witness_witness_right_right
  13. 0013specialize le_refl (S l)
  14. 0014exact le_refl
  15. 0015cases hstep
  16. 0016cases hstep_witness
  17. 0017cases hstep_witness_witness
  18. 0018cases hstep_witness_witness_witness
  19. 0019cases hstep_witness_witness_witness_right
  20. 0020cases hstep_witness_witness_witness_right_right
  21. 0021have hn : n = x4
  22. 0022specialize beta_at_unique x
  23. 0023specialize beta_at_unique x1
  24. 0024specialize beta_at_unique (S l)
  25. 0025specialize beta_at_unique n
  26. 0026specialize beta_at_unique x4
  27. 0027apply beta_at_unique
  28. 0028exact hproduct_witness_witness_right_left
  29. 0029exact hstep_witness_witness_witness_right_right_left
  30. 0030exists x2
  31. 0031exists x3
  32. 0032split
  33. 0033exact hstep_witness_witness_witness_left
  34. 0034split
  35. 0035exists x
  36. 0036exists x1
  37. 0037split
  38. 0038exact hproduct_witness_witness_left
  39. 0039split
  40. 0040exact hstep_witness_witness_witness_right_left
  41. 0041intro i
  42. 0042intro hi
  43. 0043specialize hproduct_witness_witness_right_right i
  44. 0044apply hproduct_witness_witness_right_right
  45. 0045specialize le_succ (S i)
  46. 0046specialize le_succ l
  47. 0047apply le_succ
  48. 0048exact hi
  49. 0049trans x4
  50. 0050exact hn
  51. 0051exact hstep_witness_witness_witness_right_right_right