BT00QK

power_divides_exponent_antitone

Alpha body-checked · checked-use disabled

Divisibility by a higher relational power entails every lower exponent.

Exact expanded PA statement

forall p e f a. (exists bpd_gap_antitone_exponents. bpd_gap_antitone_exponents + (e) = (f)) -> (exists bpv_result_antitone_high. ((exists ff_b_antitone_high_power ff_c_antitone_high_power. ((forall ff_i_antitone_high_power_repeat. (exists ff_lt_antitone_high_power_repeat_bound. ff_lt_antitone_high_power_repeat_bound + S ff_i_antitone_high_power_repeat = f) -> (((exists ff_h_antitone_high_power_repeat_decoded. ff_h_antitone_high_power_repeat_decoded + S (p) = S ((S (ff_i_antitone_high_power_repeat)) * ff_c_antitone_high_power)) /\ exists ff_q_antitone_high_power_repeat_decoded. ff_b_antitone_high_power = ff_q_antitone_high_power_repeat_decoded * S ((S (ff_i_antitone_high_power_repeat)) * ff_c_antitone_high_power) + (p)))) /\ (exists ff_u_antitone_high_power_product ff_v_antitone_high_power_product. ((((exists ff_h_antitone_high_power_product_start. ff_h_antitone_high_power_product_start + S (1) = S ((S (0)) * ff_v_antitone_high_power_product)) /\ exists ff_q_antitone_high_power_product_start. ff_u_antitone_high_power_product = ff_q_antitone_high_power_product_start * S ((S (0)) * ff_v_antitone_high_power_product) + (1))) /\ ((((exists ff_h_antitone_high_power_product_terminal. ff_h_antitone_high_power_product_terminal + S (bpv_result_antitone_high) = S ((S (f)) * ff_v_antitone_high_power_product)) /\ exists ff_q_antitone_high_power_product_terminal. ff_u_antitone_high_power_product = ff_q_antitone_high_power_product_terminal * S ((S (f)) * ff_v_antitone_high_power_product) + (bpv_result_antitone_high))) /\ forall ff_i_antitone_high_power_product. (exists ff_lt_antitone_high_power_product_bound. ff_lt_antitone_high_power_product_bound + S ff_i_antitone_high_power_product = f) -> exists ff_p_antitone_high_power_product ff_r_antitone_high_power_product ff_s_antitone_high_power_product. ((((exists ff_h_antitone_high_power_product_factor. ff_h_antitone_high_power_product_factor + S (ff_p_antitone_high_power_product) = S ((S (ff_i_antitone_high_power_product)) * ff_c_antitone_high_power)) /\ exists ff_q_antitone_high_power_product_factor. ff_b_antitone_high_power = ff_q_antitone_high_power_product_factor * S ((S (ff_i_antitone_high_power_product)) * ff_c_antitone_high_power) + (ff_p_antitone_high_power_product))) /\ ((((exists ff_h_antitone_high_power_product_partial. ff_h_antitone_high_power_product_partial + S (ff_r_antitone_high_power_product) = S ((S (ff_i_antitone_high_power_product)) * ff_v_antitone_high_power_product)) /\ exists ff_q_antitone_high_power_product_partial. ff_u_antitone_high_power_product = ff_q_antitone_high_power_product_partial * S ((S (ff_i_antitone_high_power_product)) * ff_v_antitone_high_power_product) + (ff_r_antitone_high_power_product))) /\ ((((exists ff_h_antitone_high_power_product_successor. ff_h_antitone_high_power_product_successor + S (ff_s_antitone_high_power_product) = S ((S (S ff_i_antitone_high_power_product)) * ff_v_antitone_high_power_product)) /\ exists ff_q_antitone_high_power_product_successor. ff_u_antitone_high_power_product = ff_q_antitone_high_power_product_successor * S ((S (S ff_i_antitone_high_power_product)) * ff_v_antitone_high_power_product) + (ff_s_antitone_high_power_product))) /\ ff_s_antitone_high_power_product = ff_r_antitone_high_power_product * ff_p_antitone_high_power_product)))))))) /\ (exists bpv_factor_antitone_high_divides. a = bpv_result_antitone_high * bpv_factor_antitone_high_divides))) -> (exists bpv_result_antitone_low. ((exists ff_b_antitone_low_power ff_c_antitone_low_power. ((forall ff_i_antitone_low_power_repeat. (exists ff_lt_antitone_low_power_repeat_bound. ff_lt_antitone_low_power_repeat_bound + S ff_i_antitone_low_power_repeat = e) -> (((exists ff_h_antitone_low_power_repeat_decoded. ff_h_antitone_low_power_repeat_decoded + S (p) = S ((S (ff_i_antitone_low_power_repeat)) * ff_c_antitone_low_power)) /\ exists ff_q_antitone_low_power_repeat_decoded. ff_b_antitone_low_power = ff_q_antitone_low_power_repeat_decoded * S ((S (ff_i_antitone_low_power_repeat)) * ff_c_antitone_low_power) + (p)))) /\ (exists ff_u_antitone_low_power_product ff_v_antitone_low_power_product. ((((exists ff_h_antitone_low_power_product_start. ff_h_antitone_low_power_product_start + S (1) = S ((S (0)) * ff_v_antitone_low_power_product)) /\ exists ff_q_antitone_low_power_product_start. ff_u_antitone_low_power_product = ff_q_antitone_low_power_product_start * S ((S (0)) * ff_v_antitone_low_power_product) + (1))) /\ ((((exists ff_h_antitone_low_power_product_terminal. ff_h_antitone_low_power_product_terminal + S (bpv_result_antitone_low) = S ((S (e)) * ff_v_antitone_low_power_product)) /\ exists ff_q_antitone_low_power_product_terminal. ff_u_antitone_low_power_product = ff_q_antitone_low_power_product_terminal * S ((S (e)) * ff_v_antitone_low_power_product) + (bpv_result_antitone_low))) /\ forall ff_i_antitone_low_power_product. (exists ff_lt_antitone_low_power_product_bound. ff_lt_antitone_low_power_product_bound + S ff_i_antitone_low_power_product = e) -> exists ff_p_antitone_low_power_product ff_r_antitone_low_power_product ff_s_antitone_low_power_product. ((((exists ff_h_antitone_low_power_product_factor. ff_h_antitone_low_power_product_factor + S (ff_p_antitone_low_power_product) = S ((S (ff_i_antitone_low_power_product)) * ff_c_antitone_low_power)) /\ exists ff_q_antitone_low_power_product_factor. ff_b_antitone_low_power = ff_q_antitone_low_power_product_factor * S ((S (ff_i_antitone_low_power_product)) * ff_c_antitone_low_power) + (ff_p_antitone_low_power_product))) /\ ((((exists ff_h_antitone_low_power_product_partial. ff_h_antitone_low_power_product_partial + S (ff_r_antitone_low_power_product) = S ((S (ff_i_antitone_low_power_product)) * ff_v_antitone_low_power_product)) /\ exists ff_q_antitone_low_power_product_partial. ff_u_antitone_low_power_product = ff_q_antitone_low_power_product_partial * S ((S (ff_i_antitone_low_power_product)) * ff_v_antitone_low_power_product) + (ff_r_antitone_low_power_product))) /\ ((((exists ff_h_antitone_low_power_product_successor. ff_h_antitone_low_power_product_successor + S (ff_s_antitone_low_power_product) = S ((S (S ff_i_antitone_low_power_product)) * ff_v_antitone_low_power_product)) /\ exists ff_q_antitone_low_power_product_successor. ff_u_antitone_low_power_product = ff_q_antitone_low_power_product_successor * S ((S (S ff_i_antitone_low_power_product)) * ff_v_antitone_low_power_product) + (ff_s_antitone_low_power_product))) /\ ff_s_antitone_low_power_product = ff_r_antitone_low_power_product * ff_p_antitone_low_power_product)))))))) /\ (exists bpv_factor_antitone_low_divides. a = bpv_result_antitone_low * bpv_factor_antitone_low_divides)))

