BT00X6

bertrand_main_inequality_factorized_from_total

Alpha body-checked · checked-use disabled

The factorized threshold and all-root envelope imply the B6 power-product inequality under one supplied power-totality premise.

Exact expanded PA statement

forall n s q r A B F. (forall bpt_a_b6_main_factorized bpt_e_b6_main_factorized. exists bpt_x_b6_main_factorized. (exists ff_b_bpt_value_b6_main_factorized ff_c_bpt_value_b6_main_factorized. ((forall ff_i_bpt_value_b6_main_factorized_repeat. (exists ff_lt_bpt_value_b6_main_factorized_repeat_bound. ff_lt_bpt_value_b6_main_factorized_repeat_bound + S ff_i_bpt_value_b6_main_factorized_repeat = bpt_e_b6_main_factorized) -> (((exists ff_h_bpt_value_b6_main_factorized_repeat_decoded. ff_h_bpt_value_b6_main_factorized_repeat_decoded + S (bpt_a_b6_main_factorized) = S ((S (ff_i_bpt_value_b6_main_factorized_repeat)) * ff_c_bpt_value_b6_main_factorized)) /\ exists ff_q_bpt_value_b6_main_factorized_repeat_decoded. ff_b_bpt_value_b6_main_factorized = ff_q_bpt_value_b6_main_factorized_repeat_decoded * S ((S (ff_i_bpt_value_b6_main_factorized_repeat)) * ff_c_bpt_value_b6_main_factorized) + (bpt_a_b6_main_factorized)))) /\ (exists ff_u_bpt_value_b6_main_factorized_product ff_v_bpt_value_b6_main_factorized_product. ((((exists ff_h_bpt_value_b6_main_factorized_product_start. ff_h_bpt_value_b6_main_factorized_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_b6_main_factorized_product)) /\ exists ff_q_bpt_value_b6_main_factorized_product_start. ff_u_bpt_value_b6_main_factorized_product = ff_q_bpt_value_b6_main_factorized_product_start * S ((S (0)) * ff_v_bpt_value_b6_main_factorized_product) + (1))) /\ ((((exists ff_h_bpt_value_b6_main_factorized_product_terminal. ff_h_bpt_value_b6_main_factorized_product_terminal + S (bpt_x_b6_main_factorized) = S ((S (bpt_e_b6_main_factorized)) * ff_v_bpt_value_b6_main_factorized_product)) /\ exists ff_q_bpt_value_b6_main_factorized_product_terminal. ff_u_bpt_value_b6_main_factorized_product = ff_q_bpt_value_b6_main_factorized_product_terminal * S ((S (bpt_e_b6_main_factorized)) * ff_v_bpt_value_b6_main_factorized_product) + (bpt_x_b6_main_factorized))) /\ forall ff_i_bpt_value_b6_main_factorized_product. (exists ff_lt_bpt_value_b6_main_factorized_product_bound. ff_lt_bpt_value_b6_main_factorized_product_bound + S ff_i_bpt_value_b6_main_factorized_product = bpt_e_b6_main_factorized) -> exists ff_p_bpt_value_b6_main_factorized_product ff_r_bpt_value_b6_main_factorized_product ff_s_bpt_value_b6_main_factorized_product. ((((exists ff_h_bpt_value_b6_main_factorized_product_factor. ff_h_bpt_value_b6_main_factorized_product_factor + S (ff_p_bpt_value_b6_main_factorized_product) = S ((S (ff_i_bpt_value_b6_main_factorized_product)) * ff_c_bpt_value_b6_main_factorized)) /\ exists ff_q_bpt_value_b6_main_factorized_product_factor. ff_b_bpt_value_b6_main_factorized = ff_q_bpt_value_b6_main_factorized_product_factor * S ((S (ff_i_bpt_value_b6_main_factorized_product)) * ff_c_bpt_value_b6_main_factorized) + (ff_p_bpt_value_b6_main_factorized_product))) /\ ((((exists ff_h_bpt_value_b6_main_factorized_product_partial. ff_h_bpt_value_b6_main_factorized_product_partial + S (ff_r_bpt_value_b6_main_factorized_product) = S ((S (ff_i_bpt_value_b6_main_factorized_product)) * ff_v_bpt_value_b6_main_factorized_product)) /\ exists ff_q_bpt_value_b6_main_factorized_product_partial. ff_u_bpt_value_b6_main_factorized_product = ff_q_bpt_value_b6_main_factorized_product_partial * S ((S (ff_i_bpt_value_b6_main_factorized_product)) * ff_v_bpt_value_b6_main_factorized_product) + (ff_r_bpt_value_b6_main_factorized_product))) /\ ((((exists ff_h_bpt_value_b6_main_factorized_product_successor. ff_h_bpt_value_b6_main_factorized_product_successor + S (ff_s_bpt_value_b6_main_factorized_product) = S ((S (S ff_i_bpt_value_b6_main_factorized_product)) * ff_v_bpt_value_b6_main_factorized_product)) /\ exists ff_q_bpt_value_b6_main_factorized_product_successor. ff_u_bpt_value_b6_main_factorized_product = ff_q_bpt_value_b6_main_factorized_product_successor * S ((S (S ff_i_bpt_value_b6_main_factorized_product)) * ff_v_bpt_value_b6_main_factorized_product) + (ff_s_bpt_value_b6_main_factorized_product))) /\ ff_s_bpt_value_b6_main_factorized_product = ff_r_bpt_value_b6_main_factorized_product * ff_p_bpt_value_b6_main_factorized_product))))))))) -> (exists bqb_le_gap_b6_main_factorized_threshold. bqb_le_gap_b6_main_factorized_threshold + (16 * 32) = (n)) -> (((exists bcs_sqrt_lower_gap_b6_main_factorized_floor. bcs_sqrt_lower_gap_b6_main_factorized_floor + (s) * (s) = (2 * n)) /\ exists bcs_sqrt_upper_gap_b6_main_factorized_floor. bcs_sqrt_upper_gap_b6_main_factorized_floor + S (2 * n) = S (s) * S (s))) -> ((((2 * n) = 3 * (q) + (r)) /\ exists bmi_remainder_gap_b6_main_factorized_division. bmi_remainder_gap_b6_main_factorized_division + S (r) = 3)) -> (exists pa_b_b6_main_factorized_a pa_c_b6_main_factorized_a. ((forall pa_i_b6_main_factorized_a_repeat. (exists pa_lt_b6_main_factorized_a_repeat_bound. pa_lt_b6_main_factorized_a_repeat_bound + S pa_i_b6_main_factorized_a_repeat = s) -> (((exists pa_h_b6_main_factorized_a_repeat_decoded. pa_h_b6_main_factorized_a_repeat_decoded + S (2 * n) = S ((S (pa_i_b6_main_factorized_a_repeat)) * pa_c_b6_main_factorized_a)) /\ exists pa_q_b6_main_factorized_a_repeat_decoded. pa_b_b6_main_factorized_a = pa_q_b6_main_factorized_a_repeat_decoded * S ((S (pa_i_b6_main_factorized_a_repeat)) * pa_c_b6_main_factorized_a) + (2 * n)))) /\ (exists pa_u_b6_main_factorized_a_product pa_v_b6_main_factorized_a_product. ((((exists pa_h_b6_main_factorized_a_product_start. pa_h_b6_main_factorized_a_product_start + S (1) = S ((S (0)) * pa_v_b6_main_factorized_a_product)) /\ exists pa_q_b6_main_factorized_a_product_start. pa_u_b6_main_factorized_a_product = pa_q_b6_main_factorized_a_product_start * S ((S (0)) * pa_v_b6_main_factorized_a_product) + (1))) /\ ((((exists pa_h_b6_main_factorized_a_product_terminal. pa_h_b6_main_factorized_a_product_terminal + S (A) = S ((S (s)) * pa_v_b6_main_factorized_a_product)) /\ exists pa_q_b6_main_factorized_a_product_terminal. pa_u_b6_main_factorized_a_product = pa_q_b6_main_factorized_a_product_terminal * S ((S (s)) * pa_v_b6_main_factorized_a_product) + (A))) /\ forall pa_i_b6_main_factorized_a_product. (exists pa_lt_b6_main_factorized_a_product_bound. pa_lt_b6_main_factorized_a_product_bound + S pa_i_b6_main_factorized_a_product = s) -> exists pa_p_b6_main_factorized_a_product pa_r_b6_main_factorized_a_product pa_s_b6_main_factorized_a_product. ((((exists pa_h_b6_main_factorized_a_product_factor. pa_h_b6_main_factorized_a_product_factor + S (pa_p_b6_main_factorized_a_product) = S ((S (pa_i_b6_main_factorized_a_product)) * pa_c_b6_main_factorized_a)) /\ exists pa_q_b6_main_factorized_a_product_factor. pa_b_b6_main_factorized_a = pa_q_b6_main_factorized_a_product_factor * S ((S (pa_i_b6_main_factorized_a_product)) * pa_c_b6_main_factorized_a) + (pa_p_b6_main_factorized_a_product))) /\ ((((exists pa_h_b6_main_factorized_a_product_partial. pa_h_b6_main_factorized_a_product_partial + S (pa_r_b6_main_factorized_a_product) = S ((S (pa_i_b6_main_factorized_a_product)) * pa_v_b6_main_factorized_a_product)) /\ exists pa_q_b6_main_factorized_a_product_partial. pa_u_b6_main_factorized_a_product = pa_q_b6_main_factorized_a_product_partial * S ((S (pa_i_b6_main_factorized_a_product)) * pa_v_b6_main_factorized_a_product) + (pa_r_b6_main_factorized_a_product))) /\ ((((exists pa_h_b6_main_factorized_a_product_successor. pa_h_b6_main_factorized_a_product_successor + S (pa_s_b6_main_factorized_a_product) = S ((S (S pa_i_b6_main_factorized_a_product)) * pa_v_b6_main_factorized_a_product)) /\ exists pa_q_b6_main_factorized_a_product_successor. pa_u_b6_main_factorized_a_product = pa_q_b6_main_factorized_a_product_successor * S ((S (S pa_i_b6_main_factorized_a_product)) * pa_v_b6_main_factorized_a_product) + (pa_s_b6_main_factorized_a_product))) /\ pa_s_b6_main_factorized_a_product = pa_r_b6_main_factorized_a_product * pa_p_b6_main_factorized_a_product)))))))) -> (exists pa_b_b6_main_factorized_b pa_c_b6_main_factorized_b. ((forall pa_i_b6_main_factorized_b_repeat. (exists pa_lt_b6_main_factorized_b_repeat_bound. pa_lt_b6_main_factorized_b_repeat_bound + S pa_i_b6_main_factorized_b_repeat = q) -> (((exists pa_h_b6_main_factorized_b_repeat_decoded. pa_h_b6_main_factorized_b_repeat_decoded + S (4) = S ((S (pa_i_b6_main_factorized_b_repeat)) * pa_c_b6_main_factorized_b)) /\ exists pa_q_b6_main_factorized_b_repeat_decoded. pa_b_b6_main_factorized_b = pa_q_b6_main_factorized_b_repeat_decoded * S ((S (pa_i_b6_main_factorized_b_repeat)) * pa_c_b6_main_factorized_b) + (4)))) /\ (exists pa_u_b6_main_factorized_b_product pa_v_b6_main_factorized_b_product. ((((exists pa_h_b6_main_factorized_b_product_start. pa_h_b6_main_factorized_b_product_start + S (1) = S ((S (0)) * pa_v_b6_main_factorized_b_product)) /\ exists pa_q_b6_main_factorized_b_product_start. pa_u_b6_main_factorized_b_product = pa_q_b6_main_factorized_b_product_start * S ((S (0)) * pa_v_b6_main_factorized_b_product) + (1))) /\ ((((exists pa_h_b6_main_factorized_b_product_terminal. pa_h_b6_main_factorized_b_product_terminal + S (B) = S ((S (q)) * pa_v_b6_main_factorized_b_product)) /\ exists pa_q_b6_main_factorized_b_product_terminal. pa_u_b6_main_factorized_b_product = pa_q_b6_main_factorized_b_product_terminal * S ((S (q)) * pa_v_b6_main_factorized_b_product) + (B))) /\ forall pa_i_b6_main_factorized_b_product. (exists pa_lt_b6_main_factorized_b_product_bound. pa_lt_b6_main_factorized_b_product_bound + S pa_i_b6_main_factorized_b_product = q) -> exists pa_p_b6_main_factorized_b_product pa_r_b6_main_factorized_b_product pa_s_b6_main_factorized_b_product. ((((exists pa_h_b6_main_factorized_b_product_factor. pa_h_b6_main_factorized_b_product_factor + S (pa_p_b6_main_factorized_b_product) = S ((S (pa_i_b6_main_factorized_b_product)) * pa_c_b6_main_factorized_b)) /\ exists pa_q_b6_main_factorized_b_product_factor. pa_b_b6_main_factorized_b = pa_q_b6_main_factorized_b_product_factor * S ((S (pa_i_b6_main_factorized_b_product)) * pa_c_b6_main_factorized_b) + (pa_p_b6_main_factorized_b_product))) /\ ((((exists pa_h_b6_main_factorized_b_product_partial. pa_h_b6_main_factorized_b_product_partial + S (pa_r_b6_main_factorized_b_product) = S ((S (pa_i_b6_main_factorized_b_product)) * pa_v_b6_main_factorized_b_product)) /\ exists pa_q_b6_main_factorized_b_product_partial. pa_u_b6_main_factorized_b_product = pa_q_b6_main_factorized_b_product_partial * S ((S (pa_i_b6_main_factorized_b_product)) * pa_v_b6_main_factorized_b_product) + (pa_r_b6_main_factorized_b_product))) /\ ((((exists pa_h_b6_main_factorized_b_product_successor. pa_h_b6_main_factorized_b_product_successor + S (pa_s_b6_main_factorized_b_product) = S ((S (S pa_i_b6_main_factorized_b_product)) * pa_v_b6_main_factorized_b_product)) /\ exists pa_q_b6_main_factorized_b_product_successor. pa_u_b6_main_factorized_b_product = pa_q_b6_main_factorized_b_product_successor * S ((S (S pa_i_b6_main_factorized_b_product)) * pa_v_b6_main_factorized_b_product) + (pa_s_b6_main_factorized_b_product))) /\ pa_s_b6_main_factorized_b_product = pa_r_b6_main_factorized_b_product * pa_p_b6_main_factorized_b_product)))))))) -> (exists pa_b_b6_main_factorized_f pa_c_b6_main_factorized_f. ((forall pa_i_b6_main_factorized_f_repeat. (exists pa_lt_b6_main_factorized_f_repeat_bound. pa_lt_b6_main_factorized_f_repeat_bound + S pa_i_b6_main_factorized_f_repeat = n) -> (((exists pa_h_b6_main_factorized_f_repeat_decoded. pa_h_b6_main_factorized_f_repeat_decoded + S (4) = S ((S (pa_i_b6_main_factorized_f_repeat)) * pa_c_b6_main_factorized_f)) /\ exists pa_q_b6_main_factorized_f_repeat_decoded. pa_b_b6_main_factorized_f = pa_q_b6_main_factorized_f_repeat_decoded * S ((S (pa_i_b6_main_factorized_f_repeat)) * pa_c_b6_main_factorized_f) + (4)))) /\ (exists pa_u_b6_main_factorized_f_product pa_v_b6_main_factorized_f_product. ((((exists pa_h_b6_main_factorized_f_product_start. pa_h_b6_main_factorized_f_product_start + S (1) = S ((S (0)) * pa_v_b6_main_factorized_f_product)) /\ exists pa_q_b6_main_factorized_f_product_start. pa_u_b6_main_factorized_f_product = pa_q_b6_main_factorized_f_product_start * S ((S (0)) * pa_v_b6_main_factorized_f_product) + (1))) /\ ((((exists pa_h_b6_main_factorized_f_product_terminal. pa_h_b6_main_factorized_f_product_terminal + S (F) = S ((S (n)) * pa_v_b6_main_factorized_f_product)) /\ exists pa_q_b6_main_factorized_f_product_terminal. pa_u_b6_main_factorized_f_product = pa_q_b6_main_factorized_f_product_terminal * S ((S (n)) * pa_v_b6_main_factorized_f_product) + (F))) /\ forall pa_i_b6_main_factorized_f_product. (exists pa_lt_b6_main_factorized_f_product_bound. pa_lt_b6_main_factorized_f_product_bound + S pa_i_b6_main_factorized_f_product = n) -> exists pa_p_b6_main_factorized_f_product pa_r_b6_main_factorized_f_product pa_s_b6_main_factorized_f_product. ((((exists pa_h_b6_main_factorized_f_product_factor. pa_h_b6_main_factorized_f_product_factor + S (pa_p_b6_main_factorized_f_product) = S ((S (pa_i_b6_main_factorized_f_product)) * pa_c_b6_main_factorized_f)) /\ exists pa_q_b6_main_factorized_f_product_factor. pa_b_b6_main_factorized_f = pa_q_b6_main_factorized_f_product_factor * S ((S (pa_i_b6_main_factorized_f_product)) * pa_c_b6_main_factorized_f) + (pa_p_b6_main_factorized_f_product))) /\ ((((exists pa_h_b6_main_factorized_f_product_partial. pa_h_b6_main_factorized_f_product_partial + S (pa_r_b6_main_factorized_f_product) = S ((S (pa_i_b6_main_factorized_f_product)) * pa_v_b6_main_factorized_f_product)) /\ exists pa_q_b6_main_factorized_f_product_partial. pa_u_b6_main_factorized_f_product = pa_q_b6_main_factorized_f_product_partial * S ((S (pa_i_b6_main_factorized_f_product)) * pa_v_b6_main_factorized_f_product) + (pa_r_b6_main_factorized_f_product))) /\ ((((exists pa_h_b6_main_factorized_f_product_successor. pa_h_b6_main_factorized_f_product_successor + S (pa_s_b6_main_factorized_f_product) = S ((S (S pa_i_b6_main_factorized_f_product)) * pa_v_b6_main_factorized_f_product)) /\ exists pa_q_b6_main_factorized_f_product_successor. pa_u_b6_main_factorized_f_product = pa_q_b6_main_factorized_f_product_successor * S ((S (S pa_i_b6_main_factorized_f_product)) * pa_v_b6_main_factorized_f_product) + (pa_s_b6_main_factorized_f_product))) /\ pa_s_b6_main_factorized_f_product = pa_r_b6_main_factorized_f_product * pa_p_b6_main_factorized_f_product)))))))) -> (exists bqb_le_gap_b6_main_factorized_result. bqb_le_gap_b6_main_factorized_result + (n * A * B) = (F))

