BT00YV

coprime_powers

Alpha body-checked · checked-use disabled

Powers of coprime bases are coprime.

Exact expanded PA statement

forall p q e f a z. (forall bpr_coprime_divisor_bcpowers_source. (exists bpr_coprime_left_bcpowers_source. p = bpr_coprime_divisor_bcpowers_source * bpr_coprime_left_bcpowers_source) -> (exists bpr_coprime_right_bcpowers_source. q = bpr_coprime_divisor_bcpowers_source * bpr_coprime_right_bcpowers_source) -> bpr_coprime_divisor_bcpowers_source = 1) -> (exists bpr_power_code_bcpowers_left bpr_power_scale_bcpowers_left. ((forall bpr_power_index_bcpowers_left. (exists bpr_gap_bcpowers_left_repeat_bound. bpr_gap_bcpowers_left_repeat_bound + S (bpr_power_index_bcpowers_left) = e) -> (((exists bpr_height_bcpowers_left_repeat_entry. bpr_height_bcpowers_left_repeat_entry + S (p) = S ((S (bpr_power_index_bcpowers_left)) * bpr_power_scale_bcpowers_left)) /\ exists bpr_quotient_bcpowers_left_repeat_entry. bpr_power_code_bcpowers_left = bpr_quotient_bcpowers_left_repeat_entry * S ((S (bpr_power_index_bcpowers_left)) * bpr_power_scale_bcpowers_left) + (p)))) /\ (exists ff_u_bcpowers_left_product ff_v_bcpowers_left_product. ((((exists ff_h_bcpowers_left_product_start. ff_h_bcpowers_left_product_start + S (1) = S ((S (0)) * ff_v_bcpowers_left_product)) /\ exists ff_q_bcpowers_left_product_start. ff_u_bcpowers_left_product = ff_q_bcpowers_left_product_start * S ((S (0)) * ff_v_bcpowers_left_product) + (1))) /\ ((((exists ff_h_bcpowers_left_product_terminal. ff_h_bcpowers_left_product_terminal + S (a) = S ((S (e)) * ff_v_bcpowers_left_product)) /\ exists ff_q_bcpowers_left_product_terminal. ff_u_bcpowers_left_product = ff_q_bcpowers_left_product_terminal * S ((S (e)) * ff_v_bcpowers_left_product) + (a))) /\ forall ff_i_bcpowers_left_product. (exists ff_lt_bcpowers_left_product_bound. ff_lt_bcpowers_left_product_bound + S ff_i_bcpowers_left_product = e) -> exists ff_p_bcpowers_left_product ff_r_bcpowers_left_product ff_s_bcpowers_left_product. ((((exists ff_h_bcpowers_left_product_factor. ff_h_bcpowers_left_product_factor + S (ff_p_bcpowers_left_product) = S ((S (ff_i_bcpowers_left_product)) * bpr_power_scale_bcpowers_left)) /\ exists ff_q_bcpowers_left_product_factor. bpr_power_code_bcpowers_left = ff_q_bcpowers_left_product_factor * S ((S (ff_i_bcpowers_left_product)) * bpr_power_scale_bcpowers_left) + (ff_p_bcpowers_left_product))) /\ ((((exists ff_h_bcpowers_left_product_partial. ff_h_bcpowers_left_product_partial + S (ff_r_bcpowers_left_product) = S ((S (ff_i_bcpowers_left_product)) * ff_v_bcpowers_left_product)) /\ exists ff_q_bcpowers_left_product_partial. ff_u_bcpowers_left_product = ff_q_bcpowers_left_product_partial * S ((S (ff_i_bcpowers_left_product)) * ff_v_bcpowers_left_product) + (ff_r_bcpowers_left_product))) /\ ((((exists ff_h_bcpowers_left_product_successor. ff_h_bcpowers_left_product_successor + S (ff_s_bcpowers_left_product) = S ((S (S ff_i_bcpowers_left_product)) * ff_v_bcpowers_left_product)) /\ exists ff_q_bcpowers_left_product_successor. ff_u_bcpowers_left_product = ff_q_bcpowers_left_product_successor * S ((S (S ff_i_bcpowers_left_product)) * ff_v_bcpowers_left_product) + (ff_s_bcpowers_left_product))) /\ ff_s_bcpowers_left_product = ff_r_bcpowers_left_product * ff_p_bcpowers_left_product)))))))) -> (exists bpr_power_code_bcpowers_right bpr_power_scale_bcpowers_right. ((forall bpr_power_index_bcpowers_right. (exists bpr_gap_bcpowers_right_repeat_bound. bpr_gap_bcpowers_right_repeat_bound + S (bpr_power_index_bcpowers_right) = f) -> (((exists bpr_height_bcpowers_right_repeat_entry. bpr_height_bcpowers_right_repeat_entry + S (q) = S ((S (bpr_power_index_bcpowers_right)) * bpr_power_scale_bcpowers_right)) /\ exists bpr_quotient_bcpowers_right_repeat_entry. bpr_power_code_bcpowers_right = bpr_quotient_bcpowers_right_repeat_entry * S ((S (bpr_power_index_bcpowers_right)) * bpr_power_scale_bcpowers_right) + (q)))) /\ (exists ff_u_bcpowers_right_product ff_v_bcpowers_right_product. ((((exists ff_h_bcpowers_right_product_start. ff_h_bcpowers_right_product_start + S (1) = S ((S (0)) * ff_v_bcpowers_right_product)) /\ exists ff_q_bcpowers_right_product_start. ff_u_bcpowers_right_product = ff_q_bcpowers_right_product_start * S ((S (0)) * ff_v_bcpowers_right_product) + (1))) /\ ((((exists ff_h_bcpowers_right_product_terminal. ff_h_bcpowers_right_product_terminal + S (z) = S ((S (f)) * ff_v_bcpowers_right_product)) /\ exists ff_q_bcpowers_right_product_terminal. ff_u_bcpowers_right_product = ff_q_bcpowers_right_product_terminal * S ((S (f)) * ff_v_bcpowers_right_product) + (z))) /\ forall ff_i_bcpowers_right_product. (exists ff_lt_bcpowers_right_product_bound. ff_lt_bcpowers_right_product_bound + S ff_i_bcpowers_right_product = f) -> exists ff_p_bcpowers_right_product ff_r_bcpowers_right_product ff_s_bcpowers_right_product. ((((exists ff_h_bcpowers_right_product_factor. ff_h_bcpowers_right_product_factor + S (ff_p_bcpowers_right_product) = S ((S (ff_i_bcpowers_right_product)) * bpr_power_scale_bcpowers_right)) /\ exists ff_q_bcpowers_right_product_factor. bpr_power_code_bcpowers_right = ff_q_bcpowers_right_product_factor * S ((S (ff_i_bcpowers_right_product)) * bpr_power_scale_bcpowers_right) + (ff_p_bcpowers_right_product))) /\ ((((exists ff_h_bcpowers_right_product_partial. ff_h_bcpowers_right_product_partial + S (ff_r_bcpowers_right_product) = S ((S (ff_i_bcpowers_right_product)) * ff_v_bcpowers_right_product)) /\ exists ff_q_bcpowers_right_product_partial. ff_u_bcpowers_right_product = ff_q_bcpowers_right_product_partial * S ((S (ff_i_bcpowers_right_product)) * ff_v_bcpowers_right_product) + (ff_r_bcpowers_right_product))) /\ ((((exists ff_h_bcpowers_right_product_successor. ff_h_bcpowers_right_product_successor + S (ff_s_bcpowers_right_product) = S ((S (S ff_i_bcpowers_right_product)) * ff_v_bcpowers_right_product)) /\ exists ff_q_bcpowers_right_product_successor. ff_u_bcpowers_right_product = ff_q_bcpowers_right_product_successor * S ((S (S ff_i_bcpowers_right_product)) * ff_v_bcpowers_right_product) + (ff_s_bcpowers_right_product))) /\ ff_s_bcpowers_right_product = ff_r_bcpowers_right_product * ff_p_bcpowers_right_product)))))))) -> (forall bpr_coprime_divisor_bcpowers_result. (exists bpr_coprime_left_bcpowers_result. a = bpr_coprime_divisor_bcpowers_result * bpr_coprime_left_bcpowers_result) -> (exists bpr_coprime_right_bcpowers_result. z = bpr_coprime_divisor_bcpowers_result * bpr_coprime_right_bcpowers_result) -> bpr_coprime_divisor_bcpowers_result = 1)

