BT00PY

pow_base_monotone

Alpha body-checked · checked-use disabled

Relational powers are monotone in the base at every exponent.

Exact expanded PA statement

forall a b e x y. (exists bpo_gap_pow_base. bpo_gap_pow_base + (a) = (b)) -> (exists ff_b_bpo_left ff_c_bpo_left. ((forall ff_i_bpo_left_repeat. (exists ff_lt_bpo_left_repeat_bound. ff_lt_bpo_left_repeat_bound + S ff_i_bpo_left_repeat = e) -> (((exists ff_h_bpo_left_repeat_decoded. ff_h_bpo_left_repeat_decoded + S (a) = S ((S (ff_i_bpo_left_repeat)) * ff_c_bpo_left)) /\ exists ff_q_bpo_left_repeat_decoded. ff_b_bpo_left = ff_q_bpo_left_repeat_decoded * S ((S (ff_i_bpo_left_repeat)) * ff_c_bpo_left) + (a)))) /\ (exists ff_u_bpo_left_product ff_v_bpo_left_product. ((((exists ff_h_bpo_left_product_start. ff_h_bpo_left_product_start + S (1) = S ((S (0)) * ff_v_bpo_left_product)) /\ exists ff_q_bpo_left_product_start. ff_u_bpo_left_product = ff_q_bpo_left_product_start * S ((S (0)) * ff_v_bpo_left_product) + (1))) /\ ((((exists ff_h_bpo_left_product_terminal. ff_h_bpo_left_product_terminal + S (x) = S ((S (e)) * ff_v_bpo_left_product)) /\ exists ff_q_bpo_left_product_terminal. ff_u_bpo_left_product = ff_q_bpo_left_product_terminal * S ((S (e)) * ff_v_bpo_left_product) + (x))) /\ forall ff_i_bpo_left_product. (exists ff_lt_bpo_left_product_bound. ff_lt_bpo_left_product_bound + S ff_i_bpo_left_product = e) -> exists ff_p_bpo_left_product ff_r_bpo_left_product ff_s_bpo_left_product. ((((exists ff_h_bpo_left_product_factor. ff_h_bpo_left_product_factor + S (ff_p_bpo_left_product) = S ((S (ff_i_bpo_left_product)) * ff_c_bpo_left)) /\ exists ff_q_bpo_left_product_factor. ff_b_bpo_left = ff_q_bpo_left_product_factor * S ((S (ff_i_bpo_left_product)) * ff_c_bpo_left) + (ff_p_bpo_left_product))) /\ ((((exists ff_h_bpo_left_product_partial. ff_h_bpo_left_product_partial + S (ff_r_bpo_left_product) = S ((S (ff_i_bpo_left_product)) * ff_v_bpo_left_product)) /\ exists ff_q_bpo_left_product_partial. ff_u_bpo_left_product = ff_q_bpo_left_product_partial * S ((S (ff_i_bpo_left_product)) * ff_v_bpo_left_product) + (ff_r_bpo_left_product))) /\ ((((exists ff_h_bpo_left_product_successor. ff_h_bpo_left_product_successor + S (ff_s_bpo_left_product) = S ((S (S ff_i_bpo_left_product)) * ff_v_bpo_left_product)) /\ exists ff_q_bpo_left_product_successor. ff_u_bpo_left_product = ff_q_bpo_left_product_successor * S ((S (S ff_i_bpo_left_product)) * ff_v_bpo_left_product) + (ff_s_bpo_left_product))) /\ ff_s_bpo_left_product = ff_r_bpo_left_product * ff_p_bpo_left_product)))))))) -> (exists ff_b_bpo_right ff_c_bpo_right. ((forall ff_i_bpo_right_repeat. (exists ff_lt_bpo_right_repeat_bound. ff_lt_bpo_right_repeat_bound + S ff_i_bpo_right_repeat = e) -> (((exists ff_h_bpo_right_repeat_decoded. ff_h_bpo_right_repeat_decoded + S (b) = S ((S (ff_i_bpo_right_repeat)) * ff_c_bpo_right)) /\ exists ff_q_bpo_right_repeat_decoded. ff_b_bpo_right = ff_q_bpo_right_repeat_decoded * S ((S (ff_i_bpo_right_repeat)) * ff_c_bpo_right) + (b)))) /\ (exists ff_u_bpo_right_product ff_v_bpo_right_product. ((((exists ff_h_bpo_right_product_start. ff_h_bpo_right_product_start + S (1) = S ((S (0)) * ff_v_bpo_right_product)) /\ exists ff_q_bpo_right_product_start. ff_u_bpo_right_product = ff_q_bpo_right_product_start * S ((S (0)) * ff_v_bpo_right_product) + (1))) /\ ((((exists ff_h_bpo_right_product_terminal. ff_h_bpo_right_product_terminal + S (y) = S ((S (e)) * ff_v_bpo_right_product)) /\ exists ff_q_bpo_right_product_terminal. ff_u_bpo_right_product = ff_q_bpo_right_product_terminal * S ((S (e)) * ff_v_bpo_right_product) + (y))) /\ forall ff_i_bpo_right_product. (exists ff_lt_bpo_right_product_bound. ff_lt_bpo_right_product_bound + S ff_i_bpo_right_product = e) -> exists ff_p_bpo_right_product ff_r_bpo_right_product ff_s_bpo_right_product. ((((exists ff_h_bpo_right_product_factor. ff_h_bpo_right_product_factor + S (ff_p_bpo_right_product) = S ((S (ff_i_bpo_right_product)) * ff_c_bpo_right)) /\ exists ff_q_bpo_right_product_factor. ff_b_bpo_right = ff_q_bpo_right_product_factor * S ((S (ff_i_bpo_right_product)) * ff_c_bpo_right) + (ff_p_bpo_right_product))) /\ ((((exists ff_h_bpo_right_product_partial. ff_h_bpo_right_product_partial + S (ff_r_bpo_right_product) = S ((S (ff_i_bpo_right_product)) * ff_v_bpo_right_product)) /\ exists ff_q_bpo_right_product_partial. ff_u_bpo_right_product = ff_q_bpo_right_product_partial * S ((S (ff_i_bpo_right_product)) * ff_v_bpo_right_product) + (ff_r_bpo_right_product))) /\ ((((exists ff_h_bpo_right_product_successor. ff_h_bpo_right_product_successor + S (ff_s_bpo_right_product) = S ((S (S ff_i_bpo_right_product)) * ff_v_bpo_right_product)) /\ exists ff_q_bpo_right_product_successor. ff_u_bpo_right_product = ff_q_bpo_right_product_successor * S ((S (S ff_i_bpo_right_product)) * ff_v_bpo_right_product) + (ff_s_bpo_right_product))) /\ ff_s_bpo_right_product = ff_r_bpo_right_product * ff_p_bpo_right_product)))))))) -> (exists bpo_gap_pow_result. bpo_gap_pow_result + (x) = (y))

