List of theorems referencing the symbol R_IS_NONNEG

(792) Theorem 642: [Any real x or its reverse is non-negative, and if both are non-negative, then x = 0] (X in Re) •imp ((R_is_nonneg(X) or R_is_nonneg(R_Rev(X))) & ((R_is_nonneg(X) & R_is_nonneg(R_Rev(X))) •imp (X = R_0)))
(793) Theorem 643: [Each non-negative rational Cauchy sequences is equivalent to its own absolute value] (X in Re) •imp (R_is_nonneg(X) •eq Ra_eqseq(arb(X),Ras_ABS(arb(X))))
(794) Theorem 644: [The sum of two non-negative rational Cauchy sequences is equivalent to its own absolute value] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y)) •imp Ra_eqseq(arb(X) •Ras_PLUS arb(Y),Ras_ABS(arb(X) •Ras_PLUS arb(Y)))
(795) Theorem 645: [The product of two non-negative rational Cauchy sequences is equivalent to its own absolute value] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y)) •imp Ra_eqseq(arb(X) •Ras_TIMES arb(Y),Ras_ABS(arb(X) •Ras_TIMES arb(Y)))
(796) Theorem 646: [The sum and product of two non-negative reals is non-negative] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y)) •imp (R_is_nonneg(X •R_PLUS Y) & R_is_nonneg(X •R_TIMES Y))
(800) Theorem 650: [0 and 1 are non-negative reals] R_is_nonneg(R_0) & R_is_nonneg(R_1)
(802) Theorem 652: [The ordering of reals is defined by the sign of their differences] ((((X in Re) & (Y in Re)) •imp ((X •R_GE Y) •eq R_is_nonneg(X •R_PLUS R_Rev(Y))))) & ((X •R_LE Y) •eq (Y •R_GE X)) & ((X •R_GT Y) •eq ((X •R_GE Y) & (X /= Y))) & ((X •R_LT Y) •eq (Y •R_GT X))
(803) Theorem 653: [Various basic properties of real comparison, quantified form] (FORALL x, y | ((x in Re) & (y in Re)) •imp ((x •R_GE y) •eq R_is_nonneg(x •R_PLUS R_Rev(y)))) & (FORALL x, y | ((x •R_LE y) •eq (y •R_GE x))) & (FORALL x, y | ((x •R_GT y) •eq ((x •R_GE y) & (x /= y)))) & (FORALL x, y | ((x •R_LT y) •eq (y •R_GT x))) & (FORALL x, y | ((x in Re) & (y in Re)) •imp ((x •R_LE y) •eq (R_is_nonneg(y •R_PLUS R_Rev(x))))) & (FORALL x, y | ((x in Re) & (y in Re)) •imp ((x •R_GT y) •eq (R_is_nonneg(x •R_PLUS R_Rev(y)) & (x /= y)))) & (FORALL x, y | (((x in Re) & (y in Re)) •imp ((x •R_GT y) •eq (R_is_nonneg(x •R_MINUS y) & (x /= y))))) & (FORALL x, y | ((x in Re) & (y in Re) & ((x = y) or (not(x •R_GE y)))) •imp (y •R_GE x))
(804) Theorem 654: [Various basic properties of real comparison] (((X in Re) & (Y in Re)) •imp ((X •R_GE Y) •eq R_is_nonneg(X •R_PLUS R_Rev(Y)))) & ((X •R_LE Y) •eq (Y •R_GE X)) & ((X •R_GT Y) •eq ((X •R_GE Y) & (X /= Y))) & ((X •R_LT Y) •eq (Y •R_GT X)) & (((X in Re) & (Y in Re)) •imp ((X •R_LE Y) •eq R_is_nonneg(Y •R_PLUS R_Rev(X)))) & (((X in Re) & (Y in Re)) •imp ((X •R_GT Y) •eq (R_is_nonneg(X •R_PLUS R_Rev(Y)) & (X /= Y)))) & (((X in Re) & (Y in Re)) •imp ((X •R_GT Y) •eq (R_is_nonneg(X •R_MINUS Y) & (X /= Y)))) & (((X in Re) & (Y in Re) & ((X = Y) or (not(X •R_GE Y)))) •imp (Y •R_GE X))
(809) Theorem 659: [Greater_than_equal is greater-than and equal] (X in Re) •imp ((X •R_GE R_0) •eq R_is_nonneg(X))
(822) Theorem 672a: ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y) & (X •R_PLUS Y = R_0)) •imp ((X = R_0) & (Y = R_0))
(829) Theorem 678: [The product of reals x,y of which x is positive is non-negative iff y is non-negative] ((X in Re) & (Y in Re) & (X /= R_0) & R_is_nonneg(X)) •imp (R_is_nonneg(X •R_TIMES Y) •eq R_is_nonneg(Y))
(830) Theorem 679: [The product of nonnegative reals is non-negative] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y)) •imp R_is_nonneg(X •R_TIMES Y)
(836) Theorem 684: [The square of any real is non-negative] (X in Re) •imp R_is_nonneg(X •R_TIMES X)
(843) Theorem 690: [Trigger for Otter theory 'orderedGroups'] (R_0 in Re) & (FORALL x,y | ((x in Re) & (y in Re)) •imp ((x •R_PLUS y) in Re)) & (FORALL x | (x in Re) •imp (R_Rev(x) in Re)) & (FORALL x,y,z | ((x in Re) & (y in Re) & (z in Re)) •imp (((x •R_PLUS y) •R_PLUS z) = (x •R_PLUS (y •R_PLUS z)))) & (FORALL x | (x in Re) •imp ((x •R_PLUS R_0) = x)) & (FORALL x | (x in Re) •imp ((x •R_PLUS R_Rev(x)) = R_0)) & (FORALL x,y | ((x in Re) & (y in Re)) •imp ((x •R_PLUS y) = (y •R_PLUS x))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp ((R_is_nonneg(x) & R_is_nonneg(y)) •imp R_is_nonneg(x •R_PLUS y))) & (FORALL x | (x in Re) •imp (R_is_nonneg(x) or R_is_nonneg(R_Rev(x)))) & (FORALL x | (x in Re) •imp ((R_is_nonneg(x) & R_is_nonneg(R_Rev(x))) •imp (x = R_0))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp ((x •R_LE y) •eq R_is_nonneg(y •R_PLUS R_Rev(x))))
(844) Theorem 691: [Basic properties of the absolute value function] (FORALL x | abs(x) = if R_is_nonneg(x) then x else R_Rev(x) end if) & (FORALL x | (x in Re) •imp (x •R_LE abs(x))) & (FORALL x | (x in Re) •imp (abs(abs(x)) = abs(x))) & (FORALL x | (x in Re) •imp ((abs(x) = R_0) •eq (x = R_0))) & (FORALL x | (x in Re) •imp (abs(R_Rev(x)) = abs(x))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp ((x •R_PLUS y) •R_LE (abs(x) •R_PLUS abs(y)))) & (FORALL x,y,z | ((x in Re) & (y in Re) & (z in Re)) •imp ((abs(x •R_PLUS R_Rev(y)) •R_LE z) •imp (y •R_LE (x •R_PLUS z)))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp (abs(x •R_PLUS y) •R_LE (abs(x) •R_PLUS abs(y)))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp ((not(R_is_nonneg(x))) •imp ((x •R_LE abs(y)) & (x /= abs(y))))) & (FORALL x,y,z | ((x in Re) & (y in Re) & (z in Re)) •imp (abs((x •R_PLUS R_Rev(z))) •R_LE (abs(x •R_PLUS R_Rev(y)) •R_PLUS abs(y •R_PLUS R_Rev(z))))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp (abs(abs(x) •R_PLUS R_Rev(abs(y))) •R_LE abs(x •R_PLUS R_Rev(y)))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp (abs(x) •R_PLUS R_Rev(abs(abs(y) •R_PLUS R_Rev(abs(x)))) •R_LE abs(y)))
(845) Theorem 692: [The absolute value of x is a non-negative real no smaller than x] (X in Re) •imp ((abs(X) in Re) & (abs(X) •R_GE R_0) & (abs(X) •R_GE X) & (R_is_nonneg(abs(X))))
(846) Theorem 693: [The absolute value of x is whichever of x and -x is non-negative] (X in Re) •imp (abs(X) = if R_is_nonneg(X) then X else R_Rev(X) end if)
(847) Theorem 694: [The absolute value of x is whichever of x and -x is non-negative, 2] (X in Re) •imp (abs(X) = if R_is_nonneg(R_Rev(X)) then R_Rev(X) else X end if)
(850) Theorem 697: [Monotonicity of addition, 2] ((X in Re) & (Y in Re) & R_is_nonneg(R_Rev(Y))) •imp ((X •R_GT (X •R_PLUS Y)) or (X = (X •R_PLUS Y)))
(851) Theorem 698: ((X in Re) & (Y in Re) & R_is_nonneg(X) & (not R_is_nonneg(Y))) •imp ((X •R_GE abs(X •R_PLUS Y)) or (R_Rev(Y) •R_GE abs(X •R_PLUS Y)))
(856) Theorem 703: (X in Ra) •imp (R_is_nonneg(Cauchy_to_Re(Za •PROD {X})) •eq (ReRa(Ra_ABS(X)) = ReRa(X)))
(857) Theorem 704: [The embedding of rationals into reals preserves all elementary algebraic operations, 1] (Y in Ra) •imp ((ReRa(Y) in Re) & (ReRa(Ra_Rev(Y)) = R_Rev(ReRa(Y))) & (R_is_nonneg(ReRa(Y)) •eq Ra_is_nonneg(Y)) & (ReRa(Ra_ABS(Y)) = abs(ReRa(Y))))
(915) Theorem 760: [The square of the square root of any positive x is x] ((X in Re) & (R_is_nonneg(X))) •imp ((sqrt(X) in Re) & (R_is_nonneg(sqrt(X))) & ((sqrt(X) •R_TIMES sqrt(X)) = X))
(916) Theorem 761: [The positive square root is unique] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y) & ((Y •R_TIMES Y) = X)) •imp (Y = sqrt(X))
(917) Theorem 762: [The square root is monotone increasing for positive numbers] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y) & (X •R_GT Y)) •imp (sqrt(X) •R_GT sqrt(Y))
(918) Theorem 763: [The square root of a product is the product of the square roots] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y)) •imp (sqrt(X •R_TIMES Y) = (sqrt(X) •R_TIMES sqrt(Y)))
(922) Theorem 20003: ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y) & (X •R_PLUS Y = R_0)) •imp ((X = R_0) & (Y = R_0))
(935) Theorem 812: (N in Cm) •imp ((C_abs(N) in Re) & R_is_nonneg(C_abs(N)))