List of theorems referencing the symbol DOT_S_LT
(561) Theorem 411: [The ordering of two signed integers is defined by the sign of their differences] ((X •S_GE Y) •eq is_nonneg(X •S_PLUS S_Rev(Y))) & ((X •S_LE Y) •eq (Y •S_GE X)) & ((X •S_GT Y) •eq ((X •S_GE Y) & (X /= Y))) & ((X •S_LT Y) •eq (Y •S_GT X))
(869) Theorem 716: [The embedding of signed integers into rationals preserves ordering] ((X in Si) & (Y in Si)) •imp (((RaSi(X) •Ra_GE RaSi(Y)) •eq (X •S_GE Y)) & ((RaSi(X) •Ra_GT RaSi(Y)) •eq (X •S_GT Y)) & ((RaSi(Y) •Ra_LE RaSi(X)) •eq (Y •S_LE X)) & ((RaSi(Y) •Ra_LT RaSi(X)) •eq (Y •S_LT X)))
(873) Theorem 720: [The embedding of integers into signed integers preserves ordering] ((X in Za) & (Y in Za)) •imp (((SiZa(X) •S_GE SiZa(Y)) •eq (X incs Y)) & ((SiZa(X) •S_GT SiZa(Y)) •eq (Y in X)) & ((SiZa(Y) •S_LE SiZa(X)) •eq (Y •incin X)) & ((SiZa(Y) •S_LT SiZa(X)) •eq (Y in X)))