BT00YU

coprime_power_right

Alpha body-checked · checked-use disabled

A power preserves coprimality with a fixed left operand.

Exact expanded PA statement

forall p q e z. (forall bpr_coprime_divisor_bcpr_source. (exists bpr_coprime_left_bcpr_source. p = bpr_coprime_divisor_bcpr_source * bpr_coprime_left_bcpr_source) -> (exists bpr_coprime_right_bcpr_source. q = bpr_coprime_divisor_bcpr_source * bpr_coprime_right_bcpr_source) -> bpr_coprime_divisor_bcpr_source = 1) -> (exists bpr_power_code_bcpr_power bpr_power_scale_bcpr_power. ((forall bpr_power_index_bcpr_power. (exists bpr_gap_bcpr_power_repeat_bound. bpr_gap_bcpr_power_repeat_bound + S (bpr_power_index_bcpr_power) = e) -> (((exists bpr_height_bcpr_power_repeat_entry. bpr_height_bcpr_power_repeat_entry + S (q) = S ((S (bpr_power_index_bcpr_power)) * bpr_power_scale_bcpr_power)) /\ exists bpr_quotient_bcpr_power_repeat_entry. bpr_power_code_bcpr_power = bpr_quotient_bcpr_power_repeat_entry * S ((S (bpr_power_index_bcpr_power)) * bpr_power_scale_bcpr_power) + (q)))) /\ (exists ff_u_bcpr_power_product ff_v_bcpr_power_product. ((((exists ff_h_bcpr_power_product_start. ff_h_bcpr_power_product_start + S (1) = S ((S (0)) * ff_v_bcpr_power_product)) /\ exists ff_q_bcpr_power_product_start. ff_u_bcpr_power_product = ff_q_bcpr_power_product_start * S ((S (0)) * ff_v_bcpr_power_product) + (1))) /\ ((((exists ff_h_bcpr_power_product_terminal. ff_h_bcpr_power_product_terminal + S (z) = S ((S (e)) * ff_v_bcpr_power_product)) /\ exists ff_q_bcpr_power_product_terminal. ff_u_bcpr_power_product = ff_q_bcpr_power_product_terminal * S ((S (e)) * ff_v_bcpr_power_product) + (z))) /\ forall ff_i_bcpr_power_product. (exists ff_lt_bcpr_power_product_bound. ff_lt_bcpr_power_product_bound + S ff_i_bcpr_power_product = e) -> exists ff_p_bcpr_power_product ff_r_bcpr_power_product ff_s_bcpr_power_product. ((((exists ff_h_bcpr_power_product_factor. ff_h_bcpr_power_product_factor + S (ff_p_bcpr_power_product) = S ((S (ff_i_bcpr_power_product)) * bpr_power_scale_bcpr_power)) /\ exists ff_q_bcpr_power_product_factor. bpr_power_code_bcpr_power = ff_q_bcpr_power_product_factor * S ((S (ff_i_bcpr_power_product)) * bpr_power_scale_bcpr_power) + (ff_p_bcpr_power_product))) /\ ((((exists ff_h_bcpr_power_product_partial. ff_h_bcpr_power_product_partial + S (ff_r_bcpr_power_product) = S ((S (ff_i_bcpr_power_product)) * ff_v_bcpr_power_product)) /\ exists ff_q_bcpr_power_product_partial. ff_u_bcpr_power_product = ff_q_bcpr_power_product_partial * S ((S (ff_i_bcpr_power_product)) * ff_v_bcpr_power_product) + (ff_r_bcpr_power_product))) /\ ((((exists ff_h_bcpr_power_product_successor. ff_h_bcpr_power_product_successor + S (ff_s_bcpr_power_product) = S ((S (S ff_i_bcpr_power_product)) * ff_v_bcpr_power_product)) /\ exists ff_q_bcpr_power_product_successor. ff_u_bcpr_power_product = ff_q_bcpr_power_product_successor * S ((S (S ff_i_bcpr_power_product)) * ff_v_bcpr_power_product) + (ff_s_bcpr_power_product))) /\ ff_s_bcpr_power_product = ff_r_bcpr_power_product * ff_p_bcpr_power_product)))))))) -> (forall bpr_coprime_divisor_bcpr_result. (exists bpr_coprime_left_bcpr_result. p = bpr_coprime_divisor_bcpr_result * bpr_coprime_left_bcpr_result) -> (exists bpr_coprime_right_bcpr_result. z = bpr_coprime_divisor_bcpr_result * bpr_coprime_right_bcpr_result) -> bpr_coprime_divisor_bcpr_result = 1)

Structural proof guide

A power preserves coprimality with a fixed left operand.

Direct prerequisites: pow_zero, pow_successor_decompose, coprime_one_right, coprime_mul_right. The authored body proceeds by structural induction (1), case analysis (2), intermediate claims (3), equality transport (2).

Proof neighborhood

Direct dependencies

BT0081 pow_zero BT0083 pow_successor_decompose BT002X coprime_one_right BT004S coprime_mul_right

Direct dependents

