beta_sum_pointwise_mod_three_add

forall d b c qb qc mb mc sb sc l X Q M E. (exists ff_u_pointmod_source ff_v_pointmod_source. ((((exists ff_h_pointmod_source_start. ff_h_pointmod_source_start + S (0) = S ((S (0)) * ff_v_pointmod_source)) /\ exists ff_q_pointmod_source_start. ff_u_pointmod_source = ff_q_pointmod_source_start * S ((S (0)) * ff_v_pointmod_source) + (0))) /\ ((((exists ff_h_pointmod_source_terminal. ff_h_pointmod_source_terminal + S (X) = S ((S (l)) * ff_v_pointmod_source)) /\ exists ff_q_pointmod_source_terminal. ff_u_pointmod_source = ff_q_pointmod_source_terminal * S ((S (l)) * ff_v_pointmod_source) + (X))) /\ forall ff_i_pointmod_source. (exists ff_lt_pointmod_source_bound. ff_lt_pointmod_source_bound + S ff_i_pointmod_source = l) -> exists ff_a_pointmod_source ff_r_pointmod_source ff_s_pointmod_source. ((((exists ff_h_pointmod_source_summand. ff_h_pointmod_source_summand + S (ff_a_pointmod_source) = S ((S (ff_i_pointmod_source)) * c)) /\ exists ff_q_pointmod_source_summand. b = ff_q_pointmod_source_summand * S ((S (ff_i_pointmod_source)) * c) + (ff_a_pointmod_source))) /\ ((((exists ff_h_pointmod_source_partial. ff_h_pointmod_source_partial + S (ff_r_pointmod_source) = S ((S (ff_i_pointmod_source)) * ff_v_pointmod_source)) /\ exists ff_q_pointmod_source_partial. ff_u_pointmod_source = ff_q_pointmod_source_partial * S ((S (ff_i_pointmod_source)) * ff_v_pointmod_source) + (ff_r_pointmod_source))) /\ ((((exists ff_h_pointmod_source_successor. ff_h_pointmod_source_successor + S (ff_s_pointmod_source) = S ((S (S ff_i_pointmod_source)) * ff_v_pointmod_source)) /\ exists ff_q_pointmod_source_successor. ff_u_pointmod_source = ff_q_pointmod_source_successor * S ((S (S ff_i_pointmod_source)) * ff_v_pointmod_source) + (ff_s_pointmod_source))) /\ ff_s_pointmod_source = ff_r_pointmod_source + ff_a_pointmod_source)))))) -> (exists ff_u_pointmod_quotient ff_v_pointmod_quotient. ((((exists ff_h_pointmod_quotient_start. ff_h_pointmod_quotient_start + S (0) = S ((S (0)) * ff_v_pointmod_quotient)) /\ exists ff_q_pointmod_quotient_start. ff_u_pointmod_quotient = ff_q_pointmod_quotient_start * S ((S (0)) * ff_v_pointmod_quotient) + (0))) /\ ((((exists ff_h_pointmod_quotient_terminal. ff_h_pointmod_quotient_terminal + S (Q) = S ((S (l)) * ff_v_pointmod_quotient)) /\ exists ff_q_pointmod_quotient_terminal. ff_u_pointmod_quotient = ff_q_pointmod_quotient_terminal * S ((S (l)) * ff_v_pointmod_quotient) + (Q))) /\ forall ff_i_pointmod_quotient. (exists ff_lt_pointmod_quotient_bound. ff_lt_pointmod_quotient_bound + S ff_i_pointmod_quotient = l) -> exists ff_a_pointmod_quotient ff_r_pointmod_quotient ff_s_pointmod_quotient. ((((exists ff_h_pointmod_quotient_summand. ff_h_pointmod_quotient_summand + S (ff_a_pointmod_quotient) = S ((S (ff_i_pointmod_quotient)) * qc)) /\ exists ff_q_pointmod_quotient_summand. qb = ff_q_pointmod_quotient_summand * S ((S (ff_i_pointmod_quotient)) * qc) + (ff_a_pointmod_quotient))) /\ ((((exists ff_h_pointmod_quotient_partial. ff_h_pointmod_quotient_partial + S (ff_r_pointmod_quotient) = S ((S (ff_i_pointmod_quotient)) * ff_v_pointmod_quotient)) /\ exists ff_q_pointmod_quotient_partial. ff_u_pointmod_quotient = ff_q_pointmod_quotient_partial * S ((S (ff_i_pointmod_quotient)) * ff_v_pointmod_quotient) + (ff_r_pointmod_quotient))) /\ ((((exists ff_h_pointmod_quotient_successor. ff_h_pointmod_quotient_successor + S (ff_s_pointmod_quotient) = S ((S (S ff_i_pointmod_quotient)) * ff_v_pointmod_quotient)) /\ exists ff_q_pointmod_quotient_successor. ff_u_pointmod_quotient = ff_q_pointmod_quotient_successor * S ((S (S ff_i_pointmod_quotient)) * ff_v_pointmod_quotient) + (ff_s_pointmod_quotient))) /\ ff_s_pointmod_quotient = ff_r_pointmod_quotient + ff_a_pointmod_quotient)))))) -> (exists ff_u_pointmod_magnitude ff_v_pointmod_magnitude. ((((exists ff_h_pointmod_magnitude_start. ff_h_pointmod_magnitude_start + S (0) = S ((S (0)) * ff_v_pointmod_magnitude)) /\ exists ff_q_pointmod_magnitude_start. ff_u_pointmod_magnitude = ff_q_pointmod_magnitude_start * S ((S (0)) * ff_v_pointmod_magnitude) + (0))) /\ ((((exists ff_h_pointmod_magnitude_terminal. ff_h_pointmod_magnitude_terminal + S (M) = S ((S (l)) * ff_v_pointmod_magnitude)) /\ exists ff_q_pointmod_magnitude_terminal. ff_u_pointmod_magnitude = ff_q_pointmod_magnitude_terminal * S ((S (l)) * ff_v_pointmod_magnitude) + (M))) /\ forall ff_i_pointmod_magnitude. (exists ff_lt_pointmod_magnitude_bound. ff_lt_pointmod_magnitude_bound + S ff_i_pointmod_magnitude = l) -> exists ff_a_pointmod_magnitude ff_r_pointmod_magnitude ff_s_pointmod_magnitude. ((((exists ff_h_pointmod_magnitude_summand. ff_h_pointmod_magnitude_summand + S (ff_a_pointmod_magnitude) = S ((S (ff_i_pointmod_magnitude)) * mc)) /\ exists ff_q_pointmod_magnitude_summand. mb = ff_q_pointmod_magnitude_summand * S ((S (ff_i_pointmod_magnitude)) * mc) + (ff_a_pointmod_magnitude))) /\ ((((exists ff_h_pointmod_magnitude_partial. ff_h_pointmod_magnitude_partial + S (ff_r_pointmod_magnitude) = S ((S (ff_i_pointmod_magnitude)) * ff_v_pointmod_magnitude)) /\ exists ff_q_pointmod_magnitude_partial. ff_u_pointmod_magnitude = ff_q_pointmod_magnitude_partial * S ((S (ff_i_pointmod_magnitude)) * ff_v_pointmod_magnitude) + (ff_r_pointmod_magnitude))) /\ ((((exists ff_h_pointmod_magnitude_successor. ff_h_pointmod_magnitude_successor + S (ff_s_pointmod_magnitude) = S ((S (S ff_i_pointmod_magnitude)) * ff_v_pointmod_magnitude)) /\ exists ff_q_pointmod_magnitude_successor. ff_u_pointmod_magnitude = ff_q_pointmod_magnitude_successor * S ((S (S ff_i_pointmod_magnitude)) * ff_v_pointmod_magnitude) + (ff_s_pointmod_magnitude))) /\ ff_s_pointmod_magnitude = ff_r_pointmod_magnitude + ff_a_pointmod_magnitude)))))) -> (exists ff_u_pointmod_sign ff_v_pointmod_sign. ((((exists ff_h_pointmod_sign_start. ff_h_pointmod_sign_start + S (0) = S ((S (0)) * ff_v_pointmod_sign)) /\ exists ff_q_pointmod_sign_start. ff_u_pointmod_sign = ff_q_pointmod_sign_start * S ((S (0)) * ff_v_pointmod_sign) + (0))) /\ ((((exists ff_h_pointmod_sign_terminal. ff_h_pointmod_sign_terminal + S (E) = S ((S (l)) * ff_v_pointmod_sign)) /\ exists ff_q_pointmod_sign_terminal. ff_u_pointmod_sign = ff_q_pointmod_sign_terminal * S ((S (l)) * ff_v_pointmod_sign) + (E))) /\ forall ff_i_pointmod_sign. (exists ff_lt_pointmod_sign_bound. ff_lt_pointmod_sign_bound + S ff_i_pointmod_sign = l) -> exists ff_a_pointmod_sign ff_r_pointmod_sign ff_s_pointmod_sign. ((((exists ff_h_pointmod_sign_summand. ff_h_pointmod_sign_summand + S (ff_a_pointmod_sign) = S ((S (ff_i_pointmod_sign)) * sc)) /\ exists ff_q_pointmod_sign_summand. sb = ff_q_pointmod_sign_summand * S ((S (ff_i_pointmod_sign)) * sc) + (ff_a_pointmod_sign))) /\ ((((exists ff_h_pointmod_sign_partial. ff_h_pointmod_sign_partial + S (ff_r_pointmod_sign) = S ((S (ff_i_pointmod_sign)) * ff_v_pointmod_sign)) /\ exists ff_q_pointmod_sign_partial. ff_u_pointmod_sign = ff_q_pointmod_sign_partial * S ((S (ff_i_pointmod_sign)) * ff_v_pointmod_sign) + (ff_r_pointmod_sign))) /\ ((((exists ff_h_pointmod_sign_successor. ff_h_pointmod_sign_successor + S (ff_s_pointmod_sign) = S ((S (S ff_i_pointmod_sign)) * ff_v_pointmod_sign)) /\ exists ff_q_pointmod_sign_successor. ff_u_pointmod_sign = ff_q_pointmod_sign_successor * S ((S (S ff_i_pointmod_sign)) * ff_v_pointmod_sign) + (ff_s_pointmod_sign))) /\ ff_s_pointmod_sign = ff_r_pointmod_sign + ff_a_pointmod_sign)))))) -> (forall i x q m s. (exists h. h + S i = l) -> (((exists ff_h_pointmod_source_entry. ff_h_pointmod_source_entry + S (x) = S ((S (i)) * c)) /\ exists ff_q_pointmod_source_entry. b = ff_q_pointmod_source_entry * S ((S (i)) * c) + (x))) -> (((exists ff_h_pointmod_quotient_entry. ff_h_pointmod_quotient_entry + S (q) = S ((S (i)) * qc)) /\ exists ff_q_pointmod_quotient_entry. qb = ff_q_pointmod_quotient_entry * S ((S (i)) * qc) + (q))) -> (((exists ff_h_pointmod_magnitude_entry. ff_h_pointmod_magnitude_entry + S (m) = S ((S (i)) * mc)) /\ exists ff_q_pointmod_magnitude_entry. mb = ff_q_pointmod_magnitude_entry * S ((S (i)) * mc) + (m))) -> (((exists ff_h_pointmod_sign_entry. ff_h_pointmod_sign_entry + S (s) = S ((S (i)) * sc)) /\ exists ff_q_pointmod_sign_entry. sb = ff_q_pointmod_sign_entry * S ((S (i)) * sc) + (s))) -> (exists fspm_u_pointmod_entry fspm_v_pointmod_entry. (x) + d * fspm_u_pointmod_entry = (q + m + s) + d * fspm_v_pointmod_entry)) -> (exists fspm_u_pointmod_endpoint fspm_v_pointmod_endpoint. (X) + d * fspm_u_pointmod_endpoint = (Q + M + E) + d * fspm_v_pointmod_endpoint)