Structural proof guide

The factorized threshold and all-root envelope imply the B6 power-product inequality under one supplied power-totality premise.

Direct prerequisites: floor_sqrt_factorized_threshold_thirty_two, ceil_div_six_total, bertrand_hj_envelope_thirty_two, floor_ceil_division_budget, bertrand_floor_power_product_le_h_from_total, bertrand_four_power_product_le_of_sum_from_total, mul_le_mul_right, le_trans. The authored body proceeds by case analysis (10), intermediate claims (12).

Proof neighborhood

Direct dependencies

BT00X0 floor_sqrt_factorized_threshold_thirty_two BT00R1 ceil_div_six_total BT00X3 bertrand_hj_envelope_thirty_two BT00RJ floor_ceil_division_budget BT00X4 bertrand_floor_power_product_le_h_from_total BT00X5 bertrand_four_power_product_le_of_sum_from_total BT001M mul_le_mul_right BT000F le_trans

Direct dependents

BT00X7 bertrand_main_inequality_factorized

Formal native tactic body

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

  1. 0001intro n
  2. 0002intro s
  3. 0003intro q
  4. 0004intro r
  5. 0005intro A
  6. 0006intro B
  7. 0007intro F
  8. 0008intro htotal
  9. 0009intro hthreshold
  10. 0010intro hfloor
  11. 0011intro hdiv
  12. 0012intro hA
  13. 0013intro hB
  14. 0014intro hF
  15. 0015have hs : exists bqb_le_gap_b6_main_root_lower. bqb_le_gap_b6_main_root_lower + (32) = (s)
  16. 0016specialize floor_sqrt_factorized_threshold_thirty_two n
  17. 0017specialize floor_sqrt_factorized_threshold_thirty_two s
  18. 0018apply floor_sqrt_factorized_threshold_thirty_two
  19. 0019exact hthreshold
  20. 0020exact hfloor
  21. 0021have he_exists : exists e. (((exists bcs_lower_gap_b6_main_ceiling. bcs_lower_gap_b6_main_ceiling + (s * s) = 6 * (e)) /\ exists bcs_upper_gap_b6_main_ceiling. bcs_upper_gap_b6_main_ceiling + S (6 * (e)) = (s * s) + 6))
  22. 0022specialize ceil_div_six_total (s * s)
  23. 0023exact ceil_div_six_total
  24. 0024cases he_exists
  25. 0025have hH_exists : exists H. (exists pa_b_b6_main_envelope_h pa_c_b6_main_envelope_h. ((forall pa_i_b6_main_envelope_h_repeat. (exists pa_lt_b6_main_envelope_h_repeat_bound. pa_lt_b6_main_envelope_h_repeat_bound + S pa_i_b6_main_envelope_h_repeat = 2 * s + 2) -> (((exists pa_h_b6_main_envelope_h_repeat_decoded. pa_h_b6_main_envelope_h_repeat_decoded + S (s + 1) = S ((S (pa_i_b6_main_envelope_h_repeat)) * pa_c_b6_main_envelope_h)) /\ exists pa_q_b6_main_envelope_h_repeat_decoded. pa_b_b6_main_envelope_h = pa_q_b6_main_envelope_h_repeat_decoded * S ((S (pa_i_b6_main_envelope_h_repeat)) * pa_c_b6_main_envelope_h) + (s + 1)))) /\ (exists pa_u_b6_main_envelope_h_product pa_v_b6_main_envelope_h_product. ((((exists pa_h_b6_main_envelope_h_product_start. pa_h_b6_main_envelope_h_product_start + S (1) = S ((S (0)) * pa_v_b6_main_envelope_h_product)) /\ exists pa_q_b6_main_envelope_h_product_start. pa_u_b6_main_envelope_h_product = pa_q_b6_main_envelope_h_product_start * S ((S (0)) * pa_v_b6_main_envelope_h_product) + (1))) /\ ((((exists pa_h_b6_main_envelope_h_product_terminal. pa_h_b6_main_envelope_h_product_terminal + S (H) = S ((S (2 * s + 2)) * pa_v_b6_main_envelope_h_product)) /\ exists pa_q_b6_main_envelope_h_product_terminal. pa_u_b6_main_envelope_h_product = pa_q_b6_main_envelope_h_product_terminal * S ((S (2 * s + 2)) * pa_v_b6_main_envelope_h_product) + (H))) /\ forall pa_i_b6_main_envelope_h_product. (exists pa_lt_b6_main_envelope_h_product_bound. pa_lt_b6_main_envelope_h_product_bound + S pa_i_b6_main_envelope_h_product = 2 * s + 2) -> exists pa_p_b6_main_envelope_h_product pa_r_b6_main_envelope_h_product pa_s_b6_main_envelope_h_product. ((((exists pa_h_b6_main_envelope_h_product_factor. pa_h_b6_main_envelope_h_product_factor + S (pa_p_b6_main_envelope_h_product) = S ((S (pa_i_b6_main_envelope_h_product)) * pa_c_b6_main_envelope_h)) /\ exists pa_q_b6_main_envelope_h_product_factor. pa_b_b6_main_envelope_h = pa_q_b6_main_envelope_h_product_factor * S ((S (pa_i_b6_main_envelope_h_product)) * pa_c_b6_main_envelope_h) + (pa_p_b6_main_envelope_h_product))) /\ ((((exists pa_h_b6_main_envelope_h_product_partial. pa_h_b6_main_envelope_h_product_partial + S (pa_r_b6_main_envelope_h_product) = S ((S (pa_i_b6_main_envelope_h_product)) * pa_v_b6_main_envelope_h_product)) /\ exists pa_q_b6_main_envelope_h_product_partial. pa_u_b6_main_envelope_h_product = pa_q_b6_main_envelope_h_product_partial * S ((S (pa_i_b6_main_envelope_h_product)) * pa_v_b6_main_envelope_h_product) + (pa_r_b6_main_envelope_h_product))) /\ ((((exists pa_h_b6_main_envelope_h_product_successor. pa_h_b6_main_envelope_h_product_successor + S (pa_s_b6_main_envelope_h_product) = S ((S (S pa_i_b6_main_envelope_h_product)) * pa_v_b6_main_envelope_h_product)) /\ exists pa_q_b6_main_envelope_h_product_successor. pa_u_b6_main_envelope_h_product = pa_q_b6_main_envelope_h_product_successor * S ((S (S pa_i_b6_main_envelope_h_product)) * pa_v_b6_main_envelope_h_product) + (pa_s_b6_main_envelope_h_product))) /\ pa_s_b6_main_envelope_h_product = pa_r_b6_main_envelope_h_product * pa_p_b6_main_envelope_h_product))))))))
  26. 0026specialize htotal (s + 1)
  27. 0027specialize htotal (2 * s + 2)
  28. 0028exact htotal
  29. 0029cases hH_exists
  30. 0030have hU_exists : exists U. (exists pa_b_b6_main_envelope_u_witness pa_c_b6_main_envelope_u_witness. ((forall pa_i_b6_main_envelope_u_witness_repeat. (exists pa_lt_b6_main_envelope_u_witness_repeat_bound. pa_lt_b6_main_envelope_u_witness_repeat_bound + S pa_i_b6_main_envelope_u_witness_repeat = x) -> (((exists pa_h_b6_main_envelope_u_witness_repeat_decoded. pa_h_b6_main_envelope_u_witness_repeat_decoded + S (4) = S ((S (pa_i_b6_main_envelope_u_witness_repeat)) * pa_c_b6_main_envelope_u_witness)) /\ exists pa_q_b6_main_envelope_u_witness_repeat_decoded. pa_b_b6_main_envelope_u_witness = pa_q_b6_main_envelope_u_witness_repeat_decoded * S ((S (pa_i_b6_main_envelope_u_witness_repeat)) * pa_c_b6_main_envelope_u_witness) + (4)))) /\ (exists pa_u_b6_main_envelope_u_witness_product pa_v_b6_main_envelope_u_witness_product. ((((exists pa_h_b6_main_envelope_u_witness_product_start. pa_h_b6_main_envelope_u_witness_product_start + S (1) = S ((S (0)) * pa_v_b6_main_envelope_u_witness_product)) /\ exists pa_q_b6_main_envelope_u_witness_product_start. pa_u_b6_main_envelope_u_witness_product = pa_q_b6_main_envelope_u_witness_product_start * S ((S (0)) * pa_v_b6_main_envelope_u_witness_product) + (1))) /\ ((((exists pa_h_b6_main_envelope_u_witness_product_terminal. pa_h_b6_main_envelope_u_witness_product_terminal + S (U) = S ((S (x)) * pa_v_b6_main_envelope_u_witness_product)) /\ exists pa_q_b6_main_envelope_u_witness_product_terminal. pa_u_b6_main_envelope_u_witness_product = pa_q_b6_main_envelope_u_witness_product_terminal * S ((S (x)) * pa_v_b6_main_envelope_u_witness_product) + (U))) /\ forall pa_i_b6_main_envelope_u_witness_product. (exists pa_lt_b6_main_envelope_u_witness_product_bound. pa_lt_b6_main_envelope_u_witness_product_bound + S pa_i_b6_main_envelope_u_witness_product = x) -> exists pa_p_b6_main_envelope_u_witness_product pa_r_b6_main_envelope_u_witness_product pa_s_b6_main_envelope_u_witness_product. ((((exists pa_h_b6_main_envelope_u_witness_product_factor. pa_h_b6_main_envelope_u_witness_product_factor + S (pa_p_b6_main_envelope_u_witness_product) = S ((S (pa_i_b6_main_envelope_u_witness_product)) * pa_c_b6_main_envelope_u_witness)) /\ exists pa_q_b6_main_envelope_u_witness_product_factor. pa_b_b6_main_envelope_u_witness = pa_q_b6_main_envelope_u_witness_product_factor * S ((S (pa_i_b6_main_envelope_u_witness_product)) * pa_c_b6_main_envelope_u_witness) + (pa_p_b6_main_envelope_u_witness_product))) /\ ((((exists pa_h_b6_main_envelope_u_witness_product_partial. pa_h_b6_main_envelope_u_witness_product_partial + S (pa_r_b6_main_envelope_u_witness_product) = S ((S (pa_i_b6_main_envelope_u_witness_product)) * pa_v_b6_main_envelope_u_witness_product)) /\ exists pa_q_b6_main_envelope_u_witness_product_partial. pa_u_b6_main_envelope_u_witness_product = pa_q_b6_main_envelope_u_witness_product_partial * S ((S (pa_i_b6_main_envelope_u_witness_product)) * pa_v_b6_main_envelope_u_witness_product) + (pa_r_b6_main_envelope_u_witness_product))) /\ ((((exists pa_h_b6_main_envelope_u_witness_product_successor. pa_h_b6_main_envelope_u_witness_product_successor + S (pa_s_b6_main_envelope_u_witness_product) = S ((S (S pa_i_b6_main_envelope_u_witness_product)) * pa_v_b6_main_envelope_u_witness_product)) /\ exists pa_q_b6_main_envelope_u_witness_product_successor. pa_u_b6_main_envelope_u_witness_product = pa_q_b6_main_envelope_u_witness_product_successor * S ((S (S pa_i_b6_main_envelope_u_witness_product)) * pa_v_b6_main_envelope_u_witness_product) + (pa_s_b6_main_envelope_u_witness_product))) /\ pa_s_b6_main_envelope_u_witness_product = pa_r_b6_main_envelope_u_witness_product * pa_p_b6_main_envelope_u_witness_product))))))))
  31. 0031specialize htotal 4
  32. 0032specialize htotal x
  33. 0033exact htotal
  34. 0034cases hU_exists
  35. 0035have hJ_exists : exists J. (exists pa_b_b6_main_envelope_j pa_c_b6_main_envelope_j. ((forall pa_i_b6_main_envelope_j_repeat. (exists pa_lt_b6_main_envelope_j_repeat_bound. pa_lt_b6_main_envelope_j_repeat_bound + S pa_i_b6_main_envelope_j_repeat = 12) -> (((exists pa_h_b6_main_envelope_j_repeat_decoded. pa_h_b6_main_envelope_j_repeat_decoded + S (s + 7) = S ((S (pa_i_b6_main_envelope_j_repeat)) * pa_c_b6_main_envelope_j)) /\ exists pa_q_b6_main_envelope_j_repeat_decoded. pa_b_b6_main_envelope_j = pa_q_b6_main_envelope_j_repeat_decoded * S ((S (pa_i_b6_main_envelope_j_repeat)) * pa_c_b6_main_envelope_j) + (s + 7)))) /\ (exists pa_u_b6_main_envelope_j_product pa_v_b6_main_envelope_j_product. ((((exists pa_h_b6_main_envelope_j_product_start. pa_h_b6_main_envelope_j_product_start + S (1) = S ((S (0)) * pa_v_b6_main_envelope_j_product)) /\ exists pa_q_b6_main_envelope_j_product_start. pa_u_b6_main_envelope_j_product = pa_q_b6_main_envelope_j_product_start * S ((S (0)) * pa_v_b6_main_envelope_j_product) + (1))) /\ ((((exists pa_h_b6_main_envelope_j_product_terminal. pa_h_b6_main_envelope_j_product_terminal + S (J) = S ((S (12)) * pa_v_b6_main_envelope_j_product)) /\ exists pa_q_b6_main_envelope_j_product_terminal. pa_u_b6_main_envelope_j_product = pa_q_b6_main_envelope_j_product_terminal * S ((S (12)) * pa_v_b6_main_envelope_j_product) + (J))) /\ forall pa_i_b6_main_envelope_j_product. (exists pa_lt_b6_main_envelope_j_product_bound. pa_lt_b6_main_envelope_j_product_bound + S pa_i_b6_main_envelope_j_product = 12) -> exists pa_p_b6_main_envelope_j_product pa_r_b6_main_envelope_j_product pa_s_b6_main_envelope_j_product. ((((exists pa_h_b6_main_envelope_j_product_factor. pa_h_b6_main_envelope_j_product_factor + S (pa_p_b6_main_envelope_j_product) = S ((S (pa_i_b6_main_envelope_j_product)) * pa_c_b6_main_envelope_j)) /\ exists pa_q_b6_main_envelope_j_product_factor. pa_b_b6_main_envelope_j = pa_q_b6_main_envelope_j_product_factor * S ((S (pa_i_b6_main_envelope_j_product)) * pa_c_b6_main_envelope_j) + (pa_p_b6_main_envelope_j_product))) /\ ((((exists pa_h_b6_main_envelope_j_product_partial. pa_h_b6_main_envelope_j_product_partial + S (pa_r_b6_main_envelope_j_product) = S ((S (pa_i_b6_main_envelope_j_product)) * pa_v_b6_main_envelope_j_product)) /\ exists pa_q_b6_main_envelope_j_product_partial. pa_u_b6_main_envelope_j_product = pa_q_b6_main_envelope_j_product_partial * S ((S (pa_i_b6_main_envelope_j_product)) * pa_v_b6_main_envelope_j_product) + (pa_r_b6_main_envelope_j_product))) /\ ((((exists pa_h_b6_main_envelope_j_product_successor. pa_h_b6_main_envelope_j_product_successor + S (pa_s_b6_main_envelope_j_product) = S ((S (S pa_i_b6_main_envelope_j_product)) * pa_v_b6_main_envelope_j_product)) /\ exists pa_q_b6_main_envelope_j_product_successor. pa_u_b6_main_envelope_j_product = pa_q_b6_main_envelope_j_product_successor * S ((S (S pa_i_b6_main_envelope_j_product)) * pa_v_b6_main_envelope_j_product) + (pa_s_b6_main_envelope_j_product))) /\ pa_s_b6_main_envelope_j_product = pa_r_b6_main_envelope_j_product * pa_p_b6_main_envelope_j_product))))))))
  36. 0036specialize htotal (s + 7)
  37. 0037specialize htotal 12
  38. 0038exact htotal
  39. 0039cases hJ_exists
  40. 0040have hG_exists : exists G. (exists pa_b_b6_main_envelope_g pa_c_b6_main_envelope_g. ((forall pa_i_b6_main_envelope_g_repeat. (exists pa_lt_b6_main_envelope_g_repeat_bound. pa_lt_b6_main_envelope_g_repeat_bound + S pa_i_b6_main_envelope_g_repeat = s + 5) -> (((exists pa_h_b6_main_envelope_g_repeat_decoded. pa_h_b6_main_envelope_g_repeat_decoded + S (4) = S ((S (pa_i_b6_main_envelope_g_repeat)) * pa_c_b6_main_envelope_g)) /\ exists pa_q_b6_main_envelope_g_repeat_decoded. pa_b_b6_main_envelope_g = pa_q_b6_main_envelope_g_repeat_decoded * S ((S (pa_i_b6_main_envelope_g_repeat)) * pa_c_b6_main_envelope_g) + (4)))) /\ (exists pa_u_b6_main_envelope_g_product pa_v_b6_main_envelope_g_product. ((((exists pa_h_b6_main_envelope_g_product_start. pa_h_b6_main_envelope_g_product_start + S (1) = S ((S (0)) * pa_v_b6_main_envelope_g_product)) /\ exists pa_q_b6_main_envelope_g_product_start. pa_u_b6_main_envelope_g_product = pa_q_b6_main_envelope_g_product_start * S ((S (0)) * pa_v_b6_main_envelope_g_product) + (1))) /\ ((((exists pa_h_b6_main_envelope_g_product_terminal. pa_h_b6_main_envelope_g_product_terminal + S (G) = S ((S (s + 5)) * pa_v_b6_main_envelope_g_product)) /\ exists pa_q_b6_main_envelope_g_product_terminal. pa_u_b6_main_envelope_g_product = pa_q_b6_main_envelope_g_product_terminal * S ((S (s + 5)) * pa_v_b6_main_envelope_g_product) + (G))) /\ forall pa_i_b6_main_envelope_g_product. (exists pa_lt_b6_main_envelope_g_product_bound. pa_lt_b6_main_envelope_g_product_bound + S pa_i_b6_main_envelope_g_product = s + 5) -> exists pa_p_b6_main_envelope_g_product pa_r_b6_main_envelope_g_product pa_s_b6_main_envelope_g_product. ((((exists pa_h_b6_main_envelope_g_product_factor. pa_h_b6_main_envelope_g_product_factor + S (pa_p_b6_main_envelope_g_product) = S ((S (pa_i_b6_main_envelope_g_product)) * pa_c_b6_main_envelope_g)) /\ exists pa_q_b6_main_envelope_g_product_factor. pa_b_b6_main_envelope_g = pa_q_b6_main_envelope_g_product_factor * S ((S (pa_i_b6_main_envelope_g_product)) * pa_c_b6_main_envelope_g) + (pa_p_b6_main_envelope_g_product))) /\ ((((exists pa_h_b6_main_envelope_g_product_partial. pa_h_b6_main_envelope_g_product_partial + S (pa_r_b6_main_envelope_g_product) = S ((S (pa_i_b6_main_envelope_g_product)) * pa_v_b6_main_envelope_g_product)) /\ exists pa_q_b6_main_envelope_g_product_partial. pa_u_b6_main_envelope_g_product = pa_q_b6_main_envelope_g_product_partial * S ((S (pa_i_b6_main_envelope_g_product)) * pa_v_b6_main_envelope_g_product) + (pa_r_b6_main_envelope_g_product))) /\ ((((exists pa_h_b6_main_envelope_g_product_successor. pa_h_b6_main_envelope_g_product_successor + S (pa_s_b6_main_envelope_g_product) = S ((S (S pa_i_b6_main_envelope_g_product)) * pa_v_b6_main_envelope_g_product)) /\ exists pa_q_b6_main_envelope_g_product_successor. pa_u_b6_main_envelope_g_product = pa_q_b6_main_envelope_g_product_successor * S ((S (S pa_i_b6_main_envelope_g_product)) * pa_v_b6_main_envelope_g_product) + (pa_s_b6_main_envelope_g_product))) /\ pa_s_b6_main_envelope_g_product = pa_r_b6_main_envelope_g_product * pa_p_b6_main_envelope_g_product))))))))
  41. 0041specialize htotal 4
  42. 0042specialize htotal (s + 5)
  43. 0043exact htotal
  44. 0044cases hG_exists
  45. 0045have henvelope : ((exists bqb_le_gap_b6_main_h_u_order. bqb_le_gap_b6_main_h_u_order + (x1) = (x2)) /\ (exists bqb_le_gap_b6_main_j_g_order. bqb_le_gap_b6_main_j_g_order + (x3) = (x4)))
  46. 0046specialize bertrand_hj_envelope_thirty_two s
  47. 0047specialize bertrand_hj_envelope_thirty_two x
  48. 0048specialize bertrand_hj_envelope_thirty_two x1
  49. 0049specialize bertrand_hj_envelope_thirty_two x2
  50. 0050specialize bertrand_hj_envelope_thirty_two x3
  51. 0051specialize bertrand_hj_envelope_thirty_two x4
  52. 0052apply bertrand_hj_envelope_thirty_two
  53. 0053exact hs
  54. 0054exact he_exists_witness
  55. 0055exact hH_exists_witness
  56. 0056exact hU_exists_witness
  57. 0057exact hJ_exists_witness
  58. 0058exact hG_exists_witness
  59. 0059cases henvelope
  60. 0060have hbudget : exists c. ((((((q) + (c) = (n)) /\ exists bqb_budget_gap_b6_main_budget_data. bqb_budget_gap_b6_main_budget_data + 2 * (n) = 6 * (c))) /\ (((exists bqb_le_gap_b6_main_budget_ec_witness. bqb_le_gap_b6_main_budget_ec_witness + (x) = (c)) /\ (exists bqb_le_gap_b6_main_budget_sum_witness. bqb_le_gap_b6_main_budget_sum_witness + (q + x) = (n))))) /\ exists bmi_remainder_gap_b6_main_budget_preserved. bmi_remainder_gap_b6_main_budget_preserved + S r = 3)
  61. 0061specialize floor_ceil_division_budget n
  62. 0062specialize floor_ceil_division_budget q
  63. 0063specialize floor_ceil_division_budget r
  64. 0064specialize floor_ceil_division_budget s
  65. 0065specialize floor_ceil_division_budget x
  66. 0066apply floor_ceil_division_budget
  67. 0067exact hfloor
  68. 0068exact he_exists_witness
  69. 0069exact hdiv
  70. 0070cases hbudget
  71. 0071cases hbudget_witness
  72. 0072cases hbudget_witness_left
  73. 0073cases hbudget_witness_left_right
  74. 0074have hfloor_product : exists bqb_le_gap_b6_main_floor_product_order. bqb_le_gap_b6_main_floor_product_order + (n * A) = (x1)
  75. 0075specialize bertrand_floor_power_product_le_h_from_total n
  76. 0076specialize bertrand_floor_power_product_le_h_from_total s
  77. 0077specialize bertrand_floor_power_product_le_h_from_total A
  78. 0078specialize bertrand_floor_power_product_le_h_from_total x1
  79. 0079apply bertrand_floor_power_product_le_h_from_total
  80. 0080exact htotal
  81. 0081exact hfloor
  82. 0082exact hA
  83. 0083exact hH_exists_witness
  84. 0084have hfloor_to_u : exists bqb_le_gap_b6_main_floor_to_u_order. bqb_le_gap_b6_main_floor_to_u_order + (n * A) = (x2)
  85. 0085specialize le_trans (n * A)
  86. 0086specialize le_trans x1
  87. 0087specialize le_trans x2
  88. 0088apply le_trans
  89. 0089exact hfloor_product
  90. 0090exact henvelope_left
  91. 0091have hscaled_floor : exists bqb_le_gap_b6_main_scaled_floor_order. bqb_le_gap_b6_main_scaled_floor_order + ((n * A) * B) = (x2 * B)
  92. 0092specialize mul_le_mul_right (n * A)
  93. 0093specialize mul_le_mul_right x2
  94. 0094specialize mul_le_mul_right B
  95. 0095apply mul_le_mul_right
  96. 0096exact hfloor_to_u
  97. 0097have hub : exists bqb_le_gap_b6_main_u_b_order. bqb_le_gap_b6_main_u_b_order + (x2 * B) = (F)
  98. 0098specialize bertrand_four_power_product_le_of_sum_from_total q
  99. 0099specialize bertrand_four_power_product_le_of_sum_from_total x
  100. 0100specialize bertrand_four_power_product_le_of_sum_from_total n
  101. 0101specialize bertrand_four_power_product_le_of_sum_from_total B
  102. 0102specialize bertrand_four_power_product_le_of_sum_from_total x2
  103. 0103specialize bertrand_four_power_product_le_of_sum_from_total F
  104. 0104apply bertrand_four_power_product_le_of_sum_from_total
  105. 0105exact htotal
  106. 0106exact hbudget_witness_left_right_right
  107. 0107exact hB
  108. 0108exact hU_exists_witness
  109. 0109exact hF
  110. 0110specialize le_trans ((n * A) * B)
  111. 0111specialize le_trans (x2 * B)
  112. 0112specialize le_trans F
  113. 0113apply le_trans
  114. 0114exact hscaled_floor
  115. 0115exact hub