BT00SN — pow_exponent_monotone_from

Exact expanded PA statement

forall a e f x y. (forall bpt_a_exponent bpt_e_exponent. exists bpt_x_exponent. (exists ff_b_bpt_value_exponent ff_c_bpt_value_exponent. ((forall ff_i_bpt_value_exponent_repeat. (exists ff_lt_bpt_value_exponent_repeat_bound. ff_lt_bpt_value_exponent_repeat_bound + S ff_i_bpt_value_exponent_repeat = bpt_e_exponent) -> (((exists ff_h_bpt_value_exponent_repeat_decoded. ff_h_bpt_value_exponent_repeat_decoded + S (bpt_a_exponent) = S ((S (ff_i_bpt_value_exponent_repeat)) * ff_c_bpt_value_exponent)) /\ exists ff_q_bpt_value_exponent_repeat_decoded. ff_b_bpt_value_exponent = ff_q_bpt_value_exponent_repeat_decoded * S ((S (ff_i_bpt_value_exponent_repeat)) * ff_c_bpt_value_exponent) + (bpt_a_exponent)))) /\ (exists ff_u_bpt_value_exponent_product ff_v_bpt_value_exponent_product. ((((exists ff_h_bpt_value_exponent_product_start. ff_h_bpt_value_exponent_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_exponent_product)) /\ exists ff_q_bpt_value_exponent_product_start. ff_u_bpt_value_exponent_product = ff_q_bpt_value_exponent_product_start * S ((S (0)) * ff_v_bpt_value_exponent_product) + (1))) /\ ((((exists ff_h_bpt_value_exponent_product_terminal. ff_h_bpt_value_exponent_product_terminal + S (bpt_x_exponent) = S ((S (bpt_e_exponent)) * ff_v_bpt_value_exponent_product)) /\ exists ff_q_bpt_value_exponent_product_terminal. ff_u_bpt_value_exponent_product = ff_q_bpt_value_exponent_product_terminal * S ((S (bpt_e_exponent)) * ff_v_bpt_value_exponent_product) + (bpt_x_exponent))) /\ forall ff_i_bpt_value_exponent_product. (exists ff_lt_bpt_value_exponent_product_bound. ff_lt_bpt_value_exponent_product_bound + S ff_i_bpt_value_exponent_product = bpt_e_exponent) -> exists ff_p_bpt_value_exponent_product ff_r_bpt_value_exponent_product ff_s_bpt_value_exponent_product. ((((exists ff_h_bpt_value_exponent_product_factor. ff_h_bpt_value_exponent_product_factor + S (ff_p_bpt_value_exponent_product) = S ((S (ff_i_bpt_value_exponent_product)) * ff_c_bpt_value_exponent)) /\ exists ff_q_bpt_value_exponent_product_factor. ff_b_bpt_value_exponent = ff_q_bpt_value_exponent_product_factor * S ((S (ff_i_bpt_value_exponent_product)) * ff_c_bpt_value_exponent) + (ff_p_bpt_value_exponent_product))) /\ ((((exists ff_h_bpt_value_exponent_product_partial. ff_h_bpt_value_exponent_product_partial + S (ff_r_bpt_value_exponent_product) = S ((S (ff_i_bpt_value_exponent_product)) * ff_v_bpt_value_exponent_product)) /\ exists ff_q_bpt_value_exponent_product_partial. ff_u_bpt_value_exponent_product = ff_q_bpt_value_exponent_product_partial * S ((S (ff_i_bpt_value_exponent_product)) * ff_v_bpt_value_exponent_product) + (ff_r_bpt_value_exponent_product))) /\ ((((exists ff_h_bpt_value_exponent_product_successor. ff_h_bpt_value_exponent_product_successor + S (ff_s_bpt_value_exponent_product) = S ((S (S ff_i_bpt_value_exponent_product)) * ff_v_bpt_value_exponent_product)) /\ exists ff_q_bpt_value_exponent_product_successor. ff_u_bpt_value_exponent_product = ff_q_bpt_value_exponent_product_successor * S ((S (S ff_i_bpt_value_exponent_product)) * ff_v_bpt_value_exponent_product) + (ff_s_bpt_value_exponent_product))) /\ ff_s_bpt_value_exponent_product = ff_r_bpt_value_exponent_product * ff_p_bpt_value_exponent_product))))))))) -> (exists bpt_gap_exponent_base. bpt_gap_exponent_base + 1 = a) -> (exists bpt_gap_exponent_order. bpt_gap_exponent_order + e = f) -> (exists ff_b_bpt_exp_left ff_c_bpt_exp_left. ((forall ff_i_bpt_exp_left_repeat. (exists ff_lt_bpt_exp_left_repeat_bound. ff_lt_bpt_exp_left_repeat_bound + S ff_i_bpt_exp_left_repeat = e) -> (((exists ff_h_bpt_exp_left_repeat_decoded. ff_h_bpt_exp_left_repeat_decoded + S (a) = S ((S (ff_i_bpt_exp_left_repeat)) * ff_c_bpt_exp_left)) /\ exists ff_q_bpt_exp_left_repeat_decoded. ff_b_bpt_exp_left = ff_q_bpt_exp_left_repeat_decoded * S ((S (ff_i_bpt_exp_left_repeat)) * ff_c_bpt_exp_left) + (a)))) /\ (exists ff_u_bpt_exp_left_product ff_v_bpt_exp_left_product. ((((exists ff_h_bpt_exp_left_product_start. ff_h_bpt_exp_left_product_start + S (1) = S ((S (0)) * ff_v_bpt_exp_left_product)) /\ exists ff_q_bpt_exp_left_product_start. ff_u_bpt_exp_left_product = ff_q_bpt_exp_left_product_start * S ((S (0)) * ff_v_bpt_exp_left_product) + (1))) /\ ((((exists ff_h_bpt_exp_left_product_terminal. ff_h_bpt_exp_left_product_terminal + S (x) = S ((S (e)) * ff_v_bpt_exp_left_product)) /\ exists ff_q_bpt_exp_left_product_terminal. ff_u_bpt_exp_left_product = ff_q_bpt_exp_left_product_terminal * S ((S (e)) * ff_v_bpt_exp_left_product) + (x))) /\ forall ff_i_bpt_exp_left_product. (exists ff_lt_bpt_exp_left_product_bound. ff_lt_bpt_exp_left_product_bound + S ff_i_bpt_exp_left_product = e) -> exists ff_p_bpt_exp_left_product ff_r_bpt_exp_left_product ff_s_bpt_exp_left_product. ((((exists ff_h_bpt_exp_left_product_factor. ff_h_bpt_exp_left_product_factor + S (ff_p_bpt_exp_left_product) = S ((S (ff_i_bpt_exp_left_product)) * ff_c_bpt_exp_left)) /\ exists ff_q_bpt_exp_left_product_factor. ff_b_bpt_exp_left = ff_q_bpt_exp_left_product_factor * S ((S (ff_i_bpt_exp_left_product)) * ff_c_bpt_exp_left) + (ff_p_bpt_exp_left_product))) /\ ((((exists ff_h_bpt_exp_left_product_partial. ff_h_bpt_exp_left_product_partial + S (ff_r_bpt_exp_left_product) = S ((S (ff_i_bpt_exp_left_product)) * ff_v_bpt_exp_left_product)) /\ exists ff_q_bpt_exp_left_product_partial. ff_u_bpt_exp_left_product = ff_q_bpt_exp_left_product_partial * S ((S (ff_i_bpt_exp_left_product)) * ff_v_bpt_exp_left_product) + (ff_r_bpt_exp_left_product))) /\ ((((exists ff_h_bpt_exp_left_product_successor. ff_h_bpt_exp_left_product_successor + S (ff_s_bpt_exp_left_product) = S ((S (S ff_i_bpt_exp_left_product)) * ff_v_bpt_exp_left_product)) /\ exists ff_q_bpt_exp_left_product_successor. ff_u_bpt_exp_left_product = ff_q_bpt_exp_left_product_successor * S ((S (S ff_i_bpt_exp_left_product)) * ff_v_bpt_exp_left_product) + (ff_s_bpt_exp_left_product))) /\ ff_s_bpt_exp_left_product = ff_r_bpt_exp_left_product * ff_p_bpt_exp_left_product)))))))) -> (exists ff_b_bpt_exp_right ff_c_bpt_exp_right. ((forall ff_i_bpt_exp_right_repeat. (exists ff_lt_bpt_exp_right_repeat_bound. ff_lt_bpt_exp_right_repeat_bound + S ff_i_bpt_exp_right_repeat = f) -> (((exists ff_h_bpt_exp_right_repeat_decoded. ff_h_bpt_exp_right_repeat_decoded + S (a) = S ((S (ff_i_bpt_exp_right_repeat)) * ff_c_bpt_exp_right)) /\ exists ff_q_bpt_exp_right_repeat_decoded. ff_b_bpt_exp_right = ff_q_bpt_exp_right_repeat_decoded * S ((S (ff_i_bpt_exp_right_repeat)) * ff_c_bpt_exp_right) + (a)))) /\ (exists ff_u_bpt_exp_right_product ff_v_bpt_exp_right_product. ((((exists ff_h_bpt_exp_right_product_start. ff_h_bpt_exp_right_product_start + S (1) = S ((S (0)) * ff_v_bpt_exp_right_product)) /\ exists ff_q_bpt_exp_right_product_start. ff_u_bpt_exp_right_product = ff_q_bpt_exp_right_product_start * S ((S (0)) * ff_v_bpt_exp_right_product) + (1))) /\ ((((exists ff_h_bpt_exp_right_product_terminal. ff_h_bpt_exp_right_product_terminal + S (y) = S ((S (f)) * ff_v_bpt_exp_right_product)) /\ exists ff_q_bpt_exp_right_product_terminal. ff_u_bpt_exp_right_product = ff_q_bpt_exp_right_product_terminal * S ((S (f)) * ff_v_bpt_exp_right_product) + (y))) /\ forall ff_i_bpt_exp_right_product. (exists ff_lt_bpt_exp_right_product_bound. ff_lt_bpt_exp_right_product_bound + S ff_i_bpt_exp_right_product = f) -> exists ff_p_bpt_exp_right_product ff_r_bpt_exp_right_product ff_s_bpt_exp_right_product. ((((exists ff_h_bpt_exp_right_product_factor. ff_h_bpt_exp_right_product_factor + S (ff_p_bpt_exp_right_product) = S ((S (ff_i_bpt_exp_right_product)) * ff_c_bpt_exp_right)) /\ exists ff_q_bpt_exp_right_product_factor. ff_b_bpt_exp_right = ff_q_bpt_exp_right_product_factor * S ((S (ff_i_bpt_exp_right_product)) * ff_c_bpt_exp_right) + (ff_p_bpt_exp_right_product))) /\ ((((exists ff_h_bpt_exp_right_product_partial. ff_h_bpt_exp_right_product_partial + S (ff_r_bpt_exp_right_product) = S ((S (ff_i_bpt_exp_right_product)) * ff_v_bpt_exp_right_product)) /\ exists ff_q_bpt_exp_right_product_partial. ff_u_bpt_exp_right_product = ff_q_bpt_exp_right_product_partial * S ((S (ff_i_bpt_exp_right_product)) * ff_v_bpt_exp_right_product) + (ff_r_bpt_exp_right_product))) /\ ((((exists ff_h_bpt_exp_right_product_successor. ff_h_bpt_exp_right_product_successor + S (ff_s_bpt_exp_right_product) = S ((S (S ff_i_bpt_exp_right_product)) * ff_v_bpt_exp_right_product)) /\ exists ff_q_bpt_exp_right_product_successor. ff_u_bpt_exp_right_product = ff_q_bpt_exp_right_product_successor * S ((S (S ff_i_bpt_exp_right_product)) * ff_v_bpt_exp_right_product) + (ff_s_bpt_exp_right_product))) /\ ff_s_bpt_exp_right_product = ff_r_bpt_exp_right_product * ff_p_bpt_exp_right_product)))))))) -> (exists bpt_gap_exponent_result. bpt_gap_exponent_result + x = y)

