ND0138

IntegerMatrixEntrywiseEqual(ab,ac,bb,bc,eb,ec,fb,fc,r,w)

Genuine signed-integer equality at every actual row-major entry of two r-by-w matrices, reusing integer-vector equality at length r*w.

Conservative notation; not a theorem, primitive, or axiom.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Definition in prerequisite notation

IntegerVectorEqual(ab,ac,bb,bc,eb,ec,fb,fc,r · w)

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition 
forall ics_index_secondwave ics_value0_secondwave ics_value1_secondwave ics_value2_secondwave ics_value3_secondwave. (exists ics_gap_secondwave_bound. ics_gap_secondwave_bound + S (ics_index_secondwave) = ((r) * (w))) -> (((exists fs_h_ics_secondwave_at0. fs_h_ics_secondwave_at0 + S (ics_value0_secondwave) = S ((S (ics_index_secondwave)) * ac)) /\ exists fs_q_ics_secondwave_at0. ab = fs_q_ics_secondwave_at0 * S ((S (ics_index_secondwave)) * ac) + (ics_value0_secondwave))) -> (((exists fs_h_ics_secondwave_at1. fs_h_ics_secondwave_at1 + S (ics_value1_secondwave) = S ((S (ics_index_secondwave)) * bc)) /\ exists fs_q_ics_secondwave_at1. bb = fs_q_ics_secondwave_at1 * S ((S (ics_index_secondwave)) * bc) + (ics_value1_secondwave))) -> (((exists fs_h_ics_secondwave_at2. fs_h_ics_secondwave_at2 + S (ics_value2_secondwave) = S ((S (ics_index_secondwave)) * ec)) /\ exists fs_q_ics_secondwave_at2. eb = fs_q_ics_secondwave_at2 * S ((S (ics_index_secondwave)) * ec) + (ics_value2_secondwave))) -> (((exists fs_h_ics_secondwave_at3. fs_h_ics_secondwave_at3 + S (ics_value3_secondwave) = S ((S (ics_index_secondwave)) * fc)) /\ exists fs_q_ics_secondwave_at3. fb = fs_q_ics_secondwave_at3 * S ((S (ics_index_secondwave)) * fc) + (ics_value3_secondwave))) -> ics_value0_secondwave + ics_value3_secondwave = ics_value2_secondwave + ics_value1_secondwave

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

IntegerVectorEqual(ab,ac,db,dc,eb,ec,fb,fc,l)

Definitions depending on this notation

none

Checked theorems using this definition

DL008E · matrix_integer_minor_cell_balanceDL0091 · matrix_integer_signed_minor_balanceDL0092 · matrix_integer_cofactor_streams_from_recursionDL0093 · matrix_integer_first_row_equalityDL0094 · signed_recursive_determinant_integer_invariantDL0097 · matrix_integer_selected_point_balanceDL0099 · matrix_integer_signed_selected_balanceDL009A · matrix_integer_selected_determinant_balanceDL009C · matrix_integer_nonzero_minor_transportDL009D · matrix_integer_all_minors_zero_transportDL009E · rectangular_matrix_rank_integer_transportDL009F · rectangular_matrix_rank_integer_invariantDL00A9 · absolute_recursive_determinant_integer_transportDL00AD · positive_determinant_matrix_data_integer_transport