BT00VD

beta_pairwise_coprime_product_divides_common_multiple

Alpha body-checked · checked-use disabled

A pairwise-coprime product divides every common multiple of its factors.

Exact expanded PA statement

forall b c l n z. (forall bpr_left_index_bpcpdcm_pairwise bpr_right_index_bpcpdcm_pairwise bpr_left_value_bpcpdcm_pairwise bpr_right_value_bpcpdcm_pairwise. (exists bpr_gap_bpcpdcm_pairwise_left_bound. bpr_gap_bpcpdcm_pairwise_left_bound + S (bpr_left_index_bpcpdcm_pairwise) = l) -> (exists bpr_gap_bpcpdcm_pairwise_right_bound. bpr_gap_bpcpdcm_pairwise_right_bound + S (bpr_right_index_bpcpdcm_pairwise) = l) -> (((exists bpr_height_bpcpdcm_pairwise_left_at. bpr_height_bpcpdcm_pairwise_left_at + S (bpr_left_value_bpcpdcm_pairwise) = S ((S (bpr_left_index_bpcpdcm_pairwise)) * c)) /\ exists bpr_quotient_bpcpdcm_pairwise_left_at. b = bpr_quotient_bpcpdcm_pairwise_left_at * S ((S (bpr_left_index_bpcpdcm_pairwise)) * c) + (bpr_left_value_bpcpdcm_pairwise))) -> (((exists bpr_height_bpcpdcm_pairwise_right_at. bpr_height_bpcpdcm_pairwise_right_at + S (bpr_right_value_bpcpdcm_pairwise) = S ((S (bpr_right_index_bpcpdcm_pairwise)) * c)) /\ exists bpr_quotient_bpcpdcm_pairwise_right_at. b = bpr_quotient_bpcpdcm_pairwise_right_at * S ((S (bpr_right_index_bpcpdcm_pairwise)) * c) + (bpr_right_value_bpcpdcm_pairwise))) -> ~(bpr_left_index_bpcpdcm_pairwise = bpr_right_index_bpcpdcm_pairwise) -> (forall bpr_coprime_divisor_bpcpdcm_pairwise_coprime. (exists bpr_coprime_left_factor_bpcpdcm_pairwise_coprime. bpr_left_value_bpcpdcm_pairwise = bpr_coprime_divisor_bpcpdcm_pairwise_coprime * bpr_coprime_left_factor_bpcpdcm_pairwise_coprime) -> (exists bpr_coprime_right_factor_bpcpdcm_pairwise_coprime. bpr_right_value_bpcpdcm_pairwise = bpr_coprime_divisor_bpcpdcm_pairwise_coprime * bpr_coprime_right_factor_bpcpdcm_pairwise_coprime) -> bpr_coprime_divisor_bpcpdcm_pairwise_coprime = 1)) -> (forall bpr_divisor_index_bpcpdcm_pointwise bpr_divisor_value_bpcpdcm_pointwise. (exists bpr_gap_bpcpdcm_pointwise_index_bound. bpr_gap_bpcpdcm_pointwise_index_bound + S (bpr_divisor_index_bpcpdcm_pointwise) = l) -> (((exists bpr_height_bpcpdcm_pointwise_decoded. bpr_height_bpcpdcm_pointwise_decoded + S (bpr_divisor_value_bpcpdcm_pointwise) = S ((S (bpr_divisor_index_bpcpdcm_pointwise)) * c)) /\ exists bpr_quotient_bpcpdcm_pointwise_decoded. b = bpr_quotient_bpcpdcm_pointwise_decoded * S ((S (bpr_divisor_index_bpcpdcm_pointwise)) * c) + (bpr_divisor_value_bpcpdcm_pointwise))) -> exists bpr_quotient_bpcpdcm_pointwise_result. z = bpr_divisor_value_bpcpdcm_pointwise * bpr_quotient_bpcpdcm_pointwise_result) -> (exists ff_u_bpcpdcm_source ff_v_bpcpdcm_source. ((((exists ff_h_bpcpdcm_source_start. ff_h_bpcpdcm_source_start + S (1) = S ((S (0)) * ff_v_bpcpdcm_source)) /\ exists ff_q_bpcpdcm_source_start. ff_u_bpcpdcm_source = ff_q_bpcpdcm_source_start * S ((S (0)) * ff_v_bpcpdcm_source) + (1))) /\ ((((exists ff_h_bpcpdcm_source_terminal. ff_h_bpcpdcm_source_terminal + S (n) = S ((S (l)) * ff_v_bpcpdcm_source)) /\ exists ff_q_bpcpdcm_source_terminal. ff_u_bpcpdcm_source = ff_q_bpcpdcm_source_terminal * S ((S (l)) * ff_v_bpcpdcm_source) + (n))) /\ forall ff_i_bpcpdcm_source. (exists ff_lt_bpcpdcm_source_bound. ff_lt_bpcpdcm_source_bound + S ff_i_bpcpdcm_source = l) -> exists ff_p_bpcpdcm_source ff_r_bpcpdcm_source ff_s_bpcpdcm_source. ((((exists ff_h_bpcpdcm_source_factor. ff_h_bpcpdcm_source_factor + S (ff_p_bpcpdcm_source) = S ((S (ff_i_bpcpdcm_source)) * c)) /\ exists ff_q_bpcpdcm_source_factor. b = ff_q_bpcpdcm_source_factor * S ((S (ff_i_bpcpdcm_source)) * c) + (ff_p_bpcpdcm_source))) /\ ((((exists ff_h_bpcpdcm_source_partial. ff_h_bpcpdcm_source_partial + S (ff_r_bpcpdcm_source) = S ((S (ff_i_bpcpdcm_source)) * ff_v_bpcpdcm_source)) /\ exists ff_q_bpcpdcm_source_partial. ff_u_bpcpdcm_source = ff_q_bpcpdcm_source_partial * S ((S (ff_i_bpcpdcm_source)) * ff_v_bpcpdcm_source) + (ff_r_bpcpdcm_source))) /\ ((((exists ff_h_bpcpdcm_source_successor. ff_h_bpcpdcm_source_successor + S (ff_s_bpcpdcm_source) = S ((S (S ff_i_bpcpdcm_source)) * ff_v_bpcpdcm_source)) /\ exists ff_q_bpcpdcm_source_successor. ff_u_bpcpdcm_source = ff_q_bpcpdcm_source_successor * S ((S (S ff_i_bpcpdcm_source)) * ff_v_bpcpdcm_source) + (ff_s_bpcpdcm_source))) /\ ff_s_bpcpdcm_source = ff_r_bpcpdcm_source * ff_p_bpcpdcm_source)))))) -> (exists bpr_quotient_bpcpdcm_result. z = (n) * bpr_quotient_bpcpdcm_result)