Structural proof guide

Divisibility by a higher relational power entails every lower exponent.

Direct prerequisites: pow_exists, pow_add, add_comm, mul_assoc. The authored body proceeds by case analysis (6), intermediate claims (4).

Proof neighborhood

Direct dependencies

BT0080 pow_exists BT009X pow_add BT0002 add_comm BT0008 mul_assoc

Direct dependents

BT00QS power_valuation_mul_upper BT00SC power_divides_of_exponent_le_valuation BT00W0 power_valuation_nonzero_exponent_divides_base

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 e
  3. 0003intro f
  4. 0004intro a
  5. 0005intro hef
  6. 0006intro hhigh
  7. 0007cases hef
  8. 0008cases hhigh
  9. 0009cases hhigh_witness
  10. 0010cases hhigh_witness_right
  11. 0011have hsum : f = e + x
  12. 0012trans x + e
  13. 0013symm
  14. 0014exact hef_witness
  15. 0015specialize add_comm x
  16. 0016specialize add_comm e
  17. 0017exact add_comm
  18. 0018have hlow_power : exists r. (exists ff_b_bpd_antitone_low_witness ff_c_bpd_antitone_low_witness. ((forall ff_i_bpd_antitone_low_witness_repeat. (exists ff_lt_bpd_antitone_low_witness_repeat_bound. ff_lt_bpd_antitone_low_witness_repeat_bound + S ff_i_bpd_antitone_low_witness_repeat = e) -> (((exists ff_h_bpd_antitone_low_witness_repeat_decoded. ff_h_bpd_antitone_low_witness_repeat_decoded + S (p) = S ((S (ff_i_bpd_antitone_low_witness_repeat)) * ff_c_bpd_antitone_low_witness)) /\ exists ff_q_bpd_antitone_low_witness_repeat_decoded. ff_b_bpd_antitone_low_witness = ff_q_bpd_antitone_low_witness_repeat_decoded * S ((S (ff_i_bpd_antitone_low_witness_repeat)) * ff_c_bpd_antitone_low_witness) + (p)))) /\ (exists ff_u_bpd_antitone_low_witness_product ff_v_bpd_antitone_low_witness_product. ((((exists ff_h_bpd_antitone_low_witness_product_start. ff_h_bpd_antitone_low_witness_product_start + S (1) = S ((S (0)) * ff_v_bpd_antitone_low_witness_product)) /\ exists ff_q_bpd_antitone_low_witness_product_start. ff_u_bpd_antitone_low_witness_product = ff_q_bpd_antitone_low_witness_product_start * S ((S (0)) * ff_v_bpd_antitone_low_witness_product) + (1))) /\ ((((exists ff_h_bpd_antitone_low_witness_product_terminal. ff_h_bpd_antitone_low_witness_product_terminal + S (r) = S ((S (e)) * ff_v_bpd_antitone_low_witness_product)) /\ exists ff_q_bpd_antitone_low_witness_product_terminal. ff_u_bpd_antitone_low_witness_product = ff_q_bpd_antitone_low_witness_product_terminal * S ((S (e)) * ff_v_bpd_antitone_low_witness_product) + (r))) /\ forall ff_i_bpd_antitone_low_witness_product. (exists ff_lt_bpd_antitone_low_witness_product_bound. ff_lt_bpd_antitone_low_witness_product_bound + S ff_i_bpd_antitone_low_witness_product = e) -> exists ff_p_bpd_antitone_low_witness_product ff_r_bpd_antitone_low_witness_product ff_s_bpd_antitone_low_witness_product. ((((exists ff_h_bpd_antitone_low_witness_product_factor. ff_h_bpd_antitone_low_witness_product_factor + S (ff_p_bpd_antitone_low_witness_product) = S ((S (ff_i_bpd_antitone_low_witness_product)) * ff_c_bpd_antitone_low_witness)) /\ exists ff_q_bpd_antitone_low_witness_product_factor. ff_b_bpd_antitone_low_witness = ff_q_bpd_antitone_low_witness_product_factor * S ((S (ff_i_bpd_antitone_low_witness_product)) * ff_c_bpd_antitone_low_witness) + (ff_p_bpd_antitone_low_witness_product))) /\ ((((exists ff_h_bpd_antitone_low_witness_product_partial. ff_h_bpd_antitone_low_witness_product_partial + S (ff_r_bpd_antitone_low_witness_product) = S ((S (ff_i_bpd_antitone_low_witness_product)) * ff_v_bpd_antitone_low_witness_product)) /\ exists ff_q_bpd_antitone_low_witness_product_partial. ff_u_bpd_antitone_low_witness_product = ff_q_bpd_antitone_low_witness_product_partial * S ((S (ff_i_bpd_antitone_low_witness_product)) * ff_v_bpd_antitone_low_witness_product) + (ff_r_bpd_antitone_low_witness_product))) /\ ((((exists ff_h_bpd_antitone_low_witness_product_successor. ff_h_bpd_antitone_low_witness_product_successor + S (ff_s_bpd_antitone_low_witness_product) = S ((S (S ff_i_bpd_antitone_low_witness_product)) * ff_v_bpd_antitone_low_witness_product)) /\ exists ff_q_bpd_antitone_low_witness_product_successor. ff_u_bpd_antitone_low_witness_product = ff_q_bpd_antitone_low_witness_product_successor * S ((S (S ff_i_bpd_antitone_low_witness_product)) * ff_v_bpd_antitone_low_witness_product) + (ff_s_bpd_antitone_low_witness_product))) /\ ff_s_bpd_antitone_low_witness_product = ff_r_bpd_antitone_low_witness_product * ff_p_bpd_antitone_low_witness_product))))))))
  19. 0019specialize pow_exists p
  20. 0020specialize pow_exists e
  21. 0021exact pow_exists
  22. 0022cases hlow_power
  23. 0023have hgap_power : exists r. (exists bpvi_b_bpd_antitone_gap_witness bpvi_c_bpd_antitone_gap_witness. ((forall bpvi_i_bpd_antitone_gap_witness. (exists bpvi_repeat_gap_bpd_antitone_gap_witness. bpvi_repeat_gap_bpd_antitone_gap_witness + S bpvi_i_bpd_antitone_gap_witness = x) -> (((exists bpvi_h_bpd_antitone_gap_witness_repeat. bpvi_h_bpd_antitone_gap_witness_repeat + S (p) = S ((S (bpvi_i_bpd_antitone_gap_witness)) * bpvi_c_bpd_antitone_gap_witness)) /\ exists bpvi_q_bpd_antitone_gap_witness_repeat. bpvi_b_bpd_antitone_gap_witness = bpvi_q_bpd_antitone_gap_witness_repeat * S ((S (bpvi_i_bpd_antitone_gap_witness)) * bpvi_c_bpd_antitone_gap_witness) + (p)))) /\ (exists bpvi_u_bpd_antitone_gap_witness bpvi_v_bpd_antitone_gap_witness. ((((exists bpvi_h_bpd_antitone_gap_witness_start. bpvi_h_bpd_antitone_gap_witness_start + S (1) = S ((S (0)) * bpvi_v_bpd_antitone_gap_witness)) /\ exists bpvi_q_bpd_antitone_gap_witness_start. bpvi_u_bpd_antitone_gap_witness = bpvi_q_bpd_antitone_gap_witness_start * S ((S (0)) * bpvi_v_bpd_antitone_gap_witness) + (1))) /\ ((((exists bpvi_h_bpd_antitone_gap_witness_terminal. bpvi_h_bpd_antitone_gap_witness_terminal + S (r) = S ((S (x)) * bpvi_v_bpd_antitone_gap_witness)) /\ exists bpvi_q_bpd_antitone_gap_witness_terminal. bpvi_u_bpd_antitone_gap_witness = bpvi_q_bpd_antitone_gap_witness_terminal * S ((S (x)) * bpvi_v_bpd_antitone_gap_witness) + (r))) /\ forall bpvi_j_bpd_antitone_gap_witness. (exists bpvi_product_gap_bpd_antitone_gap_witness. bpvi_product_gap_bpd_antitone_gap_witness + S bpvi_j_bpd_antitone_gap_witness = x) -> exists bpvi_factor_bpd_antitone_gap_witness bpvi_partial_bpd_antitone_gap_witness bpvi_successor_bpd_antitone_gap_witness. ((((exists bpvi_h_bpd_antitone_gap_witness_factor. bpvi_h_bpd_antitone_gap_witness_factor + S (bpvi_factor_bpd_antitone_gap_witness) = S ((S (bpvi_j_bpd_antitone_gap_witness)) * bpvi_c_bpd_antitone_gap_witness)) /\ exists bpvi_q_bpd_antitone_gap_witness_factor. bpvi_b_bpd_antitone_gap_witness = bpvi_q_bpd_antitone_gap_witness_factor * S ((S (bpvi_j_bpd_antitone_gap_witness)) * bpvi_c_bpd_antitone_gap_witness) + (bpvi_factor_bpd_antitone_gap_witness))) /\ ((((exists bpvi_h_bpd_antitone_gap_witness_partial. bpvi_h_bpd_antitone_gap_witness_partial + S (bpvi_partial_bpd_antitone_gap_witness) = S ((S (bpvi_j_bpd_antitone_gap_witness)) * bpvi_v_bpd_antitone_gap_witness)) /\ exists bpvi_q_bpd_antitone_gap_witness_partial. bpvi_u_bpd_antitone_gap_witness = bpvi_q_bpd_antitone_gap_witness_partial * S ((S (bpvi_j_bpd_antitone_gap_witness)) * bpvi_v_bpd_antitone_gap_witness) + (bpvi_partial_bpd_antitone_gap_witness))) /\ ((((exists bpvi_h_bpd_antitone_gap_witness_successor. bpvi_h_bpd_antitone_gap_witness_successor + S (bpvi_successor_bpd_antitone_gap_witness) = S ((S (S bpvi_j_bpd_antitone_gap_witness)) * bpvi_v_bpd_antitone_gap_witness)) /\ exists bpvi_q_bpd_antitone_gap_witness_successor. bpvi_u_bpd_antitone_gap_witness = bpvi_q_bpd_antitone_gap_witness_successor * S ((S (S bpvi_j_bpd_antitone_gap_witness)) * bpvi_v_bpd_antitone_gap_witness) + (bpvi_successor_bpd_antitone_gap_witness))) /\ bpvi_successor_bpd_antitone_gap_witness = bpvi_partial_bpd_antitone_gap_witness * bpvi_factor_bpd_antitone_gap_witness))))))))
  24. 0024specialize pow_exists p
  25. 0025specialize pow_exists x
  26. 0026exact pow_exists
  27. 0027cases hgap_power
  28. 0028have hfactor : x1 = x3 * x4
  29. 0029specialize pow_add p
  30. 0030specialize pow_add e
  31. 0031specialize pow_add x
  32. 0032specialize pow_add f
  33. 0033specialize pow_add x3
  34. 0034specialize pow_add x4
  35. 0035specialize pow_add x1
  36. 0036apply pow_add
  37. 0037exact hsum
  38. 0038exact hlow_power_witness
  39. 0039exact hgap_power_witness
  40. 0040exact hhigh_witness_left
  41. 0041exists x3
  42. 0042split
  43. 0043exact hlow_power_witness
  44. 0044exists x4 * x2
  45. 0045trans x1 * x2
  46. 0046exact hhigh_witness_right_witness
  47. 0047trans (x3 * x4) * x2
  48. 0048congr
  49. 0049exact hfactor
  50. 0050refl
  51. 0051apply mul_assoc