PA0081

beta_product_pointwise_coprime

Alpha v16 checked-use theorem · independently closed; not Stable

A finite product of factors pointwise coprime to m is coprime to m.

Exact expanded PA statement

forall m b c l z. (forall frp_index_pointwise frp_factor_pointwise. (exists frp_gap_pointwise_bound. frp_gap_pointwise_bound + S frp_index_pointwise = l) -> (((exists ff_h_frp_pointwise_decoded. ff_h_frp_pointwise_decoded + S (frp_factor_pointwise) = S ((S (frp_index_pointwise)) * c)) /\ exists ff_q_frp_pointwise_decoded. b = ff_q_frp_pointwise_decoded * S ((S (frp_index_pointwise)) * c) + (frp_factor_pointwise))) -> (forall frp_divisor_pointwise_coprime. (exists frp_left_factor_pointwise_coprime. frp_factor_pointwise = frp_divisor_pointwise_coprime * frp_left_factor_pointwise_coprime) -> (exists frp_right_factor_pointwise_coprime. m = frp_divisor_pointwise_coprime * frp_right_factor_pointwise_coprime) -> frp_divisor_pointwise_coprime = 1)) -> (exists ff_u_pointwise_product ff_v_pointwise_product. ((((exists ff_h_pointwise_product_start. ff_h_pointwise_product_start + S (1) = S ((S (0)) * ff_v_pointwise_product)) /\ exists ff_q_pointwise_product_start. ff_u_pointwise_product = ff_q_pointwise_product_start * S ((S (0)) * ff_v_pointwise_product) + (1))) /\ ((((exists ff_h_pointwise_product_terminal. ff_h_pointwise_product_terminal + S (z) = S ((S (l)) * ff_v_pointwise_product)) /\ exists ff_q_pointwise_product_terminal. ff_u_pointwise_product = ff_q_pointwise_product_terminal * S ((S (l)) * ff_v_pointwise_product) + (z))) /\ forall ff_i_pointwise_product. (exists ff_lt_pointwise_product_bound. ff_lt_pointwise_product_bound + S ff_i_pointwise_product = l) -> exists ff_p_pointwise_product ff_r_pointwise_product ff_s_pointwise_product. ((((exists ff_h_pointwise_product_factor. ff_h_pointwise_product_factor + S (ff_p_pointwise_product) = S ((S (ff_i_pointwise_product)) * c)) /\ exists ff_q_pointwise_product_factor. b = ff_q_pointwise_product_factor * S ((S (ff_i_pointwise_product)) * c) + (ff_p_pointwise_product))) /\ ((((exists ff_h_pointwise_product_partial. ff_h_pointwise_product_partial + S (ff_r_pointwise_product) = S ((S (ff_i_pointwise_product)) * ff_v_pointwise_product)) /\ exists ff_q_pointwise_product_partial. ff_u_pointwise_product = ff_q_pointwise_product_partial * S ((S (ff_i_pointwise_product)) * ff_v_pointwise_product) + (ff_r_pointwise_product))) /\ ((((exists ff_h_pointwise_product_successor. ff_h_pointwise_product_successor + S (ff_s_pointwise_product) = S ((S (S ff_i_pointwise_product)) * ff_v_pointwise_product)) /\ exists ff_q_pointwise_product_successor. ff_u_pointwise_product = ff_q_pointwise_product_successor * S ((S (S ff_i_pointwise_product)) * ff_v_pointwise_product) + (ff_s_pointwise_product))) /\ ff_s_pointwise_product = ff_r_pointwise_product * ff_p_pointwise_product)))))) -> (forall frp_divisor_pointwise_result. (exists frp_left_factor_pointwise_result. z = frp_divisor_pointwise_result * frp_left_factor_pointwise_result) -> (exists frp_right_factor_pointwise_result. m = frp_divisor_pointwise_result * frp_right_factor_pointwise_result) -> frp_divisor_pointwise_result = 1)

Structural proof guide

Generated structural guide

A finite product of factors pointwise coprime to m is coprime to m.

