List of theorems referencing the symbol RA_ABS

(653) Theorem 506: [?] (FORALL x | Ra_ABS(x) = if Ra_is_nonneg(x) then x else Ra_Rev(x) end if) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (((x •Ra_PLUS y) = (x •Ra_PLUS z)) •imp (y = z))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp (Ra_Rev(x •Ra_PLUS Ra_Rev(y)) = (y •Ra_PLUS Ra_Rev(x)))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp ((x •Ra_LE y) or (y •Ra_LE x))) & (FORALL x | (x in Ra) •imp (x •Ra_LE x)) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (((x •Ra_LE y) & (y •Ra_LE z)) •imp (x •Ra_LE z))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (((x •Ra_LE y) & (x /= y) & (y •Ra_LE z)) •imp (x /= z))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (((x •Ra_LE y) & (y •Ra_LE z) & (y /= z)) •imp (x /= z))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp ((x •Ra_LE y) •imp ((x •Ra_PLUS z) •Ra_LE (y •Ra_PLUS z)))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (((x •Ra_PLUS z) = (y •Ra_PLUS z)) •imp (x = y))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (((x •Ra_LE y) & (x /= y)) •imp ((x •Ra_PLUS z) /= (y •Ra_PLUS z)))) & (FORALL x | (x in Ra) •imp (Ra_ABS(x •Ra_PLUS Ra_Rev(x)) = Ra_0)) & (FORALL x | (x in Ra) •imp (x •Ra_LE Ra_ABS(x))) & (FORALL x | (x in Ra) •imp (Ra_ABS(Ra_ABS(x)) = Ra_ABS(x))) & (FORALL x | (x in Ra) •imp ((Ra_ABS(x) = Ra_0) •eq (x = Ra_0))) & (FORALL x | (x in Ra) •imp (Ra_ABS(Ra_Rev(x)) = Ra_ABS(x))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp ((x •Ra_PLUS y) •Ra_LE (Ra_ABS(x) •Ra_PLUS Ra_ABS(y)))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp ((Ra_ABS(x •Ra_PLUS Ra_Rev(y)) •Ra_LE z) •imp (y •Ra_LE (x •Ra_PLUS z)))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp (Ra_ABS(x •Ra_PLUS y) •Ra_LE (Ra_ABS(x) •Ra_PLUS Ra_ABS(y)))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp ((not(Ra_is_nonneg(x))) •imp ((x •Ra_LE Ra_ABS(y)) & (x /= Ra_ABS(y))))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (Ra_ABS((x •Ra_PLUS Ra_Rev(z))) •Ra_LE (Ra_ABS(x •Ra_PLUS Ra_Rev(y)) •Ra_PLUS Ra_ABS(y •Ra_PLUS Ra_Rev(z))))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp (Ra_is_nonneg(y) •imp ((x •Ra_PLUS Ra_Rev(y)) •Ra_LE (x •Ra_PLUS y)))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp (Ra_ABS(Ra_ABS(x) •Ra_PLUS Ra_Rev(Ra_ABS(y))) •Ra_LE Ra_ABS(x •Ra_PLUS Ra_Rev(y)))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp (Ra_ABS(x) •Ra_PLUS Ra_Rev(Ra_ABS(Ra_ABS(y) •Ra_PLUS Ra_Rev(Ra_ABS(x)))) •Ra_LE Ra_ABS(y)))
(655) Theorem 508: [The absolute value of a rational x is a non-negative rational no smaller than x] (X in Ra) •imp ((Ra_ABS(X) in Ra) & (Ra_ABS(X) •Ra_GE Ra_0) & (Ra_ABS(X) •Ra_GE X))
(656) Theorem 509: [The absolute value of a non-negative rational x is x] (X in Ra) •imp ((X •Ra_GE Ra_0) •eq (Ra_ABS(X) = X))
(657) Theorem 510: [The absolute value of a rational x greater than Ra_0 is x] ((X in Ra) & (X •Ra_GT Ra_0)) •imp (Ra_ABS(X) = X)
(658) Theorem 511: [The absolute value of a rational product is the product of the absolute values] ((X in Ra) & (Y in Ra)) •imp (Ra_ABS(X •Ra_TIMES Y) = (Ra_ABS(X) •Ra_TIMES Ra_ABS(Y)))
(664) Theorem 517: [The absolute value of the reciprocal equals the reciprocal of the absolute value] ((X in Ra) & (X /= Ra_0)) •imp (Ra_ABS(Recip(X)) = Recip(Ra_ABS(X)))
(664+) Theorem 518: ((X in Ra) & (Y in Ra)) •imp (Ra_ABS(X •Ra_MINUS Y) = Ra_ABS(Y •Ra_MINUS X))
(665) Theorem 519: ((X in Ra) & (Y in Ra) & (A in Ra) & (B in Ra) & (Ra_ABS(X) •Ra_GT A) & (Ra_ABS(Y) •Ra_GT B) & (A •Ra_GT Ra_0) & (B •Ra_GT Ra_0)) •imp (Ra_ABS(Recip(X) •Ra_MINUS Recip(Y)) •Ra_LE (Ra_ABS(X •Ra_MINUS Y) •Ra_TIMES (Recip(A) •Ra_TIMES Recip(B))))
(676) Theorem 525: (X in Ra) •imp (Ras_ABS(Za •PROD {X}) = (Za •PROD {Ra_ABS(X)}))
(683) Theorem 532: ((Eps in Ra) & (Eps •Ra_GT Ra_0) & (F in RaCauchy)) •imp (EXISTS k in Za | (FORALL i in Za, j in Za | ((i notin k) & (j notin k)) •imp (not (Ra_ABS((F~[i]) •Ra_MINUS (F~[j]))) •Ra_GT Eps)))
(684) Theorem 533: ((Eps in Ra) & (Eps •Ra_GT Ra_0) & (F in RaCauchy)) •imp (EXISTS k in Za | (FORALL i in Za, j in Za | ((i notin k) & (j notin k)) •imp (Eps •Ra_GT (Ra_ABS((F~[i]) •Ra_MINUS (F~[j])))) ))
(686) Theorem 535: ({F,G} •incin RaSeq) •imp (((F •Ras_PLUS G) in RaSeq) & (Ras_ABS(G) in RaSeq) & (Ras_Rev(G) in RaSeq) & ((F •Ras_TIMES G) in RaSeq) & ((F •Ras_PLUS G) = {[u,((F~[u]) •Ra_PLUS (G~[u]))]: u in Za}) & (Ras_ABS(G) = {[u,Ra_ABS(G~[u])]: u in Za}) & (Ras_Rev(G) = {[u,Ra_Rev(G~[u])]: u in Za}) & ((F •Ras_TIMES G) = {[u,((F~[u]) •Ra_TIMES (G~[u]))]: u in Za}))
(687) Theorem 536: (({F1,G1} •incin RaSeq) & (N in Za)) •imp ((F1~[N] in Ra) & (G1~[N] in Ra) & ((F1 •Ras_PLUS G1 in RaSeq) & ((F1 •Ras_PLUS G1)~[N] = (F1~[N]) •Ra_PLUS (G1~[N]))) & (((Ras_ABS(G1) in RaSeq) & (Ras_ABS(G1)~[N] = Ra_ABS(G1~[N])))) & (((Ras_Rev(G1) in RaSeq) & (Ras_Rev(G1)~[N] = Ra_Rev(G1~[N])))) & (((F1 •Ras_TIMES G1 in RaSeq) & (F1 •Ras_TIMES G1)~[N] = ((F1~[N]) •Ra_TIMES (G1~[N])))))
(692) Theorem 541: (F in RaCauchy) •imp (EXISTS x in Ra | (FORALL y in range(F) | Ra_ABS(y) •Ra_LT x ))
(694) Theorem 543: ((G in RaCauchy) & (not Ra_eqseq(G,Ra0Seq))) •imp (EXISTS eps in Ra | (eps •Ra_GT Ra_0) & Finite({i in Za | eps •Ra_GE Ra_ABS(G~[i])}))
(695) Theorem 544: ((G in RaCauchy) & (not Ra_eqseq(G,Ra0Seq))) •imp (EXISTS eps in Ra, n in Za | (eps •Ra_GT Ra_0) & (FORALL i in (Za - n) | (Ra_ABS(G~[i]) •Ra_GT eps) & (Ra_ABS(G~[i]) •Ra_GT Ra_0)) & (Ra_ABS(G~[n]) •Ra_GT Ra_0))
(696) Theorem 545: ((H in RaCauchy) & (not Ra_eqseq(H,Ra0Seq))) •imp (EXISTS eps in Ra, n in Za | (eps •Ra_GT Ra_0) & (FORALL i in (Za - n) | Ra_ABS(H~[i]) •Ra_GT eps) & (FORALL i in Za, j in Za | ((i notin n) & (j notin n)) •imp (eps •Ra_GT (Ra_ABS((H~[i]) •Ra_MINUS (H~[j]))))))
(730) Theorem 579: [All terms of a Cauchy sequence not equivalent to zero have the same sign and have an absolute value bounded below beyond a certain point] ((F in RaCauchy) & (not Ra_eqseq(F,Ra0Seq))) •imp (EXISTS eps in Ra, n in Za | (eps •Ra_GT Ra_0) & (FORALL i in (Za - n) | (Ra_ABS(F~[i]) •Ra_GT eps) & (Ra_ABS(F~[i]) = if ((F~[n]) •Ra_GE Ra_0) then (F~[i]) else Ra_Rev(F~[i]) end if) ))
(855) Theorem 702: (X in Ra) •imp (Ra_is_nonneg(X) •eq Ra_eqseq(Za •PROD {Ra_ABS(X)},Za •PROD {X}))
(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))))
(864) Theorem 710a: [The images of rationals via the embedding form a dense subset of the reals, 1] ((X in Re) & (Eps in Ra) & (Eps •Ra_GT Ra_0)) •imp (EXISTS y in Ra | Finite({m in Za | Ra_ABS(((arb(X))~[m]) •Ra_MINUS y) •Ra_GE Eps}) )
(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))))