List of theorems referencing the symbol SI
(442) Theorem 349: [Reduced form of an integer pair] ((M in Za) & (N in Za)) •imp ((Red([M,N]) in Si) & (M * N in Za))
(443) Theorem 350: [Embedding of integers in the signed integers] (N in Za) •imp (([N,0] in Si) & ([0,N] in Si))
(444) Theorem 351: [Basic properties of the signed integers 0,1, and -1] ([0,0] in Si) & ([1,0] in Si) & ([0,1] in Si) & ([1,0] /= [0,0]) & ([0,1] /= [0,0]) & ([1,0] /= [0,1])
(445) Theorem 352: [The signed integers as integer pairs with one component equal to 0] (N in Si) •imp ((N = [car(N),cdr(N)]) & (car(N) = 0 or cdr(N) = 0) & (car(N) in Za) & (cdr(N) in Za) & (Red(N) = N) & (car(N) * cdr(N) = 0))
(446) Theorem 353: [Signed integers as integer pairs, 2] (N in Si) •imp ((N = [car(N),0] or N = [0,cdr(N)]) & (car(N) = 0 or cdr(N) = 0) & (car(N) in Za) & (cdr(N) in Za) & (Red(N) = N) & (car(N) * cdr(N) = 0))
(447) Theorem 354: ((N in Si) & (M in Si)) •imp ((N •S_PLUS M in Si) & (N •S_TIMES M in Si))
(448) Theorem 355: [Sign reversal and subtraction for signed integers] ((N in Si) & (M in Si)) •imp ((S_Rev(M) in Si) & (N •S_MINUS M in Si))
(453) Theorem 360: [The sum of a signed integer and an integer pair remains the same if the pair is reduced] ((K in Si) & (N in Za) & (M in Za)) •imp (K •S_PLUS [N,M] = K •S_PLUS Red([N,M]))
(454) Theorem 361: [The product of a signed integer and an integer pair remains the same if the pair is reduced] ((K in Si) & (N in Za) & (M in Za)) •imp (K •S_TIMES [N,M] = K •S_TIMES Red([N,M]))
(455) Theorem 362: [Commutativity lemma for signed integers] ((K in Si) & (N in Za) & (M in Za)) •imp (K •S_PLUS [N,M] = [N,M] •S_PLUS K)
(457) Theorem 364: [Commutative law for signed integer addition] ((N in Si) & (M in Si)) •imp (N •S_PLUS M = M •S_PLUS N)
(460) Theorem 367: [Commutative law for signed integer multiplication] ((N in Si) & (M in Si)) •imp (N •S_TIMES M = M •S_TIMES N)
(461) Theorem 368: [Associative law for signed integer addition] ((K in Si) & (N in Si) & (M in Si)) •imp (N •S_PLUS (M •S_PLUS K) = (N •S_PLUS M) •S_PLUS K)
(462) Theorem 369: [Distributive law for signed integers] ((K in Si) & (N in Si) & (M in Si)) •imp (N •S_TIMES (M •S_PLUS K) = (N •S_TIMES M) •S_PLUS (N •S_TIMES K))
(466) Theorem 373: [n*-m=-(n*m) for signed integers] ((N in Si) & (M in Si)) •imp (N •S_TIMES S_Rev(M) = S_Rev(N •S_TIMES M))
(467) Theorem 374: [Basic properties of the signed negative] (N in Si) •imp ((S_Rev(N) in Si) & (S_Rev(N) •S_PLUS N = [0,0]) & (S_Rev(S_Rev(N)) = N))
(468) Theorem 375: [Inversion lemma] ((N in Si) & (M in Si)) •imp ((S_Rev(N •S_TIMES M) = S_Rev(N) •S_TIMES M) & (S_Rev(N •S_TIMES M) = N •S_TIMES S_Rev(M)))
(469) Theorem 376: [Inversion lemma II] (N in Si) •imp (S_Rev(S_Rev(N)) = N)
(471) Theorem 378: [Associativity lemma] ((K in Si) & (N in Za) & (M in Za)) •imp ([N,0] •S_TIMES ([M,0] •S_TIMES K) = ([N,0] •S_TIMES [M,0]) •S_TIMES K)
(472) Theorem 379: [Associativity lemma II] ((K in Si) & (N in Za) & (M in Si)) •imp ([N,0] •S_TIMES (M •S_TIMES K) = ([N,0] •S_TIMES M) •S_TIMES K)
(473) Theorem 380: [Associative law] ((K in Si) & (N in Si) & (M in Si)) •imp (N •S_TIMES (M •S_TIMES K) = (N •S_TIMES M) •S_TIMES K)
(474) Theorem 381: [Subtraction is addition of the negative] ((N in Si) & (M in Si)) •imp ((N •S_MINUS M) = (N •S_PLUS S_Rev(M)))
(475) Theorem 382: [Subtraction reverses signed integer addition] ((N in Si) & (M in Si)) •imp (N = M •S_PLUS (N •S_MINUS M))
(476) Theorem 383: [The negative of a sum is the sum of the negatives] ((N in Si) & (M in Si)) •imp (S_Rev(N •S_PLUS M) = S_Rev(N) •S_PLUS S_Rev(M))
(477) Theorem 384: [Basic properties of the signed integers 0 and 1] (([0,1] •S_TIMES [0,1]) = [1,0]) & ((X in Si) •imp ((([1,0] •S_TIMES X) = X) & (([0,0] •S_TIMES X) = [0,0])))
(478) Theorem 385: [1 is the multiplicative unit for signed integers] (K in Si) •imp (K •S_TIMES [1,0] = K)
(479) Theorem 386: [The negative of a signed integer is its product by -1] ((K in Si) & (M in Si)) •imp (K •S_MINUS M = K •S_PLUS (M •S_TIMES [0,1]))
(480) Theorem 387: [A signed integer minus itself gives 0] (K in Si) •imp (K •S_MINUS K = [0,0])
(481) Theorem 388: [0 is the right additive identity for signed integers] (K in Si) •imp (K •S_PLUS [0,0] = K)
(482) Theorem 389: [0 is the left additive identity for signed integers] (K in Si) •imp ([0,0] •S_PLUS K = K)
(483) Theorem 390: [Si is an Integral Domain] ((N in Si) & (M in Si) & ((M •S_TIMES N) = [0,0])) •imp ((M = [0,0]) or (N = [0,0]))
(484) Theorem 391: [Distributivity of multiplication over subtraction] ((N in Si) & (M in Si) & (K in Si)) •imp ((m •S_TIMES n) •S_MINUS (k •S_TIMES n) = (m •S_MINUS k) •S_TIMES n)
(485) Theorem 392: [Si multiplicative cancellation] ((N in Si) & (M in Si) & (K in Si) & (M •S_TIMES N = K •S_TIMES N) & (N /= [0,0])) •imp (M = K)
(486) Theorem 393: [Multiplication by -1] (N in Si) •imp (S_Rev(N) = [0,1] •S_TIMES N)
(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])))
(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))
(564) Theorem 414: [Fractions are pairs of signed integers with non-zero denominator] (X in Fr) •eq ((X = [car(X),cdr(X)]) & (car(X) in Si) & (cdr(X) in Si) & (cdr(X) /= [0,0]))
(565) Theorem 415: [Fractions are pairs of signed integers with non-zero denominator, 2] ((X in Si) & (Y in Si)) •imp (([X,Y] in Fr) •eq (Y /= [0,0]))
(566) Theorem 416: [Rational numbers are classes of pairs of signed integers] (N in Ra) •imp ((arb(N) in Fr) & (arb(N) = [car(arb(N)),cdr(arb(N))]) & (car(arb(N)) in Si) & (cdr(arb(N)) in Si) & (cdr(arb(N)) /= [0,0]))
(570) Theorem 421: [The sum of a rational number and a formal fraction can be expressed as a sum of formal fractions] ((X in Ra) & (Y in Si) & (Z in Si) & (Z /= [0,0])) •imp (X •Ra_PLUS Fr_to_Ra([Y,Z]) = Fr_to_Ra([(car(arb(X)) •S_TIMES Z) •S_PLUS (cdr(arb(X)) •S_TIMES Y),(cdr(arb(X)) •S_TIMES Z)]))
(571) Theorem 422: [The product of a rational number and a formal fraction can be expressed as a product of formal fractions] ((X in Ra) & (Y in Si) & (Z in Si) & (Z /= [0,0])) •imp (X •Ra_TIMES Fr_to_Ra([Y,Z]) = Fr_to_Ra([car(arb(X)) •S_TIMES Y,cdr(arb(X)) •S_TIMES Z]))
(578) Theorem 429: [?] ((X in Ra) & (Y in Si) & (Z in Si) & (Z /= [0,0])) •imp (Fr_to_Ra([Y,Z]) •Ra_PLUS X = Fr_to_Ra([(car(arb(X)) •S_TIMES Z) •S_PLUS (cdr(arb(X)) •S_TIMES Y),(cdr(arb(X)) •S_TIMES Z)]))
(578+) Theorem 430: [?] ((X in Si) & (Y in Si) & (Z in Si) & (W in Si) & (Y /= [0,0]) & (W /= [0,0])) •imp (Fr_to_Ra([X,Y]) •Ra_PLUS Fr_to_Ra([Z,W]) = Fr_to_Ra([(X •S_TIMES W) •S_PLUS (Z •S_TIMES Y),Y •S_TIMES W]))
(580) Theorem 432: [?] ((X in Ra) & (Y in Si) & (Z in Si) & (Z /= [0,0])) •imp ((Fr_to_Ra([Y,Z]) •Ra_TIMES X) = Fr_to_Ra([car(arb(X)) •S_TIMES Y,cdr(arb(X)) •S_TIMES Z]))
(588) Theorem 440: [Muliplication of numerator and denominator by a common nonzero function does not change the rational number it represents] ((K in Si) & (N in Si) & (M in Si) & (K /= [0,0]) & (M /= [0,0])) •imp (Fr_to_Ra([N,M]) = Fr_to_Ra([K •S_TIMES N,K •S_TIMES M]))
(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))
(591) Theorem 443: [The unit and zero signed signed integers addition] ([1,0] in Si) & ([0,0] in Si) & ([1,0] /= [0,0]) & ([[0,0],[1,0]] in Fr) & ([[1,0],[1,0]] in Fr)
(612) Theorem 464: [Reversing the numerators of two equivalent rational fractions leaves them equivalent] ((X in Si) & (Y in Si) & (XP in Si) & (YP in Si) & Same_frac([X,Y],[XP,YP])) •imp Same_frac([S_Rev(X),Y],[S_Rev(XP),YP])
(613) Theorem 465: [Alternate form of Theorem 464] ((X in Si) & (Y in Si) & (Y /= [0,0])) •imp (Ra_Rev(Fr_to_Ra([X,Y])) = Fr_to_Ra([S_Rev(X),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))))
(866) Theorem 712: [The embedding of signed integers into rationals preserves all elementary algebraic operations, 2] ((X in Si) & (Y in Si)) •imp ((RaSi(X) in Ra) & (RaSi(Y) in Ra) & (RaSi(X •S_PLUS Y) = RaSi(X) •Ra_PLUS RaSi(Y)) & (RaSi(X •S_TIMES Y) = RaSi(X) •Ra_TIMES RaSi(Y)))
(867) Theorem 713: [The embedding of signed integers into rationals preserves all elementary algebraic operations, 3] ((X in Si) & (Y in Si)) •imp (RaSi(X •S_MINUS Y) = RaSi(X) •Ra_MINUS RaSi(Y))
(868) Theorem 714: [The embedding of signed integers into rationals is 1-1] ((X in Si) & (Y in Si)) •imp ((RaSi(X) = RaSi(Y)) •eq (X = Y))
(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)))
(870) Theorem 717: [The embedding of integers into signed integers preserves all elementary algebraic operations on integers] ((X in Za) & (Y in Za)) •imp ((SiZa(X) in Si) & (SiZa(Y) in Si) & (SiZa(X •PLUS Y) = SiZa(X) •S_PLUS SiZa(Y)) & (SiZa(X •TIMES Y) = SiZa(X) •S_TIMES SiZa(Y)))
(885) Theorem 730: [Any rational r is the quotient of two signed integers, of which the second is positive] (x in Ra) •imp (EXISTS m in Si, n in Si | ((n •S_GE [1,0]) & (x = RaSi(m) •Ra_OVER RaSi(n))))
(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)