BT00XJ

pow_le_pow_of_exponent_le

Alpha body-checked · checked-use disabled

Relational powers are monotone in the exponent above base one.

Exact expanded PA statement

forall p e f x y. (exists bcf_le_gap_bppem_base. bcf_le_gap_bppem_base + (1) = p) -> (exists bcf_le_gap_bppem_exponent. bcf_le_gap_bppem_exponent + (e) = f) -> (exists ff_b_bppem_left_power ff_c_bppem_left_power. ((forall ff_i_bppem_left_power_repeat. (exists ff_lt_bppem_left_power_repeat_bound. ff_lt_bppem_left_power_repeat_bound + S ff_i_bppem_left_power_repeat = e) -> (((exists ff_h_bppem_left_power_repeat_decoded. ff_h_bppem_left_power_repeat_decoded + S (p) = S ((S (ff_i_bppem_left_power_repeat)) * ff_c_bppem_left_power)) /\ exists ff_q_bppem_left_power_repeat_decoded. ff_b_bppem_left_power = ff_q_bppem_left_power_repeat_decoded * S ((S (ff_i_bppem_left_power_repeat)) * ff_c_bppem_left_power) + (p)))) /\ (exists ff_u_bppem_left_power_product ff_v_bppem_left_power_product. ((((exists ff_h_bppem_left_power_product_start. ff_h_bppem_left_power_product_start + S (1) = S ((S (0)) * ff_v_bppem_left_power_product)) /\ exists ff_q_bppem_left_power_product_start. ff_u_bppem_left_power_product = ff_q_bppem_left_power_product_start * S ((S (0)) * ff_v_bppem_left_power_product) + (1))) /\ ((((exists ff_h_bppem_left_power_product_terminal. ff_h_bppem_left_power_product_terminal + S (x) = S ((S (e)) * ff_v_bppem_left_power_product)) /\ exists ff_q_bppem_left_power_product_terminal. ff_u_bppem_left_power_product = ff_q_bppem_left_power_product_terminal * S ((S (e)) * ff_v_bppem_left_power_product) + (x))) /\ forall ff_i_bppem_left_power_product. (exists ff_lt_bppem_left_power_product_bound. ff_lt_bppem_left_power_product_bound + S ff_i_bppem_left_power_product = e) -> exists ff_p_bppem_left_power_product ff_r_bppem_left_power_product ff_s_bppem_left_power_product. ((((exists ff_h_bppem_left_power_product_factor. ff_h_bppem_left_power_product_factor + S (ff_p_bppem_left_power_product) = S ((S (ff_i_bppem_left_power_product)) * ff_c_bppem_left_power)) /\ exists ff_q_bppem_left_power_product_factor. ff_b_bppem_left_power = ff_q_bppem_left_power_product_factor * S ((S (ff_i_bppem_left_power_product)) * ff_c_bppem_left_power) + (ff_p_bppem_left_power_product))) /\ ((((exists ff_h_bppem_left_power_product_partial. ff_h_bppem_left_power_product_partial + S (ff_r_bppem_left_power_product) = S ((S (ff_i_bppem_left_power_product)) * ff_v_bppem_left_power_product)) /\ exists ff_q_bppem_left_power_product_partial. ff_u_bppem_left_power_product = ff_q_bppem_left_power_product_partial * S ((S (ff_i_bppem_left_power_product)) * ff_v_bppem_left_power_product) + (ff_r_bppem_left_power_product))) /\ ((((exists ff_h_bppem_left_power_product_successor. ff_h_bppem_left_power_product_successor + S (ff_s_bppem_left_power_product) = S ((S (S ff_i_bppem_left_power_product)) * ff_v_bppem_left_power_product)) /\ exists ff_q_bppem_left_power_product_successor. ff_u_bppem_left_power_product = ff_q_bppem_left_power_product_successor * S ((S (S ff_i_bppem_left_power_product)) * ff_v_bppem_left_power_product) + (ff_s_bppem_left_power_product))) /\ ff_s_bppem_left_power_product = ff_r_bppem_left_power_product * ff_p_bppem_left_power_product)))))))) -> (exists ff_b_bppem_right_power ff_c_bppem_right_power. ((forall ff_i_bppem_right_power_repeat. (exists ff_lt_bppem_right_power_repeat_bound. ff_lt_bppem_right_power_repeat_bound + S ff_i_bppem_right_power_repeat = f) -> (((exists ff_h_bppem_right_power_repeat_decoded. ff_h_bppem_right_power_repeat_decoded + S (p) = S ((S (ff_i_bppem_right_power_repeat)) * ff_c_bppem_right_power)) /\ exists ff_q_bppem_right_power_repeat_decoded. ff_b_bppem_right_power = ff_q_bppem_right_power_repeat_decoded * S ((S (ff_i_bppem_right_power_repeat)) * ff_c_bppem_right_power) + (p)))) /\ (exists ff_u_bppem_right_power_product ff_v_bppem_right_power_product. ((((exists ff_h_bppem_right_power_product_start. ff_h_bppem_right_power_product_start + S (1) = S ((S (0)) * ff_v_bppem_right_power_product)) /\ exists ff_q_bppem_right_power_product_start. ff_u_bppem_right_power_product = ff_q_bppem_right_power_product_start * S ((S (0)) * ff_v_bppem_right_power_product) + (1))) /\ ((((exists ff_h_bppem_right_power_product_terminal. ff_h_bppem_right_power_product_terminal + S (y) = S ((S (f)) * ff_v_bppem_right_power_product)) /\ exists ff_q_bppem_right_power_product_terminal. ff_u_bppem_right_power_product = ff_q_bppem_right_power_product_terminal * S ((S (f)) * ff_v_bppem_right_power_product) + (y))) /\ forall ff_i_bppem_right_power_product. (exists ff_lt_bppem_right_power_product_bound. ff_lt_bppem_right_power_product_bound + S ff_i_bppem_right_power_product = f) -> exists ff_p_bppem_right_power_product ff_r_bppem_right_power_product ff_s_bppem_right_power_product. ((((exists ff_h_bppem_right_power_product_factor. ff_h_bppem_right_power_product_factor + S (ff_p_bppem_right_power_product) = S ((S (ff_i_bppem_right_power_product)) * ff_c_bppem_right_power)) /\ exists ff_q_bppem_right_power_product_factor. ff_b_bppem_right_power = ff_q_bppem_right_power_product_factor * S ((S (ff_i_bppem_right_power_product)) * ff_c_bppem_right_power) + (ff_p_bppem_right_power_product))) /\ ((((exists ff_h_bppem_right_power_product_partial. ff_h_bppem_right_power_product_partial + S (ff_r_bppem_right_power_product) = S ((S (ff_i_bppem_right_power_product)) * ff_v_bppem_right_power_product)) /\ exists ff_q_bppem_right_power_product_partial. ff_u_bppem_right_power_product = ff_q_bppem_right_power_product_partial * S ((S (ff_i_bppem_right_power_product)) * ff_v_bppem_right_power_product) + (ff_r_bppem_right_power_product))) /\ ((((exists ff_h_bppem_right_power_product_successor. ff_h_bppem_right_power_product_successor + S (ff_s_bppem_right_power_product) = S ((S (S ff_i_bppem_right_power_product)) * ff_v_bppem_right_power_product)) /\ exists ff_q_bppem_right_power_product_successor. ff_u_bppem_right_power_product = ff_q_bppem_right_power_product_successor * S ((S (S ff_i_bppem_right_power_product)) * ff_v_bppem_right_power_product) + (ff_s_bppem_right_power_product))) /\ ff_s_bppem_right_power_product = ff_r_bppem_right_power_product * ff_p_bppem_right_power_product)))))))) -> (exists bcf_le_gap_bppem_result. bcf_le_gap_bppem_result + (x) = y)