Structural proof guide

Exponent monotonicity reuses one supplied power-totality proof.

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

Proof neighborhood

Direct dependencies

BT009X pow_add BT00Q0 one_le_pow BT00PW le_mul_of_one_le_right BT0002 add_comm

Direct dependents

BT00WP bertrand_h_root_32_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 BT00X5 bertrand_four_power_product_le_of_sum_from_total

Formal native tactic body

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

0001intro a
0002intro e
0003intro f
0004intro x
0005intro y
0006intro htotal
0007intro ha
0008intro hef
0009intro hx
0010intro hy
0011cases hef
0012have hsum : f = e + x1
0013trans x1 + e
0014symm
0015exact hef_witness
0016specialize add_comm x1
0017specialize add_comm e
0018exact add_comm
0019have hgap : exists z. (exists ff_b_bpt_exp_gap ff_c_bpt_exp_gap. ((forall ff_i_bpt_exp_gap_repeat. (exists ff_lt_bpt_exp_gap_repeat_bound. ff_lt_bpt_exp_gap_repeat_bound + S ff_i_bpt_exp_gap_repeat = x1) -> (((exists ff_h_bpt_exp_gap_repeat_decoded. ff_h_bpt_exp_gap_repeat_decoded + S (a) = S ((S (ff_i_bpt_exp_gap_repeat)) * ff_c_bpt_exp_gap)) /\ exists ff_q_bpt_exp_gap_repeat_decoded. ff_b_bpt_exp_gap = ff_q_bpt_exp_gap_repeat_decoded * S ((S (ff_i_bpt_exp_gap_repeat)) * ff_c_bpt_exp_gap) + (a)))) /\ (exists ff_u_bpt_exp_gap_product ff_v_bpt_exp_gap_product. ((((exists ff_h_bpt_exp_gap_product_start. ff_h_bpt_exp_gap_product_start + S (1) = S ((S (0)) * ff_v_bpt_exp_gap_product)) /\ exists ff_q_bpt_exp_gap_product_start. ff_u_bpt_exp_gap_product = ff_q_bpt_exp_gap_product_start * S ((S (0)) * ff_v_bpt_exp_gap_product) + (1))) /\ ((((exists ff_h_bpt_exp_gap_product_terminal. ff_h_bpt_exp_gap_product_terminal + S (z) = S ((S (x1)) * ff_v_bpt_exp_gap_product)) /\ exists ff_q_bpt_exp_gap_product_terminal. ff_u_bpt_exp_gap_product = ff_q_bpt_exp_gap_product_terminal * S ((S (x1)) * ff_v_bpt_exp_gap_product) + (z))) /\ forall ff_i_bpt_exp_gap_product. (exists ff_lt_bpt_exp_gap_product_bound. ff_lt_bpt_exp_gap_product_bound + S ff_i_bpt_exp_gap_product = x1) -> exists ff_p_bpt_exp_gap_product ff_r_bpt_exp_gap_product ff_s_bpt_exp_gap_product. ((((exists ff_h_bpt_exp_gap_product_factor. ff_h_bpt_exp_gap_product_factor + S (ff_p_bpt_exp_gap_product) = S ((S (ff_i_bpt_exp_gap_product)) * ff_c_bpt_exp_gap)) /\ exists ff_q_bpt_exp_gap_product_factor. ff_b_bpt_exp_gap = ff_q_bpt_exp_gap_product_factor * S ((S (ff_i_bpt_exp_gap_product)) * ff_c_bpt_exp_gap) + (ff_p_bpt_exp_gap_product))) /\ ((((exists ff_h_bpt_exp_gap_product_partial. ff_h_bpt_exp_gap_product_partial + S (ff_r_bpt_exp_gap_product) = S ((S (ff_i_bpt_exp_gap_product)) * ff_v_bpt_exp_gap_product)) /\ exists ff_q_bpt_exp_gap_product_partial. ff_u_bpt_exp_gap_product = ff_q_bpt_exp_gap_product_partial * S ((S (ff_i_bpt_exp_gap_product)) * ff_v_bpt_exp_gap_product) + (ff_r_bpt_exp_gap_product))) /\ ((((exists ff_h_bpt_exp_gap_product_successor. ff_h_bpt_exp_gap_product_successor + S (ff_s_bpt_exp_gap_product) = S ((S (S ff_i_bpt_exp_gap_product)) * ff_v_bpt_exp_gap_product)) /\ exists ff_q_bpt_exp_gap_product_successor. ff_u_bpt_exp_gap_product = ff_q_bpt_exp_gap_product_successor * S ((S (S ff_i_bpt_exp_gap_product)) * ff_v_bpt_exp_gap_product) + (ff_s_bpt_exp_gap_product))) /\ ff_s_bpt_exp_gap_product = ff_r_bpt_exp_gap_product * ff_p_bpt_exp_gap_product))))))))
0020specialize htotal a
0021specialize htotal x1
0022exact htotal
0023cases hgap
0024have hyfactor : y = x * x2
0025specialize pow_add a
0026specialize pow_add e
0027specialize pow_add x1
0028specialize pow_add f
0029specialize pow_add x
0030specialize pow_add x2
0031specialize pow_add y
0032apply pow_add
0033exact hsum
0034exact hx
0035exact hgap_witness
0036exact hy
0037have hgap1 : exists k. k + 1 = x2
0038specialize one_le_pow a
0039specialize one_le_pow x1
0040specialize one_le_pow x2
0041apply one_le_pow
0042exact ha
0043exact hgap_witness
0044rewrite hyfactor
0045specialize le_mul_of_one_le_right x
0046specialize le_mul_of_one_le_right x2
0047apply le_mul_of_one_le_right
0048exact hgap1