mobius_prime_square_value_zero

Exact expanded first-order arithmetic statement

forall n p z. (~((p) = 1) /\ forall pvs_left_square_value_prime pvs_right_square_value_prime. (p) = pvs_left_square_value_prime * pvs_right_square_value_prime -> pvs_left_square_value_prime = 1 \/ pvs_right_square_value_prime = 1) -> (exists pvs_factor_square_value_divisor. (n) = (p * p) * pvs_factor_square_value_divisor) -> (((~((n) = 0)) /\ ((((exists mv_square_prime_square_value_inputsquare. ((~((mv_square_prime_square_value_inputsquare) = 1) /\ forall pvs_left_square_value_inputsquareprime pvs_right_square_value_inputsquareprime. (mv_square_prime_square_value_inputsquare) = pvs_left_square_value_inputsquareprime * pvs_right_square_value_inputsquareprime -> pvs_left_square_value_inputsquareprime = 1 \/ pvs_right_square_value_inputsquareprime = 1) /\ (exists pvs_factor_square_value_inputsquaredivisor. (n) = (mv_square_prime_square_value_inputsquare * mv_square_prime_square_value_inputsquare) * pvs_factor_square_value_inputsquaredivisor))) /\ ((z) = 0))) \/ (((((~((n) = 0)) /\ (forall sfd_prime_square_value_inputsquarefree. (~((sfd_prime_square_value_inputsquarefree) = 1) /\ forall pvs_left_square_value_inputsquarefreedomain pvs_right_square_value_inputsquarefreedomain. (sfd_prime_square_value_inputsquarefree) = pvs_left_square_value_inputsquarefreedomain * pvs_right_square_value_inputsquarefreedomain -> pvs_left_square_value_inputsquarefreedomain = 1 \/ pvs_right_square_value_inputsquarefreedomain = 1) -> (exists pvs_le_gap_square_value_inputsquarefreebound. pvs_le_gap_square_value_inputsquarefreebound + (sfd_prime_square_value_inputsquarefree) = (n)) -> ~(exists pvs_factor_square_value_inputsquarefreesquare. (n) = (sfd_prime_square_value_inputsquarefree * sfd_prime_square_value_inputsquarefree) * pvs_factor_square_value_inputsquarefreesquare)))) /\ (exists mv_factor_code_square_value_inputfactors mv_factor_scale_square_value_inputfactors mv_factor_count_square_value_inputfactors. (((~(n = 0) /\ ((exists ff_u_fsat_square_value_inputfactorsfactorization_product ff_v_fsat_square_value_inputfactorsfactorization_product. ((((exists ff_h_fsat_square_value_inputfactorsfactorization_product_start. ff_h_fsat_square_value_inputfactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_square_value_inputfactorsfactorization_product)) /\ exists ff_q_fsat_square_value_inputfactorsfactorization_product_start. ff_u_fsat_square_value_inputfactorsfactorization_product = ff_q_fsat_square_value_inputfactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_square_value_inputfactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_square_value_inputfactorsfactorization_product_terminal. ff_h_fsat_square_value_inputfactorsfactorization_product_terminal + S (n) = S ((S (mv_factor_count_square_value_inputfactors)) * ff_v_fsat_square_value_inputfactorsfactorization_product)) /\ exists ff_q_fsat_square_value_inputfactorsfactorization_product_terminal. ff_u_fsat_square_value_inputfactorsfactorization_product = ff_q_fsat_square_value_inputfactorsfactorization_product_terminal * S ((S (mv_factor_count_square_value_inputfactors)) * ff_v_fsat_square_value_inputfactorsfactorization_product) + (n))) /\ forall ff_i_fsat_square_value_inputfactorsfactorization_product. (exists ff_lt_fsat_square_value_inputfactorsfactorization_product_bound. ff_lt_fsat_square_value_inputfactorsfactorization_product_bound + S ff_i_fsat_square_value_inputfactorsfactorization_product = mv_factor_count_square_value_inputfactors) -> exists ff_p_fsat_square_value_inputfactorsfactorization_product ff_r_fsat_square_value_inputfactorsfactorization_product ff_s_fsat_square_value_inputfactorsfactorization_product. ((((exists ff_h_fsat_square_value_inputfactorsfactorization_product_factor. ff_h_fsat_square_value_inputfactorsfactorization_product_factor + S (ff_p_fsat_square_value_inputfactorsfactorization_product) = S ((S (ff_i_fsat_square_value_inputfactorsfactorization_product)) * mv_factor_scale_square_value_inputfactors)) /\ exists ff_q_fsat_square_value_inputfactorsfactorization_product_factor. mv_factor_code_square_value_inputfactors = ff_q_fsat_square_value_inputfactorsfactorization_product_factor * S ((S (ff_i_fsat_square_value_inputfactorsfactorization_product)) * mv_factor_scale_square_value_inputfactors) + (ff_p_fsat_square_value_inputfactorsfactorization_product))) /\ ((((exists ff_h_fsat_square_value_inputfactorsfactorization_product_partial. ff_h_fsat_square_value_inputfactorsfactorization_product_partial + S (ff_r_fsat_square_value_inputfactorsfactorization_product) = S ((S (ff_i_fsat_square_value_inputfactorsfactorization_product)) * ff_v_fsat_square_value_inputfactorsfactorization_product)) /\ exists ff_q_fsat_square_value_inputfactorsfactorization_product_partial. ff_u_fsat_square_value_inputfactorsfactorization_product = ff_q_fsat_square_value_inputfactorsfactorization_product_partial * S ((S (ff_i_fsat_square_value_inputfactorsfactorization_product)) * ff_v_fsat_square_value_inputfactorsfactorization_product) + (ff_r_fsat_square_value_inputfactorsfactorization_product))) /\ ((((exists ff_h_fsat_square_value_inputfactorsfactorization_product_successor. ff_h_fsat_square_value_inputfactorsfactorization_product_successor + S (ff_s_fsat_square_value_inputfactorsfactorization_product) = S ((S (S ff_i_fsat_square_value_inputfactorsfactorization_product)) * ff_v_fsat_square_value_inputfactorsfactorization_product)) /\ exists ff_q_fsat_square_value_inputfactorsfactorization_product_successor. ff_u_fsat_square_value_inputfactorsfactorization_product = ff_q_fsat_square_value_inputfactorsfactorization_product_successor * S ((S (S ff_i_fsat_square_value_inputfactorsfactorization_product)) * ff_v_fsat_square_value_inputfactorsfactorization_product) + (ff_s_fsat_square_value_inputfactorsfactorization_product))) /\ ff_s_fsat_square_value_inputfactorsfactorization_product = ff_r_fsat_square_value_inputfactorsfactorization_product * ff_p_fsat_square_value_inputfactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_square_value_inputfactorsfactorization_primes. (exists ftsf_gap_fsat_square_value_inputfactorsfactorization_primes_bound. ftsf_gap_fsat_square_value_inputfactorsfactorization_primes_bound + S ftsf_index_fsat_square_value_inputfactorsfactorization_primes = (mv_factor_count_square_value_inputfactors)) -> exists ftsf_factor_fsat_square_value_inputfactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_square_value_inputfactorsfactorization_primes_entry. ff_h_ftsf_fsat_square_value_inputfactorsfactorization_primes_entry + S (ftsf_factor_fsat_square_value_inputfactorsfactorization_primes) = S ((S (ftsf_index_fsat_square_value_inputfactorsfactorization_primes)) * mv_factor_scale_square_value_inputfactors)) /\ exists ff_q_ftsf_fsat_square_value_inputfactorsfactorization_primes_entry. mv_factor_code_square_value_inputfactors = ff_q_ftsf_fsat_square_value_inputfactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_square_value_inputfactorsfactorization_primes)) * mv_factor_scale_square_value_inputfactors) + (ftsf_factor_fsat_square_value_inputfactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_square_value_inputfactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_square_value_inputfactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_square_value_inputfactorsfactorization_primes_prime. ftsf_factor_fsat_square_value_inputfactorsfactorization_primes = frm_prime_left_ftsf_fsat_square_value_inputfactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_square_value_inputfactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_square_value_inputfactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_square_value_inputfactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_square_value_inputfactorsparityeven. (mv_factor_count_square_value_inputfactors) = 2 * mv_even_half_square_value_inputfactorsparityeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_square_value_inputfactorsparityodd. (mv_factor_count_square_value_inputfactors) = 2 * mv_odd_half_square_value_inputfactorsparityodd + 1) /\ ((z) = 1))))))))))) -> z = 0