bertrand_main_inequality_nat

Exact expanded PA statement

forall n s q r A B F. (exists bqb_le_gap_b6_main_public_threshold. bqb_le_gap_b6_main_public_threshold + (16 * 32) = (n)) -> (((exists bcs_sqrt_lower_gap_b6_main_public_floor. bcs_sqrt_lower_gap_b6_main_public_floor + (s) * (s) = (n + n)) /\ exists bcs_sqrt_upper_gap_b6_main_public_floor. bcs_sqrt_upper_gap_b6_main_public_floor + S (n + n) = S (s) * S (s))) -> ((((n + n) = 3 * (q) + (r)) /\ exists bmi_remainder_gap_b6_main_public_division. bmi_remainder_gap_b6_main_public_division + S (r) = 3)) -> (exists pa_b_b6_main_public_a pa_c_b6_main_public_a. ((forall pa_i_b6_main_public_a_repeat. (exists pa_lt_b6_main_public_a_repeat_bound. pa_lt_b6_main_public_a_repeat_bound + S pa_i_b6_main_public_a_repeat = s) -> (((exists pa_h_b6_main_public_a_repeat_decoded. pa_h_b6_main_public_a_repeat_decoded + S (n + n) = S ((S (pa_i_b6_main_public_a_repeat)) * pa_c_b6_main_public_a)) /\ exists pa_q_b6_main_public_a_repeat_decoded. pa_b_b6_main_public_a = pa_q_b6_main_public_a_repeat_decoded * S ((S (pa_i_b6_main_public_a_repeat)) * pa_c_b6_main_public_a) + (n + n)))) /\ (exists pa_u_b6_main_public_a_product pa_v_b6_main_public_a_product. ((((exists pa_h_b6_main_public_a_product_start. pa_h_b6_main_public_a_product_start + S (1) = S ((S (0)) * pa_v_b6_main_public_a_product)) /\ exists pa_q_b6_main_public_a_product_start. pa_u_b6_main_public_a_product = pa_q_b6_main_public_a_product_start * S ((S (0)) * pa_v_b6_main_public_a_product) + (1))) /\ ((((exists pa_h_b6_main_public_a_product_terminal. pa_h_b6_main_public_a_product_terminal + S (A) = S ((S (s)) * pa_v_b6_main_public_a_product)) /\ exists pa_q_b6_main_public_a_product_terminal. pa_u_b6_main_public_a_product = pa_q_b6_main_public_a_product_terminal * S ((S (s)) * pa_v_b6_main_public_a_product) + (A))) /\ forall pa_i_b6_main_public_a_product. (exists pa_lt_b6_main_public_a_product_bound. pa_lt_b6_main_public_a_product_bound + S pa_i_b6_main_public_a_product = s) -> exists pa_p_b6_main_public_a_product pa_r_b6_main_public_a_product pa_s_b6_main_public_a_product. ((((exists pa_h_b6_main_public_a_product_factor. pa_h_b6_main_public_a_product_factor + S (pa_p_b6_main_public_a_product) = S ((S (pa_i_b6_main_public_a_product)) * pa_c_b6_main_public_a)) /\ exists pa_q_b6_main_public_a_product_factor. pa_b_b6_main_public_a = pa_q_b6_main_public_a_product_factor * S ((S (pa_i_b6_main_public_a_product)) * pa_c_b6_main_public_a) + (pa_p_b6_main_public_a_product))) /\ ((((exists pa_h_b6_main_public_a_product_partial. pa_h_b6_main_public_a_product_partial + S (pa_r_b6_main_public_a_product) = S ((S (pa_i_b6_main_public_a_product)) * pa_v_b6_main_public_a_product)) /\ exists pa_q_b6_main_public_a_product_partial. pa_u_b6_main_public_a_product = pa_q_b6_main_public_a_product_partial * S ((S (pa_i_b6_main_public_a_product)) * pa_v_b6_main_public_a_product) + (pa_r_b6_main_public_a_product))) /\ ((((exists pa_h_b6_main_public_a_product_successor. pa_h_b6_main_public_a_product_successor + S (pa_s_b6_main_public_a_product) = S ((S (S pa_i_b6_main_public_a_product)) * pa_v_b6_main_public_a_product)) /\ exists pa_q_b6_main_public_a_product_successor. pa_u_b6_main_public_a_product = pa_q_b6_main_public_a_product_successor * S ((S (S pa_i_b6_main_public_a_product)) * pa_v_b6_main_public_a_product) + (pa_s_b6_main_public_a_product))) /\ pa_s_b6_main_public_a_product = pa_r_b6_main_public_a_product * pa_p_b6_main_public_a_product)))))))) -> (exists pa_b_b6_main_public_b pa_c_b6_main_public_b. ((forall pa_i_b6_main_public_b_repeat. (exists pa_lt_b6_main_public_b_repeat_bound. pa_lt_b6_main_public_b_repeat_bound + S pa_i_b6_main_public_b_repeat = q) -> (((exists pa_h_b6_main_public_b_repeat_decoded. pa_h_b6_main_public_b_repeat_decoded + S (4) = S ((S (pa_i_b6_main_public_b_repeat)) * pa_c_b6_main_public_b)) /\ exists pa_q_b6_main_public_b_repeat_decoded. pa_b_b6_main_public_b = pa_q_b6_main_public_b_repeat_decoded * S ((S (pa_i_b6_main_public_b_repeat)) * pa_c_b6_main_public_b) + (4)))) /\ (exists pa_u_b6_main_public_b_product pa_v_b6_main_public_b_product. ((((exists pa_h_b6_main_public_b_product_start. pa_h_b6_main_public_b_product_start + S (1) = S ((S (0)) * pa_v_b6_main_public_b_product)) /\ exists pa_q_b6_main_public_b_product_start. pa_u_b6_main_public_b_product = pa_q_b6_main_public_b_product_start * S ((S (0)) * pa_v_b6_main_public_b_product) + (1))) /\ ((((exists pa_h_b6_main_public_b_product_terminal. pa_h_b6_main_public_b_product_terminal + S (B) = S ((S (q)) * pa_v_b6_main_public_b_product)) /\ exists pa_q_b6_main_public_b_product_terminal. pa_u_b6_main_public_b_product = pa_q_b6_main_public_b_product_terminal * S ((S (q)) * pa_v_b6_main_public_b_product) + (B))) /\ forall pa_i_b6_main_public_b_product. (exists pa_lt_b6_main_public_b_product_bound. pa_lt_b6_main_public_b_product_bound + S pa_i_b6_main_public_b_product = q) -> exists pa_p_b6_main_public_b_product pa_r_b6_main_public_b_product pa_s_b6_main_public_b_product. ((((exists pa_h_b6_main_public_b_product_factor. pa_h_b6_main_public_b_product_factor + S (pa_p_b6_main_public_b_product) = S ((S (pa_i_b6_main_public_b_product)) * pa_c_b6_main_public_b)) /\ exists pa_q_b6_main_public_b_product_factor. pa_b_b6_main_public_b = pa_q_b6_main_public_b_product_factor * S ((S (pa_i_b6_main_public_b_product)) * pa_c_b6_main_public_b) + (pa_p_b6_main_public_b_product))) /\ ((((exists pa_h_b6_main_public_b_product_partial. pa_h_b6_main_public_b_product_partial + S (pa_r_b6_main_public_b_product) = S ((S (pa_i_b6_main_public_b_product)) * pa_v_b6_main_public_b_product)) /\ exists pa_q_b6_main_public_b_product_partial. pa_u_b6_main_public_b_product = pa_q_b6_main_public_b_product_partial * S ((S (pa_i_b6_main_public_b_product)) * pa_v_b6_main_public_b_product) + (pa_r_b6_main_public_b_product))) /\ ((((exists pa_h_b6_main_public_b_product_successor. pa_h_b6_main_public_b_product_successor + S (pa_s_b6_main_public_b_product) = S ((S (S pa_i_b6_main_public_b_product)) * pa_v_b6_main_public_b_product)) /\ exists pa_q_b6_main_public_b_product_successor. pa_u_b6_main_public_b_product = pa_q_b6_main_public_b_product_successor * S ((S (S pa_i_b6_main_public_b_product)) * pa_v_b6_main_public_b_product) + (pa_s_b6_main_public_b_product))) /\ pa_s_b6_main_public_b_product = pa_r_b6_main_public_b_product * pa_p_b6_main_public_b_product)))))))) -> (exists pa_b_b6_main_public_f pa_c_b6_main_public_f. ((forall pa_i_b6_main_public_f_repeat. (exists pa_lt_b6_main_public_f_repeat_bound. pa_lt_b6_main_public_f_repeat_bound + S pa_i_b6_main_public_f_repeat = n) -> (((exists pa_h_b6_main_public_f_repeat_decoded. pa_h_b6_main_public_f_repeat_decoded + S (4) = S ((S (pa_i_b6_main_public_f_repeat)) * pa_c_b6_main_public_f)) /\ exists pa_q_b6_main_public_f_repeat_decoded. pa_b_b6_main_public_f = pa_q_b6_main_public_f_repeat_decoded * S ((S (pa_i_b6_main_public_f_repeat)) * pa_c_b6_main_public_f) + (4)))) /\ (exists pa_u_b6_main_public_f_product pa_v_b6_main_public_f_product. ((((exists pa_h_b6_main_public_f_product_start. pa_h_b6_main_public_f_product_start + S (1) = S ((S (0)) * pa_v_b6_main_public_f_product)) /\ exists pa_q_b6_main_public_f_product_start. pa_u_b6_main_public_f_product = pa_q_b6_main_public_f_product_start * S ((S (0)) * pa_v_b6_main_public_f_product) + (1))) /\ ((((exists pa_h_b6_main_public_f_product_terminal. pa_h_b6_main_public_f_product_terminal + S (F) = S ((S (n)) * pa_v_b6_main_public_f_product)) /\ exists pa_q_b6_main_public_f_product_terminal. pa_u_b6_main_public_f_product = pa_q_b6_main_public_f_product_terminal * S ((S (n)) * pa_v_b6_main_public_f_product) + (F))) /\ forall pa_i_b6_main_public_f_product. (exists pa_lt_b6_main_public_f_product_bound. pa_lt_b6_main_public_f_product_bound + S pa_i_b6_main_public_f_product = n) -> exists pa_p_b6_main_public_f_product pa_r_b6_main_public_f_product pa_s_b6_main_public_f_product. ((((exists pa_h_b6_main_public_f_product_factor. pa_h_b6_main_public_f_product_factor + S (pa_p_b6_main_public_f_product) = S ((S (pa_i_b6_main_public_f_product)) * pa_c_b6_main_public_f)) /\ exists pa_q_b6_main_public_f_product_factor. pa_b_b6_main_public_f = pa_q_b6_main_public_f_product_factor * S ((S (pa_i_b6_main_public_f_product)) * pa_c_b6_main_public_f) + (pa_p_b6_main_public_f_product))) /\ ((((exists pa_h_b6_main_public_f_product_partial. pa_h_b6_main_public_f_product_partial + S (pa_r_b6_main_public_f_product) = S ((S (pa_i_b6_main_public_f_product)) * pa_v_b6_main_public_f_product)) /\ exists pa_q_b6_main_public_f_product_partial. pa_u_b6_main_public_f_product = pa_q_b6_main_public_f_product_partial * S ((S (pa_i_b6_main_public_f_product)) * pa_v_b6_main_public_f_product) + (pa_r_b6_main_public_f_product))) /\ ((((exists pa_h_b6_main_public_f_product_successor. pa_h_b6_main_public_f_product_successor + S (pa_s_b6_main_public_f_product) = S ((S (S pa_i_b6_main_public_f_product)) * pa_v_b6_main_public_f_product)) /\ exists pa_q_b6_main_public_f_product_successor. pa_u_b6_main_public_f_product = pa_q_b6_main_public_f_product_successor * S ((S (S pa_i_b6_main_public_f_product)) * pa_v_b6_main_public_f_product) + (pa_s_b6_main_public_f_product))) /\ pa_s_b6_main_public_f_product = pa_r_b6_main_public_f_product * pa_p_b6_main_public_f_product)))))))) -> (exists bqb_le_gap_b6_main_public_result. bqb_le_gap_b6_main_public_result + (n * A * B) = (F))