Structural proof guide

Relational powers are monotone in the exponent above base one.

Direct prerequisites: pow_exists, add_comm, pow_add, one_le_pow, le_mul_of_one_le_right. The authored body proceeds by case analysis (2), intermediate claims (5), equality transport (1).

Proof neighborhood

Direct dependencies

BT0080 pow_exists BT0002 add_comm BT009X pow_add BT00Q0 one_le_pow BT00PW le_mul_of_one_le_right

Direct dependents

BT00XK pow_tail_strict_of_square BT00Y5 central_binom_prime_power_contribution_le_double

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 x
  5. 0005intro y
  6. 0006intro hbase
  7. 0007intro hexponent
  8. 0008intro hx
  9. 0009intro hy
  10. 0010cases hexponent
  11. 0011have hgap_power : exists z. (exists ff_b_bppem_gap_power ff_c_bppem_gap_power. ((forall ff_i_bppem_gap_power_repeat. (exists ff_lt_bppem_gap_power_repeat_bound. ff_lt_bppem_gap_power_repeat_bound + S ff_i_bppem_gap_power_repeat = x1) -> (((exists ff_h_bppem_gap_power_repeat_decoded. ff_h_bppem_gap_power_repeat_decoded + S (p) = S ((S (ff_i_bppem_gap_power_repeat)) * ff_c_bppem_gap_power)) /\ exists ff_q_bppem_gap_power_repeat_decoded. ff_b_bppem_gap_power = ff_q_bppem_gap_power_repeat_decoded * S ((S (ff_i_bppem_gap_power_repeat)) * ff_c_bppem_gap_power) + (p)))) /\ (exists ff_u_bppem_gap_power_product ff_v_bppem_gap_power_product. ((((exists ff_h_bppem_gap_power_product_start. ff_h_bppem_gap_power_product_start + S (1) = S ((S (0)) * ff_v_bppem_gap_power_product)) /\ exists ff_q_bppem_gap_power_product_start. ff_u_bppem_gap_power_product = ff_q_bppem_gap_power_product_start * S ((S (0)) * ff_v_bppem_gap_power_product) + (1))) /\ ((((exists ff_h_bppem_gap_power_product_terminal. ff_h_bppem_gap_power_product_terminal + S (z) = S ((S (x1)) * ff_v_bppem_gap_power_product)) /\ exists ff_q_bppem_gap_power_product_terminal. ff_u_bppem_gap_power_product = ff_q_bppem_gap_power_product_terminal * S ((S (x1)) * ff_v_bppem_gap_power_product) + (z))) /\ forall ff_i_bppem_gap_power_product. (exists ff_lt_bppem_gap_power_product_bound. ff_lt_bppem_gap_power_product_bound + S ff_i_bppem_gap_power_product = x1) -> exists ff_p_bppem_gap_power_product ff_r_bppem_gap_power_product ff_s_bppem_gap_power_product. ((((exists ff_h_bppem_gap_power_product_factor. ff_h_bppem_gap_power_product_factor + S (ff_p_bppem_gap_power_product) = S ((S (ff_i_bppem_gap_power_product)) * ff_c_bppem_gap_power)) /\ exists ff_q_bppem_gap_power_product_factor. ff_b_bppem_gap_power = ff_q_bppem_gap_power_product_factor * S ((S (ff_i_bppem_gap_power_product)) * ff_c_bppem_gap_power) + (ff_p_bppem_gap_power_product))) /\ ((((exists ff_h_bppem_gap_power_product_partial. ff_h_bppem_gap_power_product_partial + S (ff_r_bppem_gap_power_product) = S ((S (ff_i_bppem_gap_power_product)) * ff_v_bppem_gap_power_product)) /\ exists ff_q_bppem_gap_power_product_partial. ff_u_bppem_gap_power_product = ff_q_bppem_gap_power_product_partial * S ((S (ff_i_bppem_gap_power_product)) * ff_v_bppem_gap_power_product) + (ff_r_bppem_gap_power_product))) /\ ((((exists ff_h_bppem_gap_power_product_successor. ff_h_bppem_gap_power_product_successor + S (ff_s_bppem_gap_power_product) = S ((S (S ff_i_bppem_gap_power_product)) * ff_v_bppem_gap_power_product)) /\ exists ff_q_bppem_gap_power_product_successor. ff_u_bppem_gap_power_product = ff_q_bppem_gap_power_product_successor * S ((S (S ff_i_bppem_gap_power_product)) * ff_v_bppem_gap_power_product) + (ff_s_bppem_gap_power_product))) /\ ff_s_bppem_gap_power_product = ff_r_bppem_gap_power_product * ff_p_bppem_gap_power_product))))))))
  12. 0012specialize pow_exists p
  13. 0013specialize pow_exists x1
  14. 0014exact pow_exists
  15. 0015cases hgap_power
  16. 0016have hsum : f = e + x1
  17. 0017trans x1 + e
  18. 0018symm
  19. 0019exact hexponent_witness
  20. 0020apply add_comm
  21. 0021have hfactor : y = x * x2
  22. 0022specialize pow_add p
  23. 0023specialize pow_add e
  24. 0024specialize pow_add x1
  25. 0025specialize pow_add f
  26. 0026specialize pow_add x
  27. 0027specialize pow_add x2
  28. 0028specialize pow_add y
  29. 0029apply pow_add
  30. 0030exact hsum
  31. 0031exact hx
  32. 0032exact hgap_power_witness
  33. 0033exact hy
  34. 0034have hgap_order : exists bcf_le_gap_bppem_gap_power_order. bcf_le_gap_bppem_gap_power_order + (1) = x2
  35. 0035specialize one_le_pow p
  36. 0036specialize one_le_pow x1
  37. 0037specialize one_le_pow x2
  38. 0038apply one_le_pow
  39. 0039exact hbase
  40. 0040exact hgap_power_witness
  41. 0041have hproduct_order : exists bcf_le_gap_bppem_product_order. bcf_le_gap_bppem_product_order + (x) = x * x2
  42. 0042specialize le_mul_of_one_le_right x
  43. 0043specialize le_mul_of_one_le_right x2
  44. 0044apply le_mul_of_one_le_right
  45. 0045exact hgap_order
  46. 0046rewrite hfactor
  47. 0047exact hproduct_order