Use the direct prerequisites beta_product_zero, beta_product_succ_decompose, le_succ, le_refl, coprime_one_left, coprime_mul_left as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (4), intermediate claims (5), equality transport (2).

Referenced ingredients

PA0049 beta_product_zero PA004A beta_product_succ_decompose PA002O le_succ PA001A le_refl PA000P coprime_one_left PA001T coprime_mul_left

Proof neighborhood

Direct dependencies

PA0049 beta_product_zero PA004A beta_product_succ_decompose PA002O le_succ PA001A le_refl PA000P coprime_one_left PA001T coprime_mul_left

Direct dependents

PA0082 prime_positive_bounded_product_coprime PA008K prime_range_product_coprime

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro m
  2. 0002intro b
  3. 0003intro c
  4. 0004induction l
  5. 0005intro z
  6. 0006intro hpw
  7. 0007intro hproduct
  8. 0008have hz : z = 1
  9. 0009specialize beta_product_zero b
  10. 0010specialize beta_product_zero c
  11. 0011specialize beta_product_zero z
  12. 0012apply beta_product_zero
  13. 0013exact hproduct
  14. 0014rewrite hz
  15. 0015specialize coprime_one_left m
  16. 0016exact coprime_one_left
  17. 0017intro z
  18. 0018intro hpw
  19. 0019intro hproduct
  20. 0020have hdecomp : exists p r. (((exists ff_h_frp_final_factor. ff_h_frp_final_factor + S (p) = S ((S (l)) * c)) /\ exists ff_q_frp_final_factor. b = ff_q_frp_final_factor * S ((S (l)) * c) + (p))) /\ ((exists ff_u_pointwise_prefix_product ff_v_pointwise_prefix_product. ((((exists ff_h_pointwise_prefix_product_start. ff_h_pointwise_prefix_product_start + S (1) = S ((S (0)) * ff_v_pointwise_prefix_product)) /\ exists ff_q_pointwise_prefix_product_start. ff_u_pointwise_prefix_product = ff_q_pointwise_prefix_product_start * S ((S (0)) * ff_v_pointwise_prefix_product) + (1))) /\ ((((exists ff_h_pointwise_prefix_product_terminal. ff_h_pointwise_prefix_product_terminal + S (r) = S ((S (l)) * ff_v_pointwise_prefix_product)) /\ exists ff_q_pointwise_prefix_product_terminal. ff_u_pointwise_prefix_product = ff_q_pointwise_prefix_product_terminal * S ((S (l)) * ff_v_pointwise_prefix_product) + (r))) /\ forall ff_i_pointwise_prefix_product. (exists ff_lt_pointwise_prefix_product_bound. ff_lt_pointwise_prefix_product_bound + S ff_i_pointwise_prefix_product = l) -> exists ff_p_pointwise_prefix_product ff_r_pointwise_prefix_product ff_s_pointwise_prefix_product. ((((exists ff_h_pointwise_prefix_product_factor. ff_h_pointwise_prefix_product_factor + S (ff_p_pointwise_prefix_product) = S ((S (ff_i_pointwise_prefix_product)) * c)) /\ exists ff_q_pointwise_prefix_product_factor. b = ff_q_pointwise_prefix_product_factor * S ((S (ff_i_pointwise_prefix_product)) * c) + (ff_p_pointwise_prefix_product))) /\ ((((exists ff_h_pointwise_prefix_product_partial. ff_h_pointwise_prefix_product_partial + S (ff_r_pointwise_prefix_product) = S ((S (ff_i_pointwise_prefix_product)) * ff_v_pointwise_prefix_product)) /\ exists ff_q_pointwise_prefix_product_partial. ff_u_pointwise_prefix_product = ff_q_pointwise_prefix_product_partial * S ((S (ff_i_pointwise_prefix_product)) * ff_v_pointwise_prefix_product) + (ff_r_pointwise_prefix_product))) /\ ((((exists ff_h_pointwise_prefix_product_successor. ff_h_pointwise_prefix_product_successor + S (ff_s_pointwise_prefix_product) = S ((S (S ff_i_pointwise_prefix_product)) * ff_v_pointwise_prefix_product)) /\ exists ff_q_pointwise_prefix_product_successor. ff_u_pointwise_prefix_product = ff_q_pointwise_prefix_product_successor * S ((S (S ff_i_pointwise_prefix_product)) * ff_v_pointwise_prefix_product) + (ff_s_pointwise_prefix_product))) /\ ff_s_pointwise_prefix_product = ff_r_pointwise_prefix_product * ff_p_pointwise_prefix_product)))))) /\ z = r * p)
  21. 0021specialize beta_product_succ_decompose b
  22. 0022specialize beta_product_succ_decompose c
  23. 0023specialize beta_product_succ_decompose l
  24. 0024specialize beta_product_succ_decompose z
  25. 0025apply beta_product_succ_decompose
  26. 0026exact hproduct
  27. 0027cases hdecomp
  28. 0028cases hdecomp_witness
  29. 0029cases hdecomp_witness_witness
  30. 0030cases hdecomp_witness_witness_right
  31. 0031have hpw_prefix : forall frp_index_pointwise_prefix frp_factor_pointwise_prefix. (exists frp_gap_pointwise_prefix_bound. frp_gap_pointwise_prefix_bound + S frp_index_pointwise_prefix = l) -> (((exists ff_h_frp_pointwise_prefix_decoded. ff_h_frp_pointwise_prefix_decoded + S (frp_factor_pointwise_prefix) = S ((S (frp_index_pointwise_prefix)) * c)) /\ exists ff_q_frp_pointwise_prefix_decoded. b = ff_q_frp_pointwise_prefix_decoded * S ((S (frp_index_pointwise_prefix)) * c) + (frp_factor_pointwise_prefix))) -> (forall frp_divisor_pointwise_prefix_coprime. (exists frp_left_factor_pointwise_prefix_coprime. frp_factor_pointwise_prefix = frp_divisor_pointwise_prefix_coprime * frp_left_factor_pointwise_prefix_coprime) -> (exists frp_right_factor_pointwise_prefix_coprime. m = frp_divisor_pointwise_prefix_coprime * frp_right_factor_pointwise_prefix_coprime) -> frp_divisor_pointwise_prefix_coprime = 1)
  32. 0032intro i
  33. 0033intro x2
  34. 0034intro hi
  35. 0035intro hx2
  36. 0036specialize hpw i
  37. 0037specialize hpw x2
  38. 0038apply hpw
  39. 0039specialize le_succ (S i)
  40. 0040specialize le_succ l
  41. 0041apply le_succ
  42. 0042exact hi
  43. 0043exact hx2
  44. 0044have hprefix : forall frp_divisor_prefix_result. (exists frp_left_factor_prefix_result. x1 = frp_divisor_prefix_result * frp_left_factor_prefix_result) -> (exists frp_right_factor_prefix_result. m = frp_divisor_prefix_result * frp_right_factor_prefix_result) -> frp_divisor_prefix_result = 1
  45. 0045specialize IH x1
  46. 0046apply IH
  47. 0047exact hpw_prefix
  48. 0048exact hdecomp_witness_witness_right_left
  49. 0049have hfactor : forall frp_divisor_last_factor. (exists frp_left_factor_last_factor. x = frp_divisor_last_factor * frp_left_factor_last_factor) -> (exists frp_right_factor_last_factor. m = frp_divisor_last_factor * frp_right_factor_last_factor) -> frp_divisor_last_factor = 1
  50. 0050specialize hpw l
  51. 0051specialize hpw x
  52. 0052apply hpw
  53. 0053specialize le_refl (S l)
  54. 0054exact le_refl
  55. 0055exact hdecomp_witness_witness_left
  56. 0056rewrite hdecomp_witness_witness_right_right
  57. 0057specialize coprime_mul_left x1
  58. 0058specialize coprime_mul_left x
  59. 0059specialize coprime_mul_left m
  60. 0060apply coprime_mul_left
  61. 0061exact hprefix
  62. 0062exact hfactor