List of theorems referencing the symbol IS_NONNEG
(557+) Theorem 407: [If a signed integer and its additive inverse are both nonnegative, the signed integer is zero] (X in Si) •imp ((is_nonneg(X) or is_nonneg(S_Rev(X))) & ((is_nonneg(X) & is_nonneg(S_Rev(X))) •imp (X = [0,0])))
(558) Theorem 408: [The sum of two non-negative signed integers is non-negative] (((X in Si) & (Y in Si) & is_nonneg(X) & is_nonneg(Y))) •imp (is_nonneg(X •S_PLUS Y) & is_nonneg(X •S_TIMES Y))
(559) Theorem 409: ([0,0] in Si) & (FORALL x in Si | ((x •S_PLUS [0,0]) = x) & ((x •S_PLUS S_Rev(x)) = [0,0]) & (S_Rev(x) in Si)) & (FORALL x in Si, y in Si | ((x •S_PLUS y) in Si) & ((x •S_PLUS y) = (y •S_PLUS x)) & ((x •S_PLUS S_Rev(y)) = (x •S_MINUS y))) & (FORALL x in Si, y in Si, z in Si | ((x •S_PLUS y) •S_PLUS z) = (x •S_PLUS (y •S_PLUS z))) & (FORALL x in Si, y in Si | (is_nonneg(x) & is_nonneg(y)) •imp is_nonneg(x •S_PLUS y)) & (FORALL x in Si | (is_nonneg(x) or is_nonneg(S_Rev(x))) & ((is_nonneg(x) & is_nonneg(S_Rev(x))) •imp (x = [0,0])))
(560) Theorem 410: [The ordering of two signed integers is defined by the sign of their differences] (FORALL x, y | (S_GE(x,y) •eq is_nonneg(x •S_PLUS S_Rev(y))) & (S_LE(x,y) •eq S_GE(y,x)) & (S_GT(x,y) •eq (S_GE(x,y) & (x /= y))) & (S_LT(x,y) •eq S_GT(y,x)))
(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))
(562) Theorem 412: [The square of any signed integer is non-negative] (X in Si) •imp is_nonneg(X •S_TIMES X)
(563) Theorem 413: [The product of signed integers x,y of which x is positive is non-negative iff y is non-negative] ((X in Si) & (Y in Si) & (X /= [0,0]) & is_nonneg(X)) •imp (is_nonneg(X •S_TIMES Y) •eq is_nonneg(Y))
(573) Theorem 424: [?] ((X in Fr) & (Y in Fr) & Same_frac(X,Y) & is_nonneg(cdr(X)) & is_nonneg(cdr(Y))) •imp ((is_nonneg(car(X)) or car(X) = [0,0]) •eq (is_nonneg(car(Y)) or car(Y) = [0,0]))
(574) Theorem 425: [The sign of the product of the numerator and denominator of a fraction defines the sign of the rational number which it represents] ((X in Fr) & (Y in Fr) & Same_frac(X,Y)) •imp (is_nonneg(car(X) •S_TIMES cdr(X)) •eq is_nonneg(car(Y) •S_TIMES cdr(Y)))
(590) Theorem 442: [Expressing the sign of a rational in terms of the numerator and denominator of any representing fraction] ((X in Si) & (Y in Si) & (Y /= [0,0])) •imp (Ra_is_nonneg(Fr_to_Ra([X,Y])) •eq is_nonneg(X •S_TIMES Y))
(635) Theorem 488: ([2,0] in Si) & (is_nonneg([2,0])) & is_nonneg([1,0]) & (Fr_to_Ra([[1,0],[2,0]]) in Ra) & (Fr_to_Ra([[1,0],[2,0]]) •Ra_GT Ra_0)
(865) Theorem 711: [The embedding of signed integers into rationals preserves all elementary algebraic operations, 1] (X in Si) •imp ((RaSi(X) in Ra) & (Ra_is_nonneg(RaSi(X)) •eq is_nonneg(X)) & (RaSi(S_Rev(X)) = Ra_Rev(RaSi(X))) & (RaSi(S_ABS(X)) = Ra_ABS(RaSi(X))))
(920) Theorem 20000: ((N in Si) & (M in Si) & (M /= [0,0]) & is_nonneg(M)) •imp (EXISTS k in Si | is_nonneg(N •S_MINUS (k •S_TIMES M)) & is_nonneg(((k •S_PLUS [1,0])•S_TIMES M)) •S_MINUS N)