ND0372 — JordanPrimitiveTuple(n,b,c,k)

Definition in prerequisite notation

∀ jt_divisor_definition_jordan. Dvd(jt_divisor_definition_jordan,n) → JordanTupleAllDivisible(jt_divisor_definition_jordan,b,c,k) → jt_divisor_definition_jordan = 1

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

Hygienic expanded first-order definition

forall jt_divisor_definition_jordan. (exists jt_factor_definition_jordanmodulus. (n)=(jt_divisor_definition_jordan)*jt_factor_definition_jordanmodulus) -> (forall jt_index_definition_jordancoordinates jt_value_definition_jordancoordinates. (exists jt_gap_definition_jordancoordinatesindex. jt_gap_definition_jordancoordinatesindex+S (jt_index_definition_jordancoordinates)=(k)) -> (((exists fs_h_jt_definition_jordancoordinatesat. fs_h_jt_definition_jordancoordinatesat + S (jt_value_definition_jordancoordinates) = S ((S (jt_index_definition_jordancoordinates)) * c)) /\ exists fs_q_jt_definition_jordancoordinatesat. b = fs_q_jt_definition_jordancoordinatesat * S ((S (jt_index_definition_jordancoordinates)) * c) + (jt_value_definition_jordancoordinates))) -> (exists jt_factor_definition_jordancoordinatesdivides. (jt_value_definition_jordancoordinates)=(jt_divisor_definition_jordan)*jt_factor_definition_jordancoordinatesdivides)) -> jt_divisor_definition_jordan=1

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

Direct definition dependencies

Dvd(d,n)JordanTupleAllDivisible(d,b,c,k)

Definitions depending on this notation

JordanTupleEnumeration(k,n,B,C,D,E,j)JordanTupleScan(k,n,c,limit,B,C,D,E,j)JordanRectangleCRT(m,n,k,A,B,C,D,u,E,F,G,H,v,P,Q,R,T,q)

Checked theorems using this definition