bertrand_four_power_product_le_of_sum_from_total

Exact expanded PA statement

forall q e n B U F. (forall bpt_a_b6_four_product bpt_e_b6_four_product. exists bpt_x_b6_four_product. (exists ff_b_bpt_value_b6_four_product ff_c_bpt_value_b6_four_product. ((forall ff_i_bpt_value_b6_four_product_repeat. (exists ff_lt_bpt_value_b6_four_product_repeat_bound. ff_lt_bpt_value_b6_four_product_repeat_bound + S ff_i_bpt_value_b6_four_product_repeat = bpt_e_b6_four_product) -> (((exists ff_h_bpt_value_b6_four_product_repeat_decoded. ff_h_bpt_value_b6_four_product_repeat_decoded + S (bpt_a_b6_four_product) = S ((S (ff_i_bpt_value_b6_four_product_repeat)) * ff_c_bpt_value_b6_four_product)) /\ exists ff_q_bpt_value_b6_four_product_repeat_decoded. ff_b_bpt_value_b6_four_product = ff_q_bpt_value_b6_four_product_repeat_decoded * S ((S (ff_i_bpt_value_b6_four_product_repeat)) * ff_c_bpt_value_b6_four_product) + (bpt_a_b6_four_product)))) /\ (exists ff_u_bpt_value_b6_four_product_product ff_v_bpt_value_b6_four_product_product. ((((exists ff_h_bpt_value_b6_four_product_product_start. ff_h_bpt_value_b6_four_product_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_b6_four_product_product)) /\ exists ff_q_bpt_value_b6_four_product_product_start. ff_u_bpt_value_b6_four_product_product = ff_q_bpt_value_b6_four_product_product_start * S ((S (0)) * ff_v_bpt_value_b6_four_product_product) + (1))) /\ ((((exists ff_h_bpt_value_b6_four_product_product_terminal. ff_h_bpt_value_b6_four_product_product_terminal + S (bpt_x_b6_four_product) = S ((S (bpt_e_b6_four_product)) * ff_v_bpt_value_b6_four_product_product)) /\ exists ff_q_bpt_value_b6_four_product_product_terminal. ff_u_bpt_value_b6_four_product_product = ff_q_bpt_value_b6_four_product_product_terminal * S ((S (bpt_e_b6_four_product)) * ff_v_bpt_value_b6_four_product_product) + (bpt_x_b6_four_product))) /\ forall ff_i_bpt_value_b6_four_product_product. (exists ff_lt_bpt_value_b6_four_product_product_bound. ff_lt_bpt_value_b6_four_product_product_bound + S ff_i_bpt_value_b6_four_product_product = bpt_e_b6_four_product) -> exists ff_p_bpt_value_b6_four_product_product ff_r_bpt_value_b6_four_product_product ff_s_bpt_value_b6_four_product_product. ((((exists ff_h_bpt_value_b6_four_product_product_factor. ff_h_bpt_value_b6_four_product_product_factor + S (ff_p_bpt_value_b6_four_product_product) = S ((S (ff_i_bpt_value_b6_four_product_product)) * ff_c_bpt_value_b6_four_product)) /\ exists ff_q_bpt_value_b6_four_product_product_factor. ff_b_bpt_value_b6_four_product = ff_q_bpt_value_b6_four_product_product_factor * S ((S (ff_i_bpt_value_b6_four_product_product)) * ff_c_bpt_value_b6_four_product) + (ff_p_bpt_value_b6_four_product_product))) /\ ((((exists ff_h_bpt_value_b6_four_product_product_partial. ff_h_bpt_value_b6_four_product_product_partial + S (ff_r_bpt_value_b6_four_product_product) = S ((S (ff_i_bpt_value_b6_four_product_product)) * ff_v_bpt_value_b6_four_product_product)) /\ exists ff_q_bpt_value_b6_four_product_product_partial. ff_u_bpt_value_b6_four_product_product = ff_q_bpt_value_b6_four_product_product_partial * S ((S (ff_i_bpt_value_b6_four_product_product)) * ff_v_bpt_value_b6_four_product_product) + (ff_r_bpt_value_b6_four_product_product))) /\ ((((exists ff_h_bpt_value_b6_four_product_product_successor. ff_h_bpt_value_b6_four_product_product_successor + S (ff_s_bpt_value_b6_four_product_product) = S ((S (S ff_i_bpt_value_b6_four_product_product)) * ff_v_bpt_value_b6_four_product_product)) /\ exists ff_q_bpt_value_b6_four_product_product_successor. ff_u_bpt_value_b6_four_product_product = ff_q_bpt_value_b6_four_product_product_successor * S ((S (S ff_i_bpt_value_b6_four_product_product)) * ff_v_bpt_value_b6_four_product_product) + (ff_s_bpt_value_b6_four_product_product))) /\ ff_s_bpt_value_b6_four_product_product = ff_r_bpt_value_b6_four_product_product * ff_p_bpt_value_b6_four_product_product))))))))) -> (exists bqb_le_gap_b6_four_product_sum. bqb_le_gap_b6_four_product_sum + (q + e) = (n)) -> (exists pa_b_b6_four_product_q pa_c_b6_four_product_q. ((forall pa_i_b6_four_product_q_repeat. (exists pa_lt_b6_four_product_q_repeat_bound. pa_lt_b6_four_product_q_repeat_bound + S pa_i_b6_four_product_q_repeat = q) -> (((exists pa_h_b6_four_product_q_repeat_decoded. pa_h_b6_four_product_q_repeat_decoded + S (4) = S ((S (pa_i_b6_four_product_q_repeat)) * pa_c_b6_four_product_q)) /\ exists pa_q_b6_four_product_q_repeat_decoded. pa_b_b6_four_product_q = pa_q_b6_four_product_q_repeat_decoded * S ((S (pa_i_b6_four_product_q_repeat)) * pa_c_b6_four_product_q) + (4)))) /\ (exists pa_u_b6_four_product_q_product pa_v_b6_four_product_q_product. ((((exists pa_h_b6_four_product_q_product_start. pa_h_b6_four_product_q_product_start + S (1) = S ((S (0)) * pa_v_b6_four_product_q_product)) /\ exists pa_q_b6_four_product_q_product_start. pa_u_b6_four_product_q_product = pa_q_b6_four_product_q_product_start * S ((S (0)) * pa_v_b6_four_product_q_product) + (1))) /\ ((((exists pa_h_b6_four_product_q_product_terminal. pa_h_b6_four_product_q_product_terminal + S (B) = S ((S (q)) * pa_v_b6_four_product_q_product)) /\ exists pa_q_b6_four_product_q_product_terminal. pa_u_b6_four_product_q_product = pa_q_b6_four_product_q_product_terminal * S ((S (q)) * pa_v_b6_four_product_q_product) + (B))) /\ forall pa_i_b6_four_product_q_product. (exists pa_lt_b6_four_product_q_product_bound. pa_lt_b6_four_product_q_product_bound + S pa_i_b6_four_product_q_product = q) -> exists pa_p_b6_four_product_q_product pa_r_b6_four_product_q_product pa_s_b6_four_product_q_product. ((((exists pa_h_b6_four_product_q_product_factor. pa_h_b6_four_product_q_product_factor + S (pa_p_b6_four_product_q_product) = S ((S (pa_i_b6_four_product_q_product)) * pa_c_b6_four_product_q)) /\ exists pa_q_b6_four_product_q_product_factor. pa_b_b6_four_product_q = pa_q_b6_four_product_q_product_factor * S ((S (pa_i_b6_four_product_q_product)) * pa_c_b6_four_product_q) + (pa_p_b6_four_product_q_product))) /\ ((((exists pa_h_b6_four_product_q_product_partial. pa_h_b6_four_product_q_product_partial + S (pa_r_b6_four_product_q_product) = S ((S (pa_i_b6_four_product_q_product)) * pa_v_b6_four_product_q_product)) /\ exists pa_q_b6_four_product_q_product_partial. pa_u_b6_four_product_q_product = pa_q_b6_four_product_q_product_partial * S ((S (pa_i_b6_four_product_q_product)) * pa_v_b6_four_product_q_product) + (pa_r_b6_four_product_q_product))) /\ ((((exists pa_h_b6_four_product_q_product_successor. pa_h_b6_four_product_q_product_successor + S (pa_s_b6_four_product_q_product) = S ((S (S pa_i_b6_four_product_q_product)) * pa_v_b6_four_product_q_product)) /\ exists pa_q_b6_four_product_q_product_successor. pa_u_b6_four_product_q_product = pa_q_b6_four_product_q_product_successor * S ((S (S pa_i_b6_four_product_q_product)) * pa_v_b6_four_product_q_product) + (pa_s_b6_four_product_q_product))) /\ pa_s_b6_four_product_q_product = pa_r_b6_four_product_q_product * pa_p_b6_four_product_q_product)))))))) -> (exists pa_b_b6_four_product_e pa_c_b6_four_product_e. ((forall pa_i_b6_four_product_e_repeat. (exists pa_lt_b6_four_product_e_repeat_bound. pa_lt_b6_four_product_e_repeat_bound + S pa_i_b6_four_product_e_repeat = e) -> (((exists pa_h_b6_four_product_e_repeat_decoded. pa_h_b6_four_product_e_repeat_decoded + S (4) = S ((S (pa_i_b6_four_product_e_repeat)) * pa_c_b6_four_product_e)) /\ exists pa_q_b6_four_product_e_repeat_decoded. pa_b_b6_four_product_e = pa_q_b6_four_product_e_repeat_decoded * S ((S (pa_i_b6_four_product_e_repeat)) * pa_c_b6_four_product_e) + (4)))) /\ (exists pa_u_b6_four_product_e_product pa_v_b6_four_product_e_product. ((((exists pa_h_b6_four_product_e_product_start. pa_h_b6_four_product_e_product_start + S (1) = S ((S (0)) * pa_v_b6_four_product_e_product)) /\ exists pa_q_b6_four_product_e_product_start. pa_u_b6_four_product_e_product = pa_q_b6_four_product_e_product_start * S ((S (0)) * pa_v_b6_four_product_e_product) + (1))) /\ ((((exists pa_h_b6_four_product_e_product_terminal. pa_h_b6_four_product_e_product_terminal + S (U) = S ((S (e)) * pa_v_b6_four_product_e_product)) /\ exists pa_q_b6_four_product_e_product_terminal. pa_u_b6_four_product_e_product = pa_q_b6_four_product_e_product_terminal * S ((S (e)) * pa_v_b6_four_product_e_product) + (U))) /\ forall pa_i_b6_four_product_e_product. (exists pa_lt_b6_four_product_e_product_bound. pa_lt_b6_four_product_e_product_bound + S pa_i_b6_four_product_e_product = e) -> exists pa_p_b6_four_product_e_product pa_r_b6_four_product_e_product pa_s_b6_four_product_e_product. ((((exists pa_h_b6_four_product_e_product_factor. pa_h_b6_four_product_e_product_factor + S (pa_p_b6_four_product_e_product) = S ((S (pa_i_b6_four_product_e_product)) * pa_c_b6_four_product_e)) /\ exists pa_q_b6_four_product_e_product_factor. pa_b_b6_four_product_e = pa_q_b6_four_product_e_product_factor * S ((S (pa_i_b6_four_product_e_product)) * pa_c_b6_four_product_e) + (pa_p_b6_four_product_e_product))) /\ ((((exists pa_h_b6_four_product_e_product_partial. pa_h_b6_four_product_e_product_partial + S (pa_r_b6_four_product_e_product) = S ((S (pa_i_b6_four_product_e_product)) * pa_v_b6_four_product_e_product)) /\ exists pa_q_b6_four_product_e_product_partial. pa_u_b6_four_product_e_product = pa_q_b6_four_product_e_product_partial * S ((S (pa_i_b6_four_product_e_product)) * pa_v_b6_four_product_e_product) + (pa_r_b6_four_product_e_product))) /\ ((((exists pa_h_b6_four_product_e_product_successor. pa_h_b6_four_product_e_product_successor + S (pa_s_b6_four_product_e_product) = S ((S (S pa_i_b6_four_product_e_product)) * pa_v_b6_four_product_e_product)) /\ exists pa_q_b6_four_product_e_product_successor. pa_u_b6_four_product_e_product = pa_q_b6_four_product_e_product_successor * S ((S (S pa_i_b6_four_product_e_product)) * pa_v_b6_four_product_e_product) + (pa_s_b6_four_product_e_product))) /\ pa_s_b6_four_product_e_product = pa_r_b6_four_product_e_product * pa_p_b6_four_product_e_product)))))))) -> (exists pa_b_b6_four_product_n pa_c_b6_four_product_n. ((forall pa_i_b6_four_product_n_repeat. (exists pa_lt_b6_four_product_n_repeat_bound. pa_lt_b6_four_product_n_repeat_bound + S pa_i_b6_four_product_n_repeat = n) -> (((exists pa_h_b6_four_product_n_repeat_decoded. pa_h_b6_four_product_n_repeat_decoded + S (4) = S ((S (pa_i_b6_four_product_n_repeat)) * pa_c_b6_four_product_n)) /\ exists pa_q_b6_four_product_n_repeat_decoded. pa_b_b6_four_product_n = pa_q_b6_four_product_n_repeat_decoded * S ((S (pa_i_b6_four_product_n_repeat)) * pa_c_b6_four_product_n) + (4)))) /\ (exists pa_u_b6_four_product_n_product pa_v_b6_four_product_n_product. ((((exists pa_h_b6_four_product_n_product_start. pa_h_b6_four_product_n_product_start + S (1) = S ((S (0)) * pa_v_b6_four_product_n_product)) /\ exists pa_q_b6_four_product_n_product_start. pa_u_b6_four_product_n_product = pa_q_b6_four_product_n_product_start * S ((S (0)) * pa_v_b6_four_product_n_product) + (1))) /\ ((((exists pa_h_b6_four_product_n_product_terminal. pa_h_b6_four_product_n_product_terminal + S (F) = S ((S (n)) * pa_v_b6_four_product_n_product)) /\ exists pa_q_b6_four_product_n_product_terminal. pa_u_b6_four_product_n_product = pa_q_b6_four_product_n_product_terminal * S ((S (n)) * pa_v_b6_four_product_n_product) + (F))) /\ forall pa_i_b6_four_product_n_product. (exists pa_lt_b6_four_product_n_product_bound. pa_lt_b6_four_product_n_product_bound + S pa_i_b6_four_product_n_product = n) -> exists pa_p_b6_four_product_n_product pa_r_b6_four_product_n_product pa_s_b6_four_product_n_product. ((((exists pa_h_b6_four_product_n_product_factor. pa_h_b6_four_product_n_product_factor + S (pa_p_b6_four_product_n_product) = S ((S (pa_i_b6_four_product_n_product)) * pa_c_b6_four_product_n)) /\ exists pa_q_b6_four_product_n_product_factor. pa_b_b6_four_product_n = pa_q_b6_four_product_n_product_factor * S ((S (pa_i_b6_four_product_n_product)) * pa_c_b6_four_product_n) + (pa_p_b6_four_product_n_product))) /\ ((((exists pa_h_b6_four_product_n_product_partial. pa_h_b6_four_product_n_product_partial + S (pa_r_b6_four_product_n_product) = S ((S (pa_i_b6_four_product_n_product)) * pa_v_b6_four_product_n_product)) /\ exists pa_q_b6_four_product_n_product_partial. pa_u_b6_four_product_n_product = pa_q_b6_four_product_n_product_partial * S ((S (pa_i_b6_four_product_n_product)) * pa_v_b6_four_product_n_product) + (pa_r_b6_four_product_n_product))) /\ ((((exists pa_h_b6_four_product_n_product_successor. pa_h_b6_four_product_n_product_successor + S (pa_s_b6_four_product_n_product) = S ((S (S pa_i_b6_four_product_n_product)) * pa_v_b6_four_product_n_product)) /\ exists pa_q_b6_four_product_n_product_successor. pa_u_b6_four_product_n_product = pa_q_b6_four_product_n_product_successor * S ((S (S pa_i_b6_four_product_n_product)) * pa_v_b6_four_product_n_product) + (pa_s_b6_four_product_n_product))) /\ pa_s_b6_four_product_n_product = pa_r_b6_four_product_n_product * pa_p_b6_four_product_n_product)))))))) -> (exists bqb_le_gap_b6_four_product_result. bqb_le_gap_b6_four_product_result + (U * B) = (F))