prime_count_chebyshev_bounds

Exact expanded first-order arithmetic statement

forall N ell k. (exists pc_le_cheb_full_positive. pc_le_cheb_full_positive + (2) = (N)) -> ((((N) = 0 /\ (ell) = 1) \/ exists ff_exponent_bl_pc_cheb_full_length ff_lower_bl_pc_cheb_full_length ff_upper_bl_pc_cheb_full_length. (((ell) = S ff_exponent_bl_pc_cheb_full_length) /\ ((exists ff_positive_bl_pc_cheb_full_length. ff_positive_bl_pc_cheb_full_length + 1 = (N)) /\ ((exists pa_b_bl_pc_cheb_full_length_lower pa_c_bl_pc_cheb_full_length_lower. ((forall pa_i_bl_pc_cheb_full_length_lower_repeat. (exists pa_lt_bl_pc_cheb_full_length_lower_repeat_bound. pa_lt_bl_pc_cheb_full_length_lower_repeat_bound + S pa_i_bl_pc_cheb_full_length_lower_repeat = ff_exponent_bl_pc_cheb_full_length) -> (((exists pa_h_bl_pc_cheb_full_length_lower_repeat_decoded. pa_h_bl_pc_cheb_full_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_pc_cheb_full_length_lower_repeat)) * pa_c_bl_pc_cheb_full_length_lower)) /\ exists pa_q_bl_pc_cheb_full_length_lower_repeat_decoded. pa_b_bl_pc_cheb_full_length_lower = pa_q_bl_pc_cheb_full_length_lower_repeat_decoded * S ((S (pa_i_bl_pc_cheb_full_length_lower_repeat)) * pa_c_bl_pc_cheb_full_length_lower) + (2)))) /\ (exists pa_u_bl_pc_cheb_full_length_lower_product pa_v_bl_pc_cheb_full_length_lower_product. ((((exists pa_h_bl_pc_cheb_full_length_lower_product_start. pa_h_bl_pc_cheb_full_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_pc_cheb_full_length_lower_product)) /\ exists pa_q_bl_pc_cheb_full_length_lower_product_start. pa_u_bl_pc_cheb_full_length_lower_product = pa_q_bl_pc_cheb_full_length_lower_product_start * S ((S (0)) * pa_v_bl_pc_cheb_full_length_lower_product) + (1))) /\ ((((exists pa_h_bl_pc_cheb_full_length_lower_product_terminal. pa_h_bl_pc_cheb_full_length_lower_product_terminal + S (ff_lower_bl_pc_cheb_full_length) = S ((S (ff_exponent_bl_pc_cheb_full_length)) * pa_v_bl_pc_cheb_full_length_lower_product)) /\ exists pa_q_bl_pc_cheb_full_length_lower_product_terminal. pa_u_bl_pc_cheb_full_length_lower_product = pa_q_bl_pc_cheb_full_length_lower_product_terminal * S ((S (ff_exponent_bl_pc_cheb_full_length)) * pa_v_bl_pc_cheb_full_length_lower_product) + (ff_lower_bl_pc_cheb_full_length))) /\ forall pa_i_bl_pc_cheb_full_length_lower_product. (exists pa_lt_bl_pc_cheb_full_length_lower_product_bound. pa_lt_bl_pc_cheb_full_length_lower_product_bound + S pa_i_bl_pc_cheb_full_length_lower_product = ff_exponent_bl_pc_cheb_full_length) -> exists pa_p_bl_pc_cheb_full_length_lower_product pa_r_bl_pc_cheb_full_length_lower_product pa_s_bl_pc_cheb_full_length_lower_product. ((((exists pa_h_bl_pc_cheb_full_length_lower_product_factor. pa_h_bl_pc_cheb_full_length_lower_product_factor + S (pa_p_bl_pc_cheb_full_length_lower_product) = S ((S (pa_i_bl_pc_cheb_full_length_lower_product)) * pa_c_bl_pc_cheb_full_length_lower)) /\ exists pa_q_bl_pc_cheb_full_length_lower_product_factor. pa_b_bl_pc_cheb_full_length_lower = pa_q_bl_pc_cheb_full_length_lower_product_factor * S ((S (pa_i_bl_pc_cheb_full_length_lower_product)) * pa_c_bl_pc_cheb_full_length_lower) + (pa_p_bl_pc_cheb_full_length_lower_product))) /\ ((((exists pa_h_bl_pc_cheb_full_length_lower_product_partial. pa_h_bl_pc_cheb_full_length_lower_product_partial + S (pa_r_bl_pc_cheb_full_length_lower_product) = S ((S (pa_i_bl_pc_cheb_full_length_lower_product)) * pa_v_bl_pc_cheb_full_length_lower_product)) /\ exists pa_q_bl_pc_cheb_full_length_lower_product_partial. pa_u_bl_pc_cheb_full_length_lower_product = pa_q_bl_pc_cheb_full_length_lower_product_partial * S ((S (pa_i_bl_pc_cheb_full_length_lower_product)) * pa_v_bl_pc_cheb_full_length_lower_product) + (pa_r_bl_pc_cheb_full_length_lower_product))) /\ ((((exists pa_h_bl_pc_cheb_full_length_lower_product_successor. pa_h_bl_pc_cheb_full_length_lower_product_successor + S (pa_s_bl_pc_cheb_full_length_lower_product) = S ((S (S pa_i_bl_pc_cheb_full_length_lower_product)) * pa_v_bl_pc_cheb_full_length_lower_product)) /\ exists pa_q_bl_pc_cheb_full_length_lower_product_successor. pa_u_bl_pc_cheb_full_length_lower_product = pa_q_bl_pc_cheb_full_length_lower_product_successor * S ((S (S pa_i_bl_pc_cheb_full_length_lower_product)) * pa_v_bl_pc_cheb_full_length_lower_product) + (pa_s_bl_pc_cheb_full_length_lower_product))) /\ pa_s_bl_pc_cheb_full_length_lower_product = pa_r_bl_pc_cheb_full_length_lower_product * pa_p_bl_pc_cheb_full_length_lower_product)))))))) /\ ((exists pa_b_bl_pc_cheb_full_length_upper pa_c_bl_pc_cheb_full_length_upper. ((forall pa_i_bl_pc_cheb_full_length_upper_repeat. (exists pa_lt_bl_pc_cheb_full_length_upper_repeat_bound. pa_lt_bl_pc_cheb_full_length_upper_repeat_bound + S pa_i_bl_pc_cheb_full_length_upper_repeat = ell) -> (((exists pa_h_bl_pc_cheb_full_length_upper_repeat_decoded. pa_h_bl_pc_cheb_full_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_pc_cheb_full_length_upper_repeat)) * pa_c_bl_pc_cheb_full_length_upper)) /\ exists pa_q_bl_pc_cheb_full_length_upper_repeat_decoded. pa_b_bl_pc_cheb_full_length_upper = pa_q_bl_pc_cheb_full_length_upper_repeat_decoded * S ((S (pa_i_bl_pc_cheb_full_length_upper_repeat)) * pa_c_bl_pc_cheb_full_length_upper) + (2)))) /\ (exists pa_u_bl_pc_cheb_full_length_upper_product pa_v_bl_pc_cheb_full_length_upper_product. ((((exists pa_h_bl_pc_cheb_full_length_upper_product_start. pa_h_bl_pc_cheb_full_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_pc_cheb_full_length_upper_product)) /\ exists pa_q_bl_pc_cheb_full_length_upper_product_start. pa_u_bl_pc_cheb_full_length_upper_product = pa_q_bl_pc_cheb_full_length_upper_product_start * S ((S (0)) * pa_v_bl_pc_cheb_full_length_upper_product) + (1))) /\ ((((exists pa_h_bl_pc_cheb_full_length_upper_product_terminal. pa_h_bl_pc_cheb_full_length_upper_product_terminal + S (ff_upper_bl_pc_cheb_full_length) = S ((S (ell)) * pa_v_bl_pc_cheb_full_length_upper_product)) /\ exists pa_q_bl_pc_cheb_full_length_upper_product_terminal. pa_u_bl_pc_cheb_full_length_upper_product = pa_q_bl_pc_cheb_full_length_upper_product_terminal * S ((S (ell)) * pa_v_bl_pc_cheb_full_length_upper_product) + (ff_upper_bl_pc_cheb_full_length))) /\ forall pa_i_bl_pc_cheb_full_length_upper_product. (exists pa_lt_bl_pc_cheb_full_length_upper_product_bound. pa_lt_bl_pc_cheb_full_length_upper_product_bound + S pa_i_bl_pc_cheb_full_length_upper_product = ell) -> exists pa_p_bl_pc_cheb_full_length_upper_product pa_r_bl_pc_cheb_full_length_upper_product pa_s_bl_pc_cheb_full_length_upper_product. ((((exists pa_h_bl_pc_cheb_full_length_upper_product_factor. pa_h_bl_pc_cheb_full_length_upper_product_factor + S (pa_p_bl_pc_cheb_full_length_upper_product) = S ((S (pa_i_bl_pc_cheb_full_length_upper_product)) * pa_c_bl_pc_cheb_full_length_upper)) /\ exists pa_q_bl_pc_cheb_full_length_upper_product_factor. pa_b_bl_pc_cheb_full_length_upper = pa_q_bl_pc_cheb_full_length_upper_product_factor * S ((S (pa_i_bl_pc_cheb_full_length_upper_product)) * pa_c_bl_pc_cheb_full_length_upper) + (pa_p_bl_pc_cheb_full_length_upper_product))) /\ ((((exists pa_h_bl_pc_cheb_full_length_upper_product_partial. pa_h_bl_pc_cheb_full_length_upper_product_partial + S (pa_r_bl_pc_cheb_full_length_upper_product) = S ((S (pa_i_bl_pc_cheb_full_length_upper_product)) * pa_v_bl_pc_cheb_full_length_upper_product)) /\ exists pa_q_bl_pc_cheb_full_length_upper_product_partial. pa_u_bl_pc_cheb_full_length_upper_product = pa_q_bl_pc_cheb_full_length_upper_product_partial * S ((S (pa_i_bl_pc_cheb_full_length_upper_product)) * pa_v_bl_pc_cheb_full_length_upper_product) + (pa_r_bl_pc_cheb_full_length_upper_product))) /\ ((((exists pa_h_bl_pc_cheb_full_length_upper_product_successor. pa_h_bl_pc_cheb_full_length_upper_product_successor + S (pa_s_bl_pc_cheb_full_length_upper_product) = S ((S (S pa_i_bl_pc_cheb_full_length_upper_product)) * pa_v_bl_pc_cheb_full_length_upper_product)) /\ exists pa_q_bl_pc_cheb_full_length_upper_product_successor. pa_u_bl_pc_cheb_full_length_upper_product = pa_q_bl_pc_cheb_full_length_upper_product_successor * S ((S (S pa_i_bl_pc_cheb_full_length_upper_product)) * pa_v_bl_pc_cheb_full_length_upper_product) + (pa_s_bl_pc_cheb_full_length_upper_product))) /\ pa_s_bl_pc_cheb_full_length_upper_product = pa_r_bl_pc_cheb_full_length_upper_product * pa_p_bl_pc_cheb_full_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_pc_cheb_full_length. ff_lower_gap_bl_pc_cheb_full_length + (ff_lower_bl_pc_cheb_full_length) = (N)) /\ (exists ff_upper_gap_bl_pc_cheb_full_length. ff_upper_gap_bl_pc_cheb_full_length + S (N) = (ff_upper_bl_pc_cheb_full_length))))))))) -> (exists pc_code_cheb_full_count pc_scale_cheb_full_count. (forall pc_index_cheb_full_count_mask. (exists pc_lt_cheb_full_count_mask_bound. pc_lt_cheb_full_count_mask_bound + S (pc_index_cheb_full_count_mask) = (N)) -> exists pc_bit_cheb_full_count_mask. (((exists fs_h_pc_cheb_full_count_mask_entry. fs_h_pc_cheb_full_count_mask_entry + S (pc_bit_cheb_full_count_mask) = S ((S (pc_index_cheb_full_count_mask)) * pc_scale_cheb_full_count)) /\ exists fs_q_pc_cheb_full_count_mask_entry. pc_code_cheb_full_count = fs_q_pc_cheb_full_count_mask_entry * S ((S (pc_index_cheb_full_count_mask)) * pc_scale_cheb_full_count) + (pc_bit_cheb_full_count_mask))) /\ (((((~(S (pc_index_cheb_full_count_mask) = 1) /\ forall bpr_left_pc_cheb_full_count_mask_choice_prime bpr_right_pc_cheb_full_count_mask_choice_prime. S (pc_index_cheb_full_count_mask) = bpr_left_pc_cheb_full_count_mask_choice_prime * bpr_right_pc_cheb_full_count_mask_choice_prime -> bpr_left_pc_cheb_full_count_mask_choice_prime = 1 \/ bpr_right_pc_cheb_full_count_mask_choice_prime = 1)) /\ pc_bit_cheb_full_count_mask = 1) \/ (~((~(S (pc_index_cheb_full_count_mask) = 1) /\ forall bpr_left_pc_cheb_full_count_mask_choice_prime bpr_right_pc_cheb_full_count_mask_choice_prime. S (pc_index_cheb_full_count_mask) = bpr_left_pc_cheb_full_count_mask_choice_prime * bpr_right_pc_cheb_full_count_mask_choice_prime -> bpr_left_pc_cheb_full_count_mask_choice_prime = 1 \/ bpr_right_pc_cheb_full_count_mask_choice_prime = 1)) /\ pc_bit_cheb_full_count_mask = 0)))) /\ (exists fs_u_pc_cheb_full_count_sum fs_v_pc_cheb_full_count_sum. ((((exists fs_h_pc_cheb_full_count_sum_body_start. fs_h_pc_cheb_full_count_sum_body_start + S (0) = S ((S (0)) * fs_v_pc_cheb_full_count_sum)) /\ exists fs_q_pc_cheb_full_count_sum_body_start. fs_u_pc_cheb_full_count_sum = fs_q_pc_cheb_full_count_sum_body_start * S ((S (0)) * fs_v_pc_cheb_full_count_sum) + (0))) /\ ((((exists fs_h_pc_cheb_full_count_sum_body_terminal. fs_h_pc_cheb_full_count_sum_body_terminal + S (k) = S ((S (N)) * fs_v_pc_cheb_full_count_sum)) /\ exists fs_q_pc_cheb_full_count_sum_body_terminal. fs_u_pc_cheb_full_count_sum = fs_q_pc_cheb_full_count_sum_body_terminal * S ((S (N)) * fs_v_pc_cheb_full_count_sum) + (k))) /\ forall fs_i_pc_cheb_full_count_sum_body_steps. (exists fs_lt_pc_cheb_full_count_sum_body_steps_bound. fs_lt_pc_cheb_full_count_sum_body_steps_bound + S fs_i_pc_cheb_full_count_sum_body_steps = N) -> exists fs_a_pc_cheb_full_count_sum_body_steps fs_r_pc_cheb_full_count_sum_body_steps fs_s_pc_cheb_full_count_sum_body_steps. ((((exists fs_h_pc_cheb_full_count_sum_body_steps_summand. fs_h_pc_cheb_full_count_sum_body_steps_summand + S (fs_a_pc_cheb_full_count_sum_body_steps) = S ((S (fs_i_pc_cheb_full_count_sum_body_steps)) * pc_scale_cheb_full_count)) /\ exists fs_q_pc_cheb_full_count_sum_body_steps_summand. pc_code_cheb_full_count = fs_q_pc_cheb_full_count_sum_body_steps_summand * S ((S (fs_i_pc_cheb_full_count_sum_body_steps)) * pc_scale_cheb_full_count) + (fs_a_pc_cheb_full_count_sum_body_steps))) /\ ((((exists fs_h_pc_cheb_full_count_sum_body_steps_partial. fs_h_pc_cheb_full_count_sum_body_steps_partial + S (fs_r_pc_cheb_full_count_sum_body_steps) = S ((S (fs_i_pc_cheb_full_count_sum_body_steps)) * fs_v_pc_cheb_full_count_sum)) /\ exists fs_q_pc_cheb_full_count_sum_body_steps_partial. fs_u_pc_cheb_full_count_sum = fs_q_pc_cheb_full_count_sum_body_steps_partial * S ((S (fs_i_pc_cheb_full_count_sum_body_steps)) * fs_v_pc_cheb_full_count_sum) + (fs_r_pc_cheb_full_count_sum_body_steps))) /\ ((((exists fs_h_pc_cheb_full_count_sum_body_steps_successor. fs_h_pc_cheb_full_count_sum_body_steps_successor + S (fs_s_pc_cheb_full_count_sum_body_steps) = S ((S (S fs_i_pc_cheb_full_count_sum_body_steps)) * fs_v_pc_cheb_full_count_sum)) /\ exists fs_q_pc_cheb_full_count_sum_body_steps_successor. fs_u_pc_cheb_full_count_sum = fs_q_pc_cheb_full_count_sum_body_steps_successor * S ((S (S fs_i_pc_cheb_full_count_sum_body_steps)) * fs_v_pc_cheb_full_count_sum) + (fs_s_pc_cheb_full_count_sum_body_steps))) /\ fs_s_pc_cheb_full_count_sum_body_steps = fs_r_pc_cheb_full_count_sum_body_steps + fs_a_pc_cheb_full_count_sum_body_steps))))))) -> (exists pc_le_cheb_full_lower. pc_le_cheb_full_lower + (N) = (8 * k * ell)) /\ (exists pc_le_cheb_full_upper. pc_le_cheb_full_upper + (k * ell) = (8 * N))