Structural proof guide

A pairwise-coprime product divides every common multiple of its factors.

Direct prerequisites: beta_product_zero, beta_product_succ_decompose, le_succ, le_refl, one_multiple, lt_irrefl_expanded, beta_product_pointwise_coprime, coprime_product_is_lcm. The authored body proceeds by structural induction (1), case analysis (6), intermediate claims (9), equality transport (3).

Proof neighborhood

Direct dependencies

BT005I beta_product_zero BT005J beta_product_succ_decompose BT0018 le_succ BT000E le_refl BT0027 one_multiple BT001B lt_irrefl_expanded BT00DH beta_product_pointwise_coprime BT00BG coprime_product_is_lcm

Direct dependents

BT00VF primorial_interval_divides_choose_between BT00YY prime_contribution_product_divides

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 z
  6. 0006intro hpairwise
  7. 0007intro hpointwise
  8. 0008intro hproduct
  9. 0009have hn : n = 1
  10. 0010specialize beta_product_zero b
  11. 0011specialize beta_product_zero c
  12. 0012specialize beta_product_zero n
  13. 0013apply beta_product_zero
  14. 0014exact hproduct
  15. 0015rewrite hn
  16. 0016specialize one_multiple z
  17. 0017exact one_multiple
  18. 0018intro n
  19. 0019intro z
  20. 0020intro hpairwise
  21. 0021intro hpointwise
  22. 0022intro hproduct
  23. 0023have hdecomposition : exists p r. (((exists bpr_height_bpcpdcm_last. bpr_height_bpcpdcm_last + S (p) = S ((S (l)) * c)) /\ exists bpr_quotient_bpcpdcm_last. b = bpr_quotient_bpcpdcm_last * S ((S (l)) * c) + (p))) /\ ((exists ff_u_bpcpdcm_prefix ff_v_bpcpdcm_prefix. ((((exists ff_h_bpcpdcm_prefix_start. ff_h_bpcpdcm_prefix_start + S (1) = S ((S (0)) * ff_v_bpcpdcm_prefix)) /\ exists ff_q_bpcpdcm_prefix_start. ff_u_bpcpdcm_prefix = ff_q_bpcpdcm_prefix_start * S ((S (0)) * ff_v_bpcpdcm_prefix) + (1))) /\ ((((exists ff_h_bpcpdcm_prefix_terminal. ff_h_bpcpdcm_prefix_terminal + S (r) = S ((S (l)) * ff_v_bpcpdcm_prefix)) /\ exists ff_q_bpcpdcm_prefix_terminal. ff_u_bpcpdcm_prefix = ff_q_bpcpdcm_prefix_terminal * S ((S (l)) * ff_v_bpcpdcm_prefix) + (r))) /\ forall ff_i_bpcpdcm_prefix. (exists ff_lt_bpcpdcm_prefix_bound. ff_lt_bpcpdcm_prefix_bound + S ff_i_bpcpdcm_prefix = l) -> exists ff_p_bpcpdcm_prefix ff_r_bpcpdcm_prefix ff_s_bpcpdcm_prefix. ((((exists ff_h_bpcpdcm_prefix_factor. ff_h_bpcpdcm_prefix_factor + S (ff_p_bpcpdcm_prefix) = S ((S (ff_i_bpcpdcm_prefix)) * c)) /\ exists ff_q_bpcpdcm_prefix_factor. b = ff_q_bpcpdcm_prefix_factor * S ((S (ff_i_bpcpdcm_prefix)) * c) + (ff_p_bpcpdcm_prefix))) /\ ((((exists ff_h_bpcpdcm_prefix_partial. ff_h_bpcpdcm_prefix_partial + S (ff_r_bpcpdcm_prefix) = S ((S (ff_i_bpcpdcm_prefix)) * ff_v_bpcpdcm_prefix)) /\ exists ff_q_bpcpdcm_prefix_partial. ff_u_bpcpdcm_prefix = ff_q_bpcpdcm_prefix_partial * S ((S (ff_i_bpcpdcm_prefix)) * ff_v_bpcpdcm_prefix) + (ff_r_bpcpdcm_prefix))) /\ ((((exists ff_h_bpcpdcm_prefix_successor. ff_h_bpcpdcm_prefix_successor + S (ff_s_bpcpdcm_prefix) = S ((S (S ff_i_bpcpdcm_prefix)) * ff_v_bpcpdcm_prefix)) /\ exists ff_q_bpcpdcm_prefix_successor. ff_u_bpcpdcm_prefix = ff_q_bpcpdcm_prefix_successor * S ((S (S ff_i_bpcpdcm_prefix)) * ff_v_bpcpdcm_prefix) + (ff_s_bpcpdcm_prefix))) /\ ff_s_bpcpdcm_prefix = ff_r_bpcpdcm_prefix * ff_p_bpcpdcm_prefix)))))) /\ n = r * p)
  24. 0024specialize beta_product_succ_decompose b
  25. 0025specialize beta_product_succ_decompose c
  26. 0026specialize beta_product_succ_decompose l
  27. 0027specialize beta_product_succ_decompose n
  28. 0028apply beta_product_succ_decompose
  29. 0029exact hproduct
  30. 0030cases hdecomposition
  31. 0031cases hdecomposition_witness
  32. 0032cases hdecomposition_witness_witness
  33. 0033cases hdecomposition_witness_witness_right
  34. 0034have hprefix_pairwise : forall bpr_left_index_bpcpdcm_prefix_pairwise bpr_right_index_bpcpdcm_prefix_pairwise bpr_left_value_bpcpdcm_prefix_pairwise bpr_right_value_bpcpdcm_prefix_pairwise. (exists bpr_gap_bpcpdcm_prefix_pairwise_left_bound. bpr_gap_bpcpdcm_prefix_pairwise_left_bound + S (bpr_left_index_bpcpdcm_prefix_pairwise) = l) -> (exists bpr_gap_bpcpdcm_prefix_pairwise_right_bound. bpr_gap_bpcpdcm_prefix_pairwise_right_bound + S (bpr_right_index_bpcpdcm_prefix_pairwise) = l) -> (((exists bpr_height_bpcpdcm_prefix_pairwise_left_at. bpr_height_bpcpdcm_prefix_pairwise_left_at + S (bpr_left_value_bpcpdcm_prefix_pairwise) = S ((S (bpr_left_index_bpcpdcm_prefix_pairwise)) * c)) /\ exists bpr_quotient_bpcpdcm_prefix_pairwise_left_at. b = bpr_quotient_bpcpdcm_prefix_pairwise_left_at * S ((S (bpr_left_index_bpcpdcm_prefix_pairwise)) * c) + (bpr_left_value_bpcpdcm_prefix_pairwise))) -> (((exists bpr_height_bpcpdcm_prefix_pairwise_right_at. bpr_height_bpcpdcm_prefix_pairwise_right_at + S (bpr_right_value_bpcpdcm_prefix_pairwise) = S ((S (bpr_right_index_bpcpdcm_prefix_pairwise)) * c)) /\ exists bpr_quotient_bpcpdcm_prefix_pairwise_right_at. b = bpr_quotient_bpcpdcm_prefix_pairwise_right_at * S ((S (bpr_right_index_bpcpdcm_prefix_pairwise)) * c) + (bpr_right_value_bpcpdcm_prefix_pairwise))) -> ~(bpr_left_index_bpcpdcm_prefix_pairwise = bpr_right_index_bpcpdcm_prefix_pairwise) -> (forall bpr_coprime_divisor_bpcpdcm_prefix_pairwise_coprime. (exists bpr_coprime_left_factor_bpcpdcm_prefix_pairwise_coprime. bpr_left_value_bpcpdcm_prefix_pairwise = bpr_coprime_divisor_bpcpdcm_prefix_pairwise_coprime * bpr_coprime_left_factor_bpcpdcm_prefix_pairwise_coprime) -> (exists bpr_coprime_right_factor_bpcpdcm_prefix_pairwise_coprime. bpr_right_value_bpcpdcm_prefix_pairwise = bpr_coprime_divisor_bpcpdcm_prefix_pairwise_coprime * bpr_coprime_right_factor_bpcpdcm_prefix_pairwise_coprime) -> bpr_coprime_divisor_bpcpdcm_prefix_pairwise_coprime = 1)
  35. 0035intro i
  36. 0036intro j
  37. 0037intro p
  38. 0038intro q
  39. 0039intro hi
  40. 0040intro hj
  41. 0041intro hp
  42. 0042intro hq
  43. 0043intro hij
  44. 0044specialize hpairwise i
  45. 0045specialize hpairwise j
  46. 0046specialize hpairwise p
  47. 0047specialize hpairwise q
  48. 0048apply hpairwise
  49. 0049specialize le_succ (S i)
  50. 0050specialize le_succ l
  51. 0051apply le_succ
  52. 0052exact hi
  53. 0053specialize le_succ (S j)
  54. 0054specialize le_succ l
  55. 0055apply le_succ
  56. 0056exact hj
  57. 0057exact hp
  58. 0058exact hq
  59. 0059exact hij
  60. 0060have hprefix_pointwise : forall bpr_divisor_index_bpcpdcm_prefix_pointwise bpr_divisor_value_bpcpdcm_prefix_pointwise. (exists bpr_gap_bpcpdcm_prefix_pointwise_index_bound. bpr_gap_bpcpdcm_prefix_pointwise_index_bound + S (bpr_divisor_index_bpcpdcm_prefix_pointwise) = l) -> (((exists bpr_height_bpcpdcm_prefix_pointwise_decoded. bpr_height_bpcpdcm_prefix_pointwise_decoded + S (bpr_divisor_value_bpcpdcm_prefix_pointwise) = S ((S (bpr_divisor_index_bpcpdcm_prefix_pointwise)) * c)) /\ exists bpr_quotient_bpcpdcm_prefix_pointwise_decoded. b = bpr_quotient_bpcpdcm_prefix_pointwise_decoded * S ((S (bpr_divisor_index_bpcpdcm_prefix_pointwise)) * c) + (bpr_divisor_value_bpcpdcm_prefix_pointwise))) -> exists bpr_quotient_bpcpdcm_prefix_pointwise_result. z = bpr_divisor_value_bpcpdcm_prefix_pointwise * bpr_quotient_bpcpdcm_prefix_pointwise_result
  61. 0061intro i
  62. 0062intro p
  63. 0063intro hi
  64. 0064intro hp
  65. 0065specialize hpointwise i
  66. 0066specialize hpointwise p
  67. 0067apply hpointwise
  68. 0068specialize le_succ (S i)
  69. 0069specialize le_succ l
  70. 0070apply le_succ
  71. 0071exact hi
  72. 0072exact hp
  73. 0073have hprefix_divides : exists q. z = x1 * q
  74. 0074specialize IH x1
  75. 0075specialize IH z
  76. 0076apply IH
  77. 0077exact hprefix_pairwise
  78. 0078exact hprefix_pointwise
  79. 0079exact hdecomposition_witness_witness_right_left
  80. 0080have hlast_divides : exists q. z = x * q
  81. 0081specialize hpointwise l
  82. 0082specialize hpointwise x
  83. 0083apply hpointwise
  84. 0084specialize le_refl (S l)
  85. 0085exact le_refl
  86. 0086exact hdecomposition_witness_witness_left
  87. 0087have hcoprime : forall bpr_coprime_divisor_bpcpdcm_local_coprime. (exists bpr_coprime_left_factor_bpcpdcm_local_coprime. x1 = bpr_coprime_divisor_bpcpdcm_local_coprime * bpr_coprime_left_factor_bpcpdcm_local_coprime) -> (exists bpr_coprime_right_factor_bpcpdcm_local_coprime. x = bpr_coprime_divisor_bpcpdcm_local_coprime * bpr_coprime_right_factor_bpcpdcm_local_coprime) -> bpr_coprime_divisor_bpcpdcm_local_coprime = 1
  88. 0088specialize beta_product_pointwise_coprime x
  89. 0089specialize beta_product_pointwise_coprime b
  90. 0090specialize beta_product_pointwise_coprime c
  91. 0091specialize beta_product_pointwise_coprime l
  92. 0092specialize beta_product_pointwise_coprime x1
  93. 0093apply beta_product_pointwise_coprime
  94. 0094intro i
  95. 0095intro q
  96. 0096intro hi
  97. 0097intro hq
  98. 0098specialize hpairwise i
  99. 0099specialize hpairwise l
  100. 0100specialize hpairwise q
  101. 0101specialize hpairwise x
  102. 0102apply hpairwise
  103. 0103specialize le_succ (S i)
  104. 0104specialize le_succ l
  105. 0105apply le_succ
  106. 0106exact hi
  107. 0107specialize le_refl (S l)
  108. 0108exact le_refl
  109. 0109exact hq
  110. 0110exact hdecomposition_witness_witness_left
  111. 0111intro hil
  112. 0112rewrite hil at hi
  113. 0113specialize lt_irrefl_expanded l
  114. 0114apply lt_irrefl_expanded
  115. 0115exact hi
  116. 0116exact hdecomposition_witness_witness_right_left
  117. 0117have hlcm : ((((exists u. x1 * x = x1 * u) /\ exists v. x1 * x = x * v) /\ forall t. (exists a. t = x1 * a) -> (exists d. t = x * d) -> exists q. t = (x1 * x) * q))
  118. 0118specialize coprime_product_is_lcm x1
  119. 0119specialize coprime_product_is_lcm x
  120. 0120apply coprime_product_is_lcm
  121. 0121exact hcoprime
  122. 0122cases hlcm
  123. 0123cases hlcm_left
  124. 0124have hresult : exists q. z = (x1 * x) * q
  125. 0125specialize hlcm_right z
  126. 0126apply hlcm_right
  127. 0127exact hprefix_divides
  128. 0128exact hlast_divides
  129. 0129rewrite hdecomposition_witness_witness_right_right
  130. 0130exact hresult