Structural proof guide

Powers of coprime bases are coprime.

Direct prerequisites: pow_zero, pow_successor_decompose, coprime_one_left, coprime_mul_left, coprime_power_right. The authored body proceeds by structural induction (1), case analysis (2), intermediate claims (4), equality transport (2).

Proof neighborhood

Direct dependencies

BT0081 pow_zero BT0083 pow_successor_decompose BT002Y coprime_one_left BT004R coprime_mul_left BT00YU coprime_power_right

Direct dependents

BT00YW prime_contribution_prefix_pairwise_coprime

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro p
  2. 0002intro q
  3. 0003induction e
  4. 0004intro f
  5. 0005intro a
  6. 0006intro z
  7. 0007intro hcoprime
  8. 0008intro hleft
  9. 0009intro hright
  10. 0010have hvalue : a = 1
  11. 0011specialize pow_zero p
  12. 0012specialize pow_zero 0
  13. 0013specialize pow_zero a
  14. 0014apply pow_zero
  15. 0015refl
  16. 0016exact hleft
  17. 0017rewrite hvalue
  18. 0018specialize coprime_one_left z
  19. 0019apply coprime_one_left
  20. 0020intro f
  21. 0021intro a
  22. 0022intro z
  23. 0023intro hcoprime
  24. 0024intro hleft
  25. 0025intro hright
  26. 0026have hdecomposition : exists r. (exists bpr_power_code_bcpowers_previous bpr_power_scale_bcpowers_previous. ((forall bpr_power_index_bcpowers_previous. (exists bpr_gap_bcpowers_previous_repeat_bound. bpr_gap_bcpowers_previous_repeat_bound + S (bpr_power_index_bcpowers_previous) = e) -> (((exists bpr_height_bcpowers_previous_repeat_entry. bpr_height_bcpowers_previous_repeat_entry + S (p) = S ((S (bpr_power_index_bcpowers_previous)) * bpr_power_scale_bcpowers_previous)) /\ exists bpr_quotient_bcpowers_previous_repeat_entry. bpr_power_code_bcpowers_previous = bpr_quotient_bcpowers_previous_repeat_entry * S ((S (bpr_power_index_bcpowers_previous)) * bpr_power_scale_bcpowers_previous) + (p)))) /\ (exists ff_u_bcpowers_previous_product ff_v_bcpowers_previous_product. ((((exists ff_h_bcpowers_previous_product_start. ff_h_bcpowers_previous_product_start + S (1) = S ((S (0)) * ff_v_bcpowers_previous_product)) /\ exists ff_q_bcpowers_previous_product_start. ff_u_bcpowers_previous_product = ff_q_bcpowers_previous_product_start * S ((S (0)) * ff_v_bcpowers_previous_product) + (1))) /\ ((((exists ff_h_bcpowers_previous_product_terminal. ff_h_bcpowers_previous_product_terminal + S (r) = S ((S (e)) * ff_v_bcpowers_previous_product)) /\ exists ff_q_bcpowers_previous_product_terminal. ff_u_bcpowers_previous_product = ff_q_bcpowers_previous_product_terminal * S ((S (e)) * ff_v_bcpowers_previous_product) + (r))) /\ forall ff_i_bcpowers_previous_product. (exists ff_lt_bcpowers_previous_product_bound. ff_lt_bcpowers_previous_product_bound + S ff_i_bcpowers_previous_product = e) -> exists ff_p_bcpowers_previous_product ff_r_bcpowers_previous_product ff_s_bcpowers_previous_product. ((((exists ff_h_bcpowers_previous_product_factor. ff_h_bcpowers_previous_product_factor + S (ff_p_bcpowers_previous_product) = S ((S (ff_i_bcpowers_previous_product)) * bpr_power_scale_bcpowers_previous)) /\ exists ff_q_bcpowers_previous_product_factor. bpr_power_code_bcpowers_previous = ff_q_bcpowers_previous_product_factor * S ((S (ff_i_bcpowers_previous_product)) * bpr_power_scale_bcpowers_previous) + (ff_p_bcpowers_previous_product))) /\ ((((exists ff_h_bcpowers_previous_product_partial. ff_h_bcpowers_previous_product_partial + S (ff_r_bcpowers_previous_product) = S ((S (ff_i_bcpowers_previous_product)) * ff_v_bcpowers_previous_product)) /\ exists ff_q_bcpowers_previous_product_partial. ff_u_bcpowers_previous_product = ff_q_bcpowers_previous_product_partial * S ((S (ff_i_bcpowers_previous_product)) * ff_v_bcpowers_previous_product) + (ff_r_bcpowers_previous_product))) /\ ((((exists ff_h_bcpowers_previous_product_successor. ff_h_bcpowers_previous_product_successor + S (ff_s_bcpowers_previous_product) = S ((S (S ff_i_bcpowers_previous_product)) * ff_v_bcpowers_previous_product)) /\ exists ff_q_bcpowers_previous_product_successor. ff_u_bcpowers_previous_product = ff_q_bcpowers_previous_product_successor * S ((S (S ff_i_bcpowers_previous_product)) * ff_v_bcpowers_previous_product) + (ff_s_bcpowers_previous_product))) /\ ff_s_bcpowers_previous_product = ff_r_bcpowers_previous_product * ff_p_bcpowers_previous_product)))))))) /\ a = r * p
  27. 0027specialize pow_successor_decompose p
  28. 0028specialize pow_successor_decompose e
  29. 0029specialize pow_successor_decompose (S e)
  30. 0030specialize pow_successor_decompose a
  31. 0031apply pow_successor_decompose
  32. 0032refl
  33. 0033exact hleft
  34. 0034cases hdecomposition
  35. 0035cases hdecomposition_witness
  36. 0036have hprefix : forall d. (exists u. x = d * u) -> (exists v. z = d * v) -> d = 1
  37. 0037specialize IH f
  38. 0038specialize IH x
  39. 0039specialize IH z
  40. 0040apply IH
  41. 0041exact hcoprime
  42. 0042exact hdecomposition_witness_left
  43. 0043exact hright
  44. 0044have hlast : forall d. (exists u. p = d * u) -> (exists v. z = d * v) -> d = 1
  45. 0045specialize coprime_power_right p
  46. 0046specialize coprime_power_right q
  47. 0047specialize coprime_power_right f
  48. 0048specialize coprime_power_right z
  49. 0049apply coprime_power_right
  50. 0050exact hcoprime
  51. 0051exact hright
  52. 0052rewrite hdecomposition_witness_right
  53. 0053apply coprime_mul_left
  54. 0054exact hprefix
  55. 0055exact hlast