Definition in prerequisite notation
∀ jt_index_definition_jordan. ∀ jt_value_definition_jordan. Lt(jt_index_definition_jordan,k) → BetaAt(b,c,jt_index_definition_jordan,jt_value_definition_jordan) → Dvd(d,jt_value_definition_jordan)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
forall jt_index_definition_jordan jt_value_definition_jordan. (exists jt_gap_definition_jordanindex. jt_gap_definition_jordanindex+S (jt_index_definition_jordan)=(k)) -> (((exists fs_h_jt_definition_jordanat. fs_h_jt_definition_jordanat + S (jt_value_definition_jordan) = S ((S (jt_index_definition_jordan)) * c)) /\ exists fs_q_jt_definition_jordanat. b = fs_q_jt_definition_jordanat * S ((S (jt_index_definition_jordan)) * c) + (jt_value_definition_jordan))) -> (exists jt_factor_definition_jordandivides. (jt_value_definition_jordan)=(d)*jt_factor_definition_jordandivides)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
JT0004 · jordan_tuple_common_divisor_transportJT0007 · jordan_tuple_divisor_downwardJT0010 · jordan_tuple_all_divisible_emptyJT0011 · jordan_tuple_all_divisible_extendJT0012 · jordan_tuple_all_divisible_decidableJT0013 · jordan_tuple_divisor_test_decidableJT0014 · jordan_tuple_primitive_bounded_decidableJT0015 · jordan_primitive_tuple_decidableJT005D · jordan_primitive_tuple_avoids_prime_common_divisorJT005E · jordan_prime_power_tuple_primitive_of_not_all_divisibleJT005F · jordan_prime_power_tuple_primitive_characterization