prime_power_quotient_zero_of_exponent_gt

Exact expanded PA statement

forall p n e d q r. ((~(p = 1) /\ forall frm_prime_left_b5cvqz_prime frm_prime_right_b5cvqz_prime. p = frm_prime_left_b5cvqz_prime * frm_prime_right_b5cvqz_prime -> frm_prime_left_b5cvqz_prime = 1 \/ frm_prime_right_b5cvqz_prime = 1)) -> (exists bcf_lt_gap_b5cvqz_exponent. bcf_lt_gap_b5cvqz_exponent + S (n) = e) -> (exists bpvi_b_b5cvqz_power bpvi_c_b5cvqz_power. ((forall bpvi_i_b5cvqz_power. (exists bpvi_repeat_gap_b5cvqz_power. bpvi_repeat_gap_b5cvqz_power + S bpvi_i_b5cvqz_power = e) -> (((exists bpvi_h_b5cvqz_power_repeat. bpvi_h_b5cvqz_power_repeat + S (p) = S ((S (bpvi_i_b5cvqz_power)) * bpvi_c_b5cvqz_power)) /\ exists bpvi_q_b5cvqz_power_repeat. bpvi_b_b5cvqz_power = bpvi_q_b5cvqz_power_repeat * S ((S (bpvi_i_b5cvqz_power)) * bpvi_c_b5cvqz_power) + (p)))) /\ (exists bpvi_u_b5cvqz_power bpvi_v_b5cvqz_power. ((((exists bpvi_h_b5cvqz_power_start. bpvi_h_b5cvqz_power_start + S (1) = S ((S (0)) * bpvi_v_b5cvqz_power)) /\ exists bpvi_q_b5cvqz_power_start. bpvi_u_b5cvqz_power = bpvi_q_b5cvqz_power_start * S ((S (0)) * bpvi_v_b5cvqz_power) + (1))) /\ ((((exists bpvi_h_b5cvqz_power_terminal. bpvi_h_b5cvqz_power_terminal + S (d) = S ((S (e)) * bpvi_v_b5cvqz_power)) /\ exists bpvi_q_b5cvqz_power_terminal. bpvi_u_b5cvqz_power = bpvi_q_b5cvqz_power_terminal * S ((S (e)) * bpvi_v_b5cvqz_power) + (d))) /\ forall bpvi_j_b5cvqz_power. (exists bpvi_product_gap_b5cvqz_power. bpvi_product_gap_b5cvqz_power + S bpvi_j_b5cvqz_power = e) -> exists bpvi_factor_b5cvqz_power bpvi_partial_b5cvqz_power bpvi_successor_b5cvqz_power. ((((exists bpvi_h_b5cvqz_power_factor. bpvi_h_b5cvqz_power_factor + S (bpvi_factor_b5cvqz_power) = S ((S (bpvi_j_b5cvqz_power)) * bpvi_c_b5cvqz_power)) /\ exists bpvi_q_b5cvqz_power_factor. bpvi_b_b5cvqz_power = bpvi_q_b5cvqz_power_factor * S ((S (bpvi_j_b5cvqz_power)) * bpvi_c_b5cvqz_power) + (bpvi_factor_b5cvqz_power))) /\ ((((exists bpvi_h_b5cvqz_power_partial. bpvi_h_b5cvqz_power_partial + S (bpvi_partial_b5cvqz_power) = S ((S (bpvi_j_b5cvqz_power)) * bpvi_v_b5cvqz_power)) /\ exists bpvi_q_b5cvqz_power_partial. bpvi_u_b5cvqz_power = bpvi_q_b5cvqz_power_partial * S ((S (bpvi_j_b5cvqz_power)) * bpvi_v_b5cvqz_power) + (bpvi_partial_b5cvqz_power))) /\ ((((exists bpvi_h_b5cvqz_power_successor. bpvi_h_b5cvqz_power_successor + S (bpvi_successor_b5cvqz_power) = S ((S (S bpvi_j_b5cvqz_power)) * bpvi_v_b5cvqz_power)) /\ exists bpvi_q_b5cvqz_power_successor. bpvi_u_b5cvqz_power = bpvi_q_b5cvqz_power_successor * S ((S (S bpvi_j_b5cvqz_power)) * bpvi_v_b5cvqz_power) + (bpvi_successor_b5cvqz_power))) /\ bpvi_successor_b5cvqz_power = bpvi_partial_b5cvqz_power * bpvi_factor_b5cvqz_power)))))))) -> (((n) = (d) * (q) + (r) /\ (exists bcf_lt_gap_b5cvqz_division_bound. bcf_lt_gap_b5cvqz_division_bound + S (r) = d))) -> q = 0