BT0069

beta_factor_divides_product

Stable · empty-context checked

Every decoded factor inside an exact beta Product divides its terminal product.

Exact expanded PA statement

forall b c l n i p. (exists h. h + S i = l) -> ((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * 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 n = S ((S l) * v)) /\ exists q. u = q * S ((S l) * v) + n) /\ 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)))))) -> exists q. n = p * q

Structural proof guide

Every decoded factor inside an exact beta Product divides its terminal product.

Direct prerequisites: add_eq_zero_right, succ_ne_zero, beta_product_succ_decompose, le_of_succ_le_succ, le_eq_or_lt, beta_at_unique, mul_comm, multiple_mul_right. The authored body proceeds by structural induction (1), case analysis (7), intermediate claims (7), equality transport (3).

Proof neighborhood

Direct dependencies

BT000L add_eq_zero_right BT000C succ_ne_zero BT005J beta_product_succ_decompose BT0017 le_of_succ_le_succ BT001C le_eq_or_lt BT0042 beta_at_unique BT0006 mul_comm BT002A multiple_mul_right

Direct dependents

BT00VA factorial_prime_divides_of_le BT0100 prime_contribution_selected_entry

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. 0003induction l
  4. 0004intro n
  5. 0005intro i
  6. 0006intro p
  7. 0007intro hi
  8. 0008intro hp
  9. 0009intro hproduct
  10. 0010exfalso
  11. 0011cases hi
  12. 0012have hsi0 : S i = 0
  13. 0013specialize add_eq_zero_right x
  14. 0014specialize add_eq_zero_right (S i)
  15. 0015apply add_eq_zero_right
  16. 0016exact hi_witness
  17. 0017specialize succ_ne_zero i
  18. 0018apply succ_ne_zero
  19. 0019exact hsi0
  20. 0020intro n
  21. 0021intro i
  22. 0022intro p
  23. 0023intro hi
  24. 0024intro hp
  25. 0025intro hproduct
  26. 0026have hdecomp : exists a r. (((exists h. h + S a = S ((S l) * c)) /\ exists q. b = q * S ((S l) * c) + a) /\ ((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 * a))
  27. 0027specialize beta_product_succ_decompose b
  28. 0028specialize beta_product_succ_decompose c
  29. 0029specialize beta_product_succ_decompose l
  30. 0030specialize beta_product_succ_decompose n
  31. 0031apply beta_product_succ_decompose
  32. 0032exact hproduct
  33. 0033cases hdecomp
  34. 0034cases hdecomp_witness
  35. 0035cases hdecomp_witness_witness
  36. 0036cases hdecomp_witness_witness_right
  37. 0037have hil : exists h. h + i = l
  38. 0038specialize le_of_succ_le_succ i
  39. 0039specialize le_of_succ_le_succ l
  40. 0040apply le_of_succ_le_succ
  41. 0041exact hi
  42. 0042have hsplit : i = l \/ exists h. h + S i = l
  43. 0043specialize le_eq_or_lt i
  44. 0044specialize le_eq_or_lt l
  45. 0045apply le_eq_or_lt
  46. 0046exact hil
  47. 0047cases hsplit
  48. 0048have hpa : p = x
  49. 0049specialize beta_at_unique b
  50. 0050specialize beta_at_unique c
  51. 0051specialize beta_at_unique l
  52. 0052specialize beta_at_unique p
  53. 0053specialize beta_at_unique x
  54. 0054apply beta_at_unique
  55. 0055rewrite hsplit_left at hp
  56. 0056rewrite hsplit_left at hp
  57. 0057exact hp
  58. 0058exact hdecomp_witness_witness_left
  59. 0059exists x1
  60. 0060trans x1 * x
  61. 0061exact hdecomp_witness_witness_right_right
  62. 0062rewrite hpa
  63. 0063apply mul_comm
  64. 0064have hidiv : exists q. x1 = p * q
  65. 0065specialize IH x1
  66. 0066specialize IH i
  67. 0067specialize IH p
  68. 0068apply IH
  69. 0069exact hsplit_right
  70. 0070exact hp
  71. 0071exact hdecomp_witness_witness_right_left
  72. 0072have hmul : exists q. x1 * x = p * q
  73. 0073specialize multiple_mul_right p
  74. 0074specialize multiple_mul_right x1
  75. 0075specialize multiple_mul_right x
  76. 0076apply multiple_mul_right
  77. 0077exact hidiv
  78. 0078cases hmul
  79. 0079exists x2
  80. 0080trans x1 * x
  81. 0081exact hdecomp_witness_witness_right_right
  82. 0082exact hmul_witness