Definition in prerequisite notation
∀ jt_index_definition_jordan. ∀ jt_left_definition_jordan. ∀ jt_right_definition_jordan. Lt(jt_index_definition_jordan,k) → BetaAt(b,c,jt_index_definition_jordan,jt_left_definition_jordan) → BetaAt(d,e,jt_index_definition_jordan,jt_right_definition_jordan) → ModEq(n,jt_left_definition_jordan,jt_right_definition_jordan)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
forall jt_index_definition_jordan jt_left_definition_jordan jt_right_definition_jordan. (exists jt_gap_definition_jordanindex. jt_gap_definition_jordanindex+S (jt_index_definition_jordan)=(k)) -> (((exists fs_h_jt_definition_jordanleft. fs_h_jt_definition_jordanleft + S (jt_left_definition_jordan) = S ((S (jt_index_definition_jordan)) * c)) /\ exists fs_q_jt_definition_jordanleft. b = fs_q_jt_definition_jordanleft * S ((S (jt_index_definition_jordan)) * c) + (jt_left_definition_jordan))) -> (((exists fs_h_jt_definition_jordanright. fs_h_jt_definition_jordanright + S (jt_right_definition_jordan) = S ((S (jt_index_definition_jordan)) * e)) /\ exists fs_q_jt_definition_jordanright. d = fs_q_jt_definition_jordanright * S ((S (jt_index_definition_jordan)) * e) + (jt_right_definition_jordan))) -> (exists jt_left_definition_jordanmod jt_right_definition_jordanmod. (jt_left_definition_jordan)+(n)*jt_left_definition_jordanmod=(jt_right_definition_jordan)+(n)*jt_right_definition_jordanmod)The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
Checked theorems using this definition
JT000E · jordan_tuple_congruence_symmJT000F · jordan_primitive_tuple_congruence_transportJT002D · jordan_crt_tuple_leftJT002E · jordan_crt_tuple_rightJT002F · jordan_tuple_normalize_existsJT0030 · jordan_tuple_congruence_transJT0031 · jordan_tuple_congruence_divisorJT0032 · jordan_canonical_crt_tuple_existsJT0038 · jordan_tuple_equal_congruenceJT0039 · jordan_tuple_bounded_congruence_equalJT003A · jordan_tuple_congruence_coprime_productJT003B · jordan_crt_component_recoveryJT0045 · jordan_enumeration_reduce_primitiveJT0047 · jordan_rectangle_crt_covers