prime_power_quotient_tail_zero

Exact expanded PA statement

forall p n d. ((~(p = 1) /\ forall frm_prime_left_blvb_prime frm_prime_right_blvb_prime. p = frm_prime_left_blvb_prime * frm_prime_right_blvb_prime -> frm_prime_left_blvb_prime = 1 \/ frm_prime_right_blvb_prime = 1)) -> (exists bpvi_b_blvb_quotient_tail_power bpvi_c_blvb_quotient_tail_power. ((forall bpvi_i_blvb_quotient_tail_power. (exists bpvi_repeat_gap_blvb_quotient_tail_power. bpvi_repeat_gap_blvb_quotient_tail_power + S bpvi_i_blvb_quotient_tail_power = S n) -> (((exists bpvi_h_blvb_quotient_tail_power_repeat. bpvi_h_blvb_quotient_tail_power_repeat + S (p) = S ((S (bpvi_i_blvb_quotient_tail_power)) * bpvi_c_blvb_quotient_tail_power)) /\ exists bpvi_q_blvb_quotient_tail_power_repeat. bpvi_b_blvb_quotient_tail_power = bpvi_q_blvb_quotient_tail_power_repeat * S ((S (bpvi_i_blvb_quotient_tail_power)) * bpvi_c_blvb_quotient_tail_power) + (p)))) /\ (exists bpvi_u_blvb_quotient_tail_power bpvi_v_blvb_quotient_tail_power. ((((exists bpvi_h_blvb_quotient_tail_power_start. bpvi_h_blvb_quotient_tail_power_start + S (1) = S ((S (0)) * bpvi_v_blvb_quotient_tail_power)) /\ exists bpvi_q_blvb_quotient_tail_power_start. bpvi_u_blvb_quotient_tail_power = bpvi_q_blvb_quotient_tail_power_start * S ((S (0)) * bpvi_v_blvb_quotient_tail_power) + (1))) /\ ((((exists bpvi_h_blvb_quotient_tail_power_terminal. bpvi_h_blvb_quotient_tail_power_terminal + S (d) = S ((S (S n)) * bpvi_v_blvb_quotient_tail_power)) /\ exists bpvi_q_blvb_quotient_tail_power_terminal. bpvi_u_blvb_quotient_tail_power = bpvi_q_blvb_quotient_tail_power_terminal * S ((S (S n)) * bpvi_v_blvb_quotient_tail_power) + (d))) /\ forall bpvi_j_blvb_quotient_tail_power. (exists bpvi_product_gap_blvb_quotient_tail_power. bpvi_product_gap_blvb_quotient_tail_power + S bpvi_j_blvb_quotient_tail_power = S n) -> exists bpvi_factor_blvb_quotient_tail_power bpvi_partial_blvb_quotient_tail_power bpvi_successor_blvb_quotient_tail_power. ((((exists bpvi_h_blvb_quotient_tail_power_factor. bpvi_h_blvb_quotient_tail_power_factor + S (bpvi_factor_blvb_quotient_tail_power) = S ((S (bpvi_j_blvb_quotient_tail_power)) * bpvi_c_blvb_quotient_tail_power)) /\ exists bpvi_q_blvb_quotient_tail_power_factor. bpvi_b_blvb_quotient_tail_power = bpvi_q_blvb_quotient_tail_power_factor * S ((S (bpvi_j_blvb_quotient_tail_power)) * bpvi_c_blvb_quotient_tail_power) + (bpvi_factor_blvb_quotient_tail_power))) /\ ((((exists bpvi_h_blvb_quotient_tail_power_partial. bpvi_h_blvb_quotient_tail_power_partial + S (bpvi_partial_blvb_quotient_tail_power) = S ((S (bpvi_j_blvb_quotient_tail_power)) * bpvi_v_blvb_quotient_tail_power)) /\ exists bpvi_q_blvb_quotient_tail_power_partial. bpvi_u_blvb_quotient_tail_power = bpvi_q_blvb_quotient_tail_power_partial * S ((S (bpvi_j_blvb_quotient_tail_power)) * bpvi_v_blvb_quotient_tail_power) + (bpvi_partial_blvb_quotient_tail_power))) /\ ((((exists bpvi_h_blvb_quotient_tail_power_successor. bpvi_h_blvb_quotient_tail_power_successor + S (bpvi_successor_blvb_quotient_tail_power) = S ((S (S bpvi_j_blvb_quotient_tail_power)) * bpvi_v_blvb_quotient_tail_power)) /\ exists bpvi_q_blvb_quotient_tail_power_successor. bpvi_u_blvb_quotient_tail_power = bpvi_q_blvb_quotient_tail_power_successor * S ((S (S bpvi_j_blvb_quotient_tail_power)) * bpvi_v_blvb_quotient_tail_power) + (bpvi_successor_blvb_quotient_tail_power))) /\ bpvi_successor_blvb_quotient_tail_power = bpvi_partial_blvb_quotient_tail_power * bpvi_factor_blvb_quotient_tail_power)))))))) -> ((n = (d) * (0) + (n) /\ exists blvb_remainder_gap_blvb_quotient_tail_zero. blvb_remainder_gap_blvb_quotient_tail_zero + S (n) = (d)))