Structural proof guide

Relational powers are monotone in the base at every exponent.

Direct prerequisites: pow_zero, pow_successor_decompose, le_refl, mul_le_mul. The authored body proceeds by structural induction (1), case analysis (4), intermediate claims (5), equality transport (4).

Proof neighborhood

Direct dependencies

BT0081 pow_zero BT0083 pow_successor_decompose BT000E le_refl BT00PV mul_le_mul

Direct dependents

BT00SW bertrand_h_six_step_transport_from_total BT00SX bertrand_j_six_step_transport_from_total BT00W3 pow_block_bound_from_total BT00WF pow_six_six_le_pow_four_eight_from_total BT00WG pow_six_four_le_pow_four_six_from_total BT00WH pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total BT00WJ pow_two_successor_double_le_pow_four_successor_from_total BT00WQ bertrand_h_root_33_from_total BT00WR bertrand_h_root_34_from_total BT00WS bertrand_h_root_35_from_total BT00WT bertrand_h_root_36_from_total BT00WU bertrand_h_root_37_from_total BT00WV bertrand_j_base_thirty_two_window_from_total BT00X4 bertrand_floor_power_product_le_h_from_total

Formal native tactic body

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

  1. 0001intro a
  2. 0002intro b
  3. 0003intro e
  4. 0004induction e
  5. 0005intro x
  6. 0006intro y
  7. 0007intro hab
  8. 0008intro hx
  9. 0009intro hy
  10. 0010have hx1 : x = 1
  11. 0011specialize pow_zero a
  12. 0012specialize pow_zero 0
  13. 0013specialize pow_zero x
  14. 0014apply pow_zero
  15. 0015refl
  16. 0016exact hx
  17. 0017have hy1 : y = 1
  18. 0018specialize pow_zero b
  19. 0019specialize pow_zero 0
  20. 0020specialize pow_zero y
  21. 0021apply pow_zero
  22. 0022refl
  23. 0023exact hy
  24. 0024rewrite hx1
  25. 0025rewrite hy1
  26. 0026specialize le_refl 1
  27. 0027exact le_refl
  28. 0028intro x
  29. 0029intro y
  30. 0030intro hab
  31. 0031intro hx
  32. 0032intro hy
  33. 0033have hxstep : exists r. (exists ff_b_bpo_left_prefix ff_c_bpo_left_prefix. ((forall ff_i_bpo_left_prefix_repeat. (exists ff_lt_bpo_left_prefix_repeat_bound. ff_lt_bpo_left_prefix_repeat_bound + S ff_i_bpo_left_prefix_repeat = e) -> (((exists ff_h_bpo_left_prefix_repeat_decoded. ff_h_bpo_left_prefix_repeat_decoded + S (a) = S ((S (ff_i_bpo_left_prefix_repeat)) * ff_c_bpo_left_prefix)) /\ exists ff_q_bpo_left_prefix_repeat_decoded. ff_b_bpo_left_prefix = ff_q_bpo_left_prefix_repeat_decoded * S ((S (ff_i_bpo_left_prefix_repeat)) * ff_c_bpo_left_prefix) + (a)))) /\ (exists ff_u_bpo_left_prefix_product ff_v_bpo_left_prefix_product. ((((exists ff_h_bpo_left_prefix_product_start. ff_h_bpo_left_prefix_product_start + S (1) = S ((S (0)) * ff_v_bpo_left_prefix_product)) /\ exists ff_q_bpo_left_prefix_product_start. ff_u_bpo_left_prefix_product = ff_q_bpo_left_prefix_product_start * S ((S (0)) * ff_v_bpo_left_prefix_product) + (1))) /\ ((((exists ff_h_bpo_left_prefix_product_terminal. ff_h_bpo_left_prefix_product_terminal + S (r) = S ((S (e)) * ff_v_bpo_left_prefix_product)) /\ exists ff_q_bpo_left_prefix_product_terminal. ff_u_bpo_left_prefix_product = ff_q_bpo_left_prefix_product_terminal * S ((S (e)) * ff_v_bpo_left_prefix_product) + (r))) /\ forall ff_i_bpo_left_prefix_product. (exists ff_lt_bpo_left_prefix_product_bound. ff_lt_bpo_left_prefix_product_bound + S ff_i_bpo_left_prefix_product = e) -> exists ff_p_bpo_left_prefix_product ff_r_bpo_left_prefix_product ff_s_bpo_left_prefix_product. ((((exists ff_h_bpo_left_prefix_product_factor. ff_h_bpo_left_prefix_product_factor + S (ff_p_bpo_left_prefix_product) = S ((S (ff_i_bpo_left_prefix_product)) * ff_c_bpo_left_prefix)) /\ exists ff_q_bpo_left_prefix_product_factor. ff_b_bpo_left_prefix = ff_q_bpo_left_prefix_product_factor * S ((S (ff_i_bpo_left_prefix_product)) * ff_c_bpo_left_prefix) + (ff_p_bpo_left_prefix_product))) /\ ((((exists ff_h_bpo_left_prefix_product_partial. ff_h_bpo_left_prefix_product_partial + S (ff_r_bpo_left_prefix_product) = S ((S (ff_i_bpo_left_prefix_product)) * ff_v_bpo_left_prefix_product)) /\ exists ff_q_bpo_left_prefix_product_partial. ff_u_bpo_left_prefix_product = ff_q_bpo_left_prefix_product_partial * S ((S (ff_i_bpo_left_prefix_product)) * ff_v_bpo_left_prefix_product) + (ff_r_bpo_left_prefix_product))) /\ ((((exists ff_h_bpo_left_prefix_product_successor. ff_h_bpo_left_prefix_product_successor + S (ff_s_bpo_left_prefix_product) = S ((S (S ff_i_bpo_left_prefix_product)) * ff_v_bpo_left_prefix_product)) /\ exists ff_q_bpo_left_prefix_product_successor. ff_u_bpo_left_prefix_product = ff_q_bpo_left_prefix_product_successor * S ((S (S ff_i_bpo_left_prefix_product)) * ff_v_bpo_left_prefix_product) + (ff_s_bpo_left_prefix_product))) /\ ff_s_bpo_left_prefix_product = ff_r_bpo_left_prefix_product * ff_p_bpo_left_prefix_product)))))))) /\ x = r * a
  34. 0034specialize pow_successor_decompose a
  35. 0035specialize pow_successor_decompose e
  36. 0036specialize pow_successor_decompose (S e)
  37. 0037specialize pow_successor_decompose x
  38. 0038apply pow_successor_decompose
  39. 0039refl
  40. 0040exact hx
  41. 0041cases hxstep
  42. 0042cases hxstep_witness
  43. 0043have hystep : exists s. (exists ff_b_bpo_right_prefix ff_c_bpo_right_prefix. ((forall ff_i_bpo_right_prefix_repeat. (exists ff_lt_bpo_right_prefix_repeat_bound. ff_lt_bpo_right_prefix_repeat_bound + S ff_i_bpo_right_prefix_repeat = e) -> (((exists ff_h_bpo_right_prefix_repeat_decoded. ff_h_bpo_right_prefix_repeat_decoded + S (b) = S ((S (ff_i_bpo_right_prefix_repeat)) * ff_c_bpo_right_prefix)) /\ exists ff_q_bpo_right_prefix_repeat_decoded. ff_b_bpo_right_prefix = ff_q_bpo_right_prefix_repeat_decoded * S ((S (ff_i_bpo_right_prefix_repeat)) * ff_c_bpo_right_prefix) + (b)))) /\ (exists ff_u_bpo_right_prefix_product ff_v_bpo_right_prefix_product. ((((exists ff_h_bpo_right_prefix_product_start. ff_h_bpo_right_prefix_product_start + S (1) = S ((S (0)) * ff_v_bpo_right_prefix_product)) /\ exists ff_q_bpo_right_prefix_product_start. ff_u_bpo_right_prefix_product = ff_q_bpo_right_prefix_product_start * S ((S (0)) * ff_v_bpo_right_prefix_product) + (1))) /\ ((((exists ff_h_bpo_right_prefix_product_terminal. ff_h_bpo_right_prefix_product_terminal + S (s) = S ((S (e)) * ff_v_bpo_right_prefix_product)) /\ exists ff_q_bpo_right_prefix_product_terminal. ff_u_bpo_right_prefix_product = ff_q_bpo_right_prefix_product_terminal * S ((S (e)) * ff_v_bpo_right_prefix_product) + (s))) /\ forall ff_i_bpo_right_prefix_product. (exists ff_lt_bpo_right_prefix_product_bound. ff_lt_bpo_right_prefix_product_bound + S ff_i_bpo_right_prefix_product = e) -> exists ff_p_bpo_right_prefix_product ff_r_bpo_right_prefix_product ff_s_bpo_right_prefix_product. ((((exists ff_h_bpo_right_prefix_product_factor. ff_h_bpo_right_prefix_product_factor + S (ff_p_bpo_right_prefix_product) = S ((S (ff_i_bpo_right_prefix_product)) * ff_c_bpo_right_prefix)) /\ exists ff_q_bpo_right_prefix_product_factor. ff_b_bpo_right_prefix = ff_q_bpo_right_prefix_product_factor * S ((S (ff_i_bpo_right_prefix_product)) * ff_c_bpo_right_prefix) + (ff_p_bpo_right_prefix_product))) /\ ((((exists ff_h_bpo_right_prefix_product_partial. ff_h_bpo_right_prefix_product_partial + S (ff_r_bpo_right_prefix_product) = S ((S (ff_i_bpo_right_prefix_product)) * ff_v_bpo_right_prefix_product)) /\ exists ff_q_bpo_right_prefix_product_partial. ff_u_bpo_right_prefix_product = ff_q_bpo_right_prefix_product_partial * S ((S (ff_i_bpo_right_prefix_product)) * ff_v_bpo_right_prefix_product) + (ff_r_bpo_right_prefix_product))) /\ ((((exists ff_h_bpo_right_prefix_product_successor. ff_h_bpo_right_prefix_product_successor + S (ff_s_bpo_right_prefix_product) = S ((S (S ff_i_bpo_right_prefix_product)) * ff_v_bpo_right_prefix_product)) /\ exists ff_q_bpo_right_prefix_product_successor. ff_u_bpo_right_prefix_product = ff_q_bpo_right_prefix_product_successor * S ((S (S ff_i_bpo_right_prefix_product)) * ff_v_bpo_right_prefix_product) + (ff_s_bpo_right_prefix_product))) /\ ff_s_bpo_right_prefix_product = ff_r_bpo_right_prefix_product * ff_p_bpo_right_prefix_product)))))))) /\ y = s * b
  44. 0044specialize pow_successor_decompose b
  45. 0045specialize pow_successor_decompose e
  46. 0046specialize pow_successor_decompose (S e)
  47. 0047specialize pow_successor_decompose y
  48. 0048apply pow_successor_decompose
  49. 0049refl
  50. 0050exact hy
  51. 0051cases hystep
  52. 0052cases hystep_witness
  53. 0053have hpref : exists k. k + x1 = x2
  54. 0054specialize IH x1
  55. 0055specialize IH x2
  56. 0056apply IH
  57. 0057exact hab
  58. 0058exact hxstep_witness_left
  59. 0059exact hystep_witness_left
  60. 0060rewrite hxstep_witness_right
  61. 0061rewrite hystep_witness_right
  62. 0062specialize mul_le_mul x1
  63. 0063specialize mul_le_mul x2
  64. 0064specialize mul_le_mul a
  65. 0065specialize mul_le_mul b
  66. 0066apply mul_le_mul
  67. 0067exact hpref
  68. 0068exact hab