BT00YV coprime_powers

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 z
  5. 0005intro hcoprime
  6. 0006intro hpower
  7. 0007have hvalue : z = 1
  8. 0008specialize pow_zero q
  9. 0009specialize pow_zero 0
  10. 0010specialize pow_zero z
  11. 0011apply pow_zero
  12. 0012refl
  13. 0013exact hpower
  14. 0014rewrite hvalue
  15. 0015specialize coprime_one_right p
  16. 0016apply coprime_one_right
  17. 0017intro z
  18. 0018intro hcoprime
  19. 0019intro hpower
  20. 0020have hdecomposition : exists r. (exists bpr_power_code_bcpr_previous bpr_power_scale_bcpr_previous. ((forall bpr_power_index_bcpr_previous. (exists bpr_gap_bcpr_previous_repeat_bound. bpr_gap_bcpr_previous_repeat_bound + S (bpr_power_index_bcpr_previous) = e) -> (((exists bpr_height_bcpr_previous_repeat_entry. bpr_height_bcpr_previous_repeat_entry + S (q) = S ((S (bpr_power_index_bcpr_previous)) * bpr_power_scale_bcpr_previous)) /\ exists bpr_quotient_bcpr_previous_repeat_entry. bpr_power_code_bcpr_previous = bpr_quotient_bcpr_previous_repeat_entry * S ((S (bpr_power_index_bcpr_previous)) * bpr_power_scale_bcpr_previous) + (q)))) /\ (exists ff_u_bcpr_previous_product ff_v_bcpr_previous_product. ((((exists ff_h_bcpr_previous_product_start. ff_h_bcpr_previous_product_start + S (1) = S ((S (0)) * ff_v_bcpr_previous_product)) /\ exists ff_q_bcpr_previous_product_start. ff_u_bcpr_previous_product = ff_q_bcpr_previous_product_start * S ((S (0)) * ff_v_bcpr_previous_product) + (1))) /\ ((((exists ff_h_bcpr_previous_product_terminal. ff_h_bcpr_previous_product_terminal + S (r) = S ((S (e)) * ff_v_bcpr_previous_product)) /\ exists ff_q_bcpr_previous_product_terminal. ff_u_bcpr_previous_product = ff_q_bcpr_previous_product_terminal * S ((S (e)) * ff_v_bcpr_previous_product) + (r))) /\ forall ff_i_bcpr_previous_product. (exists ff_lt_bcpr_previous_product_bound. ff_lt_bcpr_previous_product_bound + S ff_i_bcpr_previous_product = e) -> exists ff_p_bcpr_previous_product ff_r_bcpr_previous_product ff_s_bcpr_previous_product. ((((exists ff_h_bcpr_previous_product_factor. ff_h_bcpr_previous_product_factor + S (ff_p_bcpr_previous_product) = S ((S (ff_i_bcpr_previous_product)) * bpr_power_scale_bcpr_previous)) /\ exists ff_q_bcpr_previous_product_factor. bpr_power_code_bcpr_previous = ff_q_bcpr_previous_product_factor * S ((S (ff_i_bcpr_previous_product)) * bpr_power_scale_bcpr_previous) + (ff_p_bcpr_previous_product))) /\ ((((exists ff_h_bcpr_previous_product_partial. ff_h_bcpr_previous_product_partial + S (ff_r_bcpr_previous_product) = S ((S (ff_i_bcpr_previous_product)) * ff_v_bcpr_previous_product)) /\ exists ff_q_bcpr_previous_product_partial. ff_u_bcpr_previous_product = ff_q_bcpr_previous_product_partial * S ((S (ff_i_bcpr_previous_product)) * ff_v_bcpr_previous_product) + (ff_r_bcpr_previous_product))) /\ ((((exists ff_h_bcpr_previous_product_successor. ff_h_bcpr_previous_product_successor + S (ff_s_bcpr_previous_product) = S ((S (S ff_i_bcpr_previous_product)) * ff_v_bcpr_previous_product)) /\ exists ff_q_bcpr_previous_product_successor. ff_u_bcpr_previous_product = ff_q_bcpr_previous_product_successor * S ((S (S ff_i_bcpr_previous_product)) * ff_v_bcpr_previous_product) + (ff_s_bcpr_previous_product))) /\ ff_s_bcpr_previous_product = ff_r_bcpr_previous_product * ff_p_bcpr_previous_product)))))))) /\ z = r * q
  21. 0021specialize pow_successor_decompose q
  22. 0022specialize pow_successor_decompose e
  23. 0023specialize pow_successor_decompose (S e)
  24. 0024specialize pow_successor_decompose z
  25. 0025apply pow_successor_decompose
  26. 0026refl
  27. 0027exact hpower
  28. 0028cases hdecomposition
  29. 0029cases hdecomposition_witness
  30. 0030have hprefix : forall d. (exists a. p = d * a) -> (exists b. x = d * b) -> d = 1
  31. 0031specialize IH x
  32. 0032apply IH
  33. 0033exact hcoprime
  34. 0034exact hdecomposition_witness_left
  35. 0035rewrite hdecomposition_witness_right
  36. 0036apply coprime_mul_right
  37. 0037exact hprefix
  38. 0038exact hcoprime