List of theorems referencing the symbol RED
(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))
(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))
(449) Theorem 356: [Reduction of an integer pair (n,n) always gives the signed 0 value] (N in Za) •imp (Red([N,N]) = [0,0])
(450) Theorem 357: [Reduction removes any common value added to the components of an integer pair] ((J in Za) & (K in Za) & (M in Za)) •imp (Red([J •PLUS M,K •PLUS M]) = Red([J,K]))
(452) Theorem 359: [The signed sum of two integer pairs is the sum of the first with the reduced form of the second] ((J in Za) & (K in Za) & (N in Za) & (M in Za)) •imp ([J,K] •S_PLUS [N,M] = [J,K] •S_PLUS Red([N,M]))
(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]))
(458) Theorem 365: [The sum of two integer pairs remains the same if the first is reduced] ((J in Za) & (K in Za) & (N in Za) & (M in Za)) •imp ([J,K] •S_PLUS [N,M] = Red([J,K]) •S_PLUS [N,M])
(459) Theorem 366: [The sum of two integer pairs remains the same if both are reduced] ((J in Za) & (K in Za) & (N in Za) & (M in Za)) •imp ([J,K] •S_PLUS [N,M] = Red([J,K]) •S_PLUS Red([N,M]))
(463) Theorem 370: [Reduction of a pair (N,0) gives (N,0)] (N in Za) •imp (Red([N,0]) = [N,0])
(465) Theorem 372: [Sign-reversal of signed integers] ((N in Za) & (M in Za)) •imp (S_Rev(Red([M,N])) = Red([N,M]))