List of theorems referencing the symbol DOT_IMP
(4) Theorem 2: [Choice from set of 2] (X in Y) •imp (arb({Y,X}) = X)
(13) Theorem 11: [Pair reconstruction lemma] (U = [A,B]) •imp (U = [car(U),cdr(U)])
(16) Theorem setformer.1: [Equality of setformers] ((x_thryvar notin s) or ((e(x_thryvar) = e0(x_thryvar)) & (P(x_thryvar) •eq PP(x_thryvar)))) •imp ({e(x): x in s | P(x)} = {e0(x): x in s | PP(x)})
(17) Theorem setformer01: [Empty setformer lemma] (s /= 0) •imp ({e(x): x in s} /= 0)
(18) Theorem setformer02: [Empty setformer lemma 2] ({x in s | P(x)} /= 0) •imp ({e(x): x in s | P(x)} /= 0)
(19) Theorem setformer2_1: [Equality of mapformers] (((x_thryvar notin s) or (y_thryvar notin (f(x_thryvar) + fp(x_thryvar)))) or (((f(x_thryvar) = fp(x_thryvar)) & (e2(x_thryvar,y_thryvar) = ep2(x_thryvar,y_thryvar)) & (R(x_thryvar,y_thryvar) •eq PQ(x_thryvar,y_thryvar))))) •imp ({e2(x,y): x in s, y in f(x) | R(x,y)} = {ep2(x,y): x in s, y in fp(x) | PQ(x,y)})
(22) Theorem 12: [Members of ordinals are ordinals] (Ord(S) & (T in S)) •imp Ord(T)
(23) Theorem 13: [Ordinal membership implies inclusion] (Ord(S) & (T in S)) •imp (T •incin S)
(27) Theorem 16: [Key property of ultimate members set] ((X in S) & (Y in X)) •imp (Y in Ult_membs(S))
(28) Theorem 17: [An ordinal is its own set of ultimate members] (Ord(S)) •imp (Ult_membs(S) = S)
(30) Theorem 19: [Ultimate members of an ordinal singleton] Ord(S) •imp (Ult_membs({S}) = S + {S})
(31) Theorem 20: [Ultimate members of the basic infinite set] (X in s_inf) •imp (membs_x(S,{X}) = membs_x(S,X) + Un(membs_x(S,X)))
(32) Theorem 21: [Ultimate members lemma 3] (S •incin Ult_memb1(S)) & (((X in Ult_memb1(S)) & (Y in X)) •imp (Y in Ult_memb1(S)))
(33) Theorem transfinite_induction.1: [Transfinite membership induction] P(mt_thryvar) & ((K in mt_thryvar) •imp (not P(K)))
(34) Theorem 22: [Monotonicity of ultimate members set] (Y in Ult_membs(S)) •imp (Ult_membs(Y) •incin Ult_membs(S))
(35) Theorem 23: [Members of ultimate members are also subsets] (Y in Ult_membs(S)) •imp (Y •incin Ult_membs(S))
(36) Theorem transfinite_member_induction1: [Ultimate members and transfinite induction] P(mt_thryvar) & (mt_thryvar in Ult_membs({n})) & ((K in mt_thryvar) •imp (not P(K)))
(49) Theorem 27: [Ordinal comparison lemma] (Ord(S) & Ord(T) & (T •incin S)) •imp ((T = S) or (T = arb(S - T)))
(50) Theorem 28: [Ordinal intersection] (Ord(S) & Ord(T)) •imp Ord(S * T)
(51) Theorem 29: [Second order comparison lemma] (Ord(S) & Ord(T)) •imp ((S •incin T) or (T •incin S))
(52) Theorem 30: [Ordinal maximum and minimum] (Ord(S) & Ord(T)) •imp (Ord(S + T) & Ord(S * T))
(53) Theorem 31: [Ordinal membership comparison] (Ord(S) & Ord(T)) •imp ((S in T) or (T in S) or (S = T))
(54) Theorem 32: [Successor ordinal] Ord(S) •imp Ord(next(S))
(55) Theorem 33: [Successor ordinal 2] Ord(S) •imp Ord(S + {S})
(56) Theorem 34: [Third ordinal comparison lemma] (Ord(S) & Ord(T)) •imp ((T •incin S) •eq ((T in S) or (T = S)))
(57) Theorem 35: [Ordinal membership and comparison] (Ord(S) & Ord(T)) •imp ((T notin S) •eq (S •incin T))
(58) Theorem 36: [Membership in the successor of an ordinal s] Ord(S) •imp ((T in next(S)) •eq ((T •incin S) & Ord(T)))
(59) Theorem 37: [Membership of s in an ordinal t implies inclusion of next(s) in t] (Ord(T) & (S in T)) •imp (next(S) •incin T)
(63) Theorem 41: [Enumerability principle] ((Ord(X) & S in {enum(y,S): y in X})) •imp (S •incin {enum(y,S): y in X})
(65) Theorem 43: [Enumeration inclusion lemma] ((enum(X,S) = S) & (Y incs X)) •imp (enum(Y,S) = S)
(66) Theorem 44: [The enumeration of a set is 1-1] (Ord(X) & Ord(W) & (X /= W)) •imp (S in {enum(u,S): u in X} or S in {enum(u,S): u in W} or enum(X,S) /= enum(W,S))
(68) Theorem 46: [Main enumeration theorem] (EXISTS x | Ord(x) & (S = {enum(y,S): y in x}) & (FORALL y in x, z0 in x | ((y /= z0) •imp (enum(y,S) /= enum(z0,S)))))
(68+) Theorem 47: [Enumeration single-valuedness principle] (FORALL s | (Ord(enum_Ord(s)) & (s = {enum(y,s): y in enum_Ord(s)}) & (FORALL y in enum_Ord(s), z0 in enum_Ord(s) | ((y /= z0) •imp (enum(y,s) /= enum(z0,s))))))
(72) Theorem 51: [Map members are pairs] (Is_map(F) •imp ((X in F) •imp (X = [car(X),cdr(X)]))) & ((FORALL x in F | x = [car(x),cdr(x)]) •imp Is_map(F))
(73) Theorem 52: [Map subsets are maps] (G •incin F & Is_map(F)) •imp Is_map(G)
(74) Theorem 53: [Single-valued map subsets are single-valued] ((G •incin F) & Svm(F)) •imp Svm(G)
(75) Theorem 54: [One-one map subsets are one-one] ((G •incin F) & one_1_map(F)) •imp one_1_map(G)
(77) Theorem 56: [Map restrictions are maps] Is_map(F) •imp Is_map(F •ON S)
(78) Theorem 57: [Restrictions of single-valed maps are single-valued] Svm(F) •imp Svm(F •ON S)
(79) Theorem 58: [Restrictions of one-one maps are one-one] one_1_map(F) •imp one_1_map(F •ON S)
(81) Theorem 60: [Domain membership lemma] (X in F) •imp (car(X) in domain(F))
(82) Theorem 61: [Range membership lemma] (X in F) •imp (cdr(X) in range(F))
(83) Theorem 62: [Map unions are maps] (Is_map(F) & Is_map(G)) •imp Is_map(F + G)
(86) Theorem 65: [Monotonicity of range and domain sets] (F •incin G) •imp ((range(F) •incin range(G)) & (domain(F) •incin domain(G)))
(92) Theorem 71: [Map image elements belong to the map range] (X in domain(F)) •imp ((F~[X]) in range(F))
(94) Theorem fcn_symbol.2: [Image by a mapformer] (XX in s) •imp (g~[XX] = f(XX))
(96) Theorem fcn_symbol.3: [Elements not in a mapformer domain] (XX notin s) •imp (g~[XX] = 0)
(103) Theorem 73: [Form of a single-valued map range] Svm(F) •imp (F = {[x,F~[x]]: x in domain(F)} & (range(F) = {F~[x]: x in domain(F)}))
(104) Theorem 74: [Map image formula] (Svm(F) & (X in F)) •imp (F~[car(X)] = cdr(X))
(105) Theorem 75: (X in domain(F)) •imp (F~[X] in range(F))
(106) Theorem 76: [Map members are pairs, 2] (Is_map(F) & (U in F)) •imp (U = [car(U),cdr(U)])
(107) Theorem 77: [Map domain member lemma] Is_map(F) •imp ((X in domain(F)) •eq ([X,F~[X]] in F))
(108) Theorem Must_be_svm.1: [Single-valued map former] Svm({[x,b(x)]: x in s}) & (domain({[x,b(x)]: x in s}) = s) & (range({[x,b(x)]: x in s}) = {b(x): x in s}) & ((u in s) •imp ({[x,b(x)]: x in s}~[u] = b(u)))
(114) Theorem 82: [Restriction to a subset] (S incs T) •imp (range(F •ON S) incs range(F •ON T))
(115) Theorem 83: [One-one map-restriction to an intersection] one_1_map(F) •imp (range(F •ON (S * T)) = range(F •ON S) * range(F •ON T))
(117) Theorem 85: [One-one map restriction to disjoint sets] (one_1_map(F) & (S * T = 0)) •imp (range(F •ON S) * range(F •ON T) = 0)
(119) Theorem 87: [Union of single_valued maps] (Svm(F) & Svm(G) & (domain(F) * domain(G) = 0)) •imp Svm(F + G)
(120) Theorem 88: [Union of 1-1 maps] (one_1_map(F) & one_1_map(G) & (range(F) * range(G) = 0) & (domain(F) * domain(G) = 0)) •imp one_1_map(F + G)
(121) Theorem 89: [Union of 1-1 maps, 2] (one_1_map(F + G) & ((G * F) = 0)) •imp ((domain(G) = (domain(F + G) - domain(F))) & (range(G) = (range(F + G) - range(F))))
(122) Theorem 90: [Members of the inverse map] Is_map(F) •imp (([X,Y] in F) •eq ([Y,X] in inv(F)))
(124) Theorem 92: [Doubletons as maps] (X /= Z) •imp ({[X,Y],[Z,W]}~[X] = Y)
(126) Theorem 94: [Range and domain of map product] (range(F @ G) = range(F •ON range(G))) & ((range(G) •incin domain(F)) •imp (domain(F @ G) = domain(G)))
(127) Theorem 95: [Range and domain of map product, 2] (range(G) = domain(F)) •imp ((range(F @ G) = range(F)) & (domain(F @ G) = domain(G)))
(128) Theorem 96: [Range and domain of map product, 3] (range(G) •incin domain(F)) •imp ((range(F @ G) •incin range(F)) & (domain(F @ G) = domain(G)))
(129) Theorem 97: [Range of restriction of one-one map] (one_1_map(F) & (S •incin domain(F)) & (S /= domain(F))) •imp ((range(F •ON S) •incin range(F)) & (range(F •ON S) /= range(F)))
(131) Theorem 99: [Double inverse map] Is_map(F) •imp (F = inv(inv(F)))
(132) Theorem 100: [Inverse of a one-one map] one_1_map(F) •imp (one_1_map(inv(F)) & (F = inv(inv(F))) & (range(inv(F)) = domain(F)) & (domain(inv(F)) = range(F)))
(133) Theorem 101: [Inverse image of an element] (one_1_map(F) & (X in domain(F))) •imp (inv(F)~[F~[X]] = X)
(134) Theorem 102: [Inverse image of an element's map image] one_1_map(F) •imp (((X in domain(F)) •imp (inv(F)~[F~[X]] = X)) & ((X in range(F)) •imp (F~[inv(F)~[X]] = X)))
(138) Theorem 105: [Recursive relationship for the union set] (Un(0) = 0) & ((M /= 0) •imp (Un(M) = (arb(M) + Un(M - {arb(M)}))))
(149) Theorem 110: [Elementary properties of identity maps] one_1_map(ident(S)) & (domain(ident(S)) = S) & (range(ident(S)) = S) & (inv(ident(S)) = ident(S)) & ((X in S) •imp (ident(S)~[X] = X)) & (Is_map(F) •imp (((domain(F) •incin S) •imp (F @ ident(S) = F)) & ((range(F) •incin S) •imp (ident(S) @ F = F))))
(150) Theorem 111: [Composition with an identity map is restriction] (Is_map(F)) •imp (F @ ident(S) = F •ON S)
(151) Theorem 112: [Composition with the inverse map] Svm(F) •imp (F @ inv(F) = ident(range(F)))
(152) Theorem 113: [Inverses of one-one maps] one_1_map(F) •imp (((F @ inv(F)) = ident(range(F))) & ((inv(F) @ F) = ident(domain(F))))
(153) Theorem 114: [Product of inverses lemma] (Is_map(F) & Is_map(G) & (domain(F) •incin range(G)) & Svm(F @ G)) •imp Svm(F)
(154) Theorem 115: [Product of Inverses] (Is_map(F) & Is_map(G)) •imp (inv(F @ G) = inv(G) @ inv(F))
(156) Theorem 117: [An inverse pair of maps must be 1-1 and must be each other's inverses] (Is_map(F) & Is_map(G) & (domain(F) = range(G)) & (range(F) = domain(G)) & (F @ G = ident(range(F))) & (G @ F = ident(domain(F)))) •imp (one_1_map(F) & (G = inv(F)))
(157) Theorem 118: [Single-valued map restrictions as setformers] Svm(F) •imp (((F •ON S) = {[x,F~[x]]: x in domain(F) | x in S}) & (domain(F •ON S) = {x: x in domain(F) | x in S}) & (range(F •ON S) = {F~[x]: x in domain(F) | x in S}))
(158) Theorem 119: [Image of a non-domain element] (X notin domain(F)) •imp ((F~[X]) = 0)
(160) Theorem 121: [Single-valued map restrictions as setformers, 2] Svm(F) •imp (((F •ON S) = {[x,F~[x]]: x in domain(F •ON S)}) & (range(F •ON S) = {F~[x]: x in domain(F •ON S)}))
(161) Theorem 122: [Images under one-one maps] (one_1_map(F) & (X in domain(F)) & (Y in domain(F)) & (F~[X] = F~[Y])) •imp (X = Y)
(162) Theorem 123: [Composition of single-valued maps] (Svm(F) & Svm(G)) •imp Svm(F @ G)
(163) Theorem 124: [Images under single-valued map composition] (Svm(F) & Svm(G) & (X in domain(G)) & (range(G) •incin domain(F))) •imp ((F @ G)~[X] = F~[G~[X]])
(164) Theorem 125: [Single-valued map ranges and domains as set formers] (Svm(F) & Svm(G) & (X in domain(G)) & (range(G) •incin domain(F))) •imp (((F @ G)~[X] = F~[G~[X]]) & (F @ G = {[x,F~[G~[x]]]: x in domain(G)}) & (range(F @ G) = {F~[G~[x]]: x in domain(G)}))
(165) Theorem 126: [Image under single-valued map] (Svm(F) & (G •incin F) & (X in domain(G))) •imp (F~[X]=G~[X])
(166) Theorem 127: [Single-valued and one-one maps] Is_map(F) •imp (one_1_map(F) •eq one_1_map(inv(F)))
(167) Theorem 128: [Composition of one-one maps] (one_1_map(F) & one_1_map(G)) •imp one_1_map(F @ G)
(168) Theorem 129: [Elements are defined uniquely by their one-one images] Svm(F) •imp (one_1_map(F) •eq (FORALL x in domain(F), y in domain(F) | ((F~[x] = F~[y]) •imp (x = y))))
(169) Theorem 130: [A 1-1 map on a set u induces a 1-1 map on the power set of u] (one_1_map(F) & (S •incin domain(F)) & (T •incin domain(F)) & (S /= T)) •imp (range(F •ON S) /= range(F •ON T))
(172) Theorem 133: [Single-valued maps have 1-1 partial inverses] Svm(F) •imp (EXISTS h | ((domain(h) = range(F)) & (range(h) •incin domain(F)) & one_1_map(h)) & (FORALL x in range(F) | (F~[h~[x]] = x)))
(174) Theorem 135: [Members of Cartesian products] (X in (S •PROD T)) •imp ((car(X) in S) & (cdr(X) in T))
(176) Theorem 137: [Image of Cartesian product by a singleton] (U in Z) •imp (((Z •PROD {V})~[U]) = V)
(177) Theorem 138: [Cartesian product disjointness] (A * B = 0) •imp ((X •PROD A) * (Y •PROD B) = 0)
(178) Theorem 139: [Cartesian modified associativity] (F = {[[[x,y],z],[x,[y,z]]]: x in A, y in B, z in C}) •imp (one_1_map(F) & (domain(F) = ((A •PROD B) •PROD C)) & (range(F) = (A •PROD (B •PROD C))))
(179) Theorem 140: [Cartesian modified commutativity] (F = {[[x,y],[y,x]]: x in A, y in B}) •imp (one_1_map(F) & (domain(F) = (A •PROD B)) & (range(F) = (B •PROD A)))
(180) Theorem 141: [Enumeration of an ordinal] (Ord(S) & X in S) •imp (enum(X,S) = X)
(183) Theorem 144: ['arb' is monotone decreasing for non-empty sets of ordinals] (Ord(R) & (R incs S) & (S incs T)) •imp (arb(S) in arb(T) or arb(S) = arb(T) or T = 0)
(184) Theorem 145: [Axiom of choice variant] ((S /= 0) & (FORALL x in S | Ord(x))) •imp (FORALL x in S | x incs arb(S))
(185) Theorem 146: [Lemma for ordinal enumeration] (Ord(S) & (T •incin S) & (X in S) & (Y in X)) •imp (enum(Y,T) in enum(X,T) or enum(X,T) incs T)
(186) Theorem 147: [Subsets of an ordinal enumerate at least as rapidly as the ordinal] (Ord(S) & (T •incin S) & (X in S)) •imp (enum(X,T) incs X or enum(X,T) incs T)
(187) Theorem 148: [Subset enumeration lemma] (Ord(S) & (T •incin S)) •imp ({enum(x,T): x in S} incs T)
(188) Theorem 149: [Second subset enumeration lemma] (Ord(S) & (T •incin S)) •imp (EXISTS x •incin S | (Ord(x) & (T = {enum(y,T): y in x}) & (FORALL y in x, z in x | ((y /= z) •imp (enum(y,T) /= enum(z,T))))))
(189) Theorem 150: [Enumerability lemma] (Ord(S) & (T •incin S)) •imp (EXISTS f in OM | one_1_map(f) & Ord(domain(f)) & (domain(f) •incin S) & (range(f) = T))
(191) Theorem 152: [One-one maps are cardinality preserving] one_1_map(F) •imp (#range(F) = #domain(F))
(199) Theorem 160: [Uniqueness of Cardinality] (Card(C) & (EXISTS f in OM | (one_1_map(f) & (range(f) = S) & domain(f) = C))) •imp (C = #S)
(202) Theorem 163: [Cardinal comparison is transitive] ((#S in #T) & (#T in #R)) •imp (#S in #R)
(203) Theorem 164: [Subsets of an ordinal have a cardinality that is no larger than the ordinal] (Ord(S) & (T •incin S)) •imp (#T •incin S)
(204) Theorem 165: [Subset cardinality theorem] (T •incin S) •imp (#T •incin #S)
(205) Theorem 166: [Single-valued mapping cannot increase cardinality] Svm(F) •imp (#range(F) •incin #domain(F))
(208) Theorem 169: [The cardinality of a single-valued map equals the cardinality of its domain] Svm(F) •imp (#domain(F) = #F)
(209) Theorem 170: [Cardinality of restriction maps] (Svm(F) & (domain(F) incs A)) •imp (#(F •ON A) = #A)
(213) Theorem 173: [Range-decomposition of a map domain] ((S * R = 0) & Svm(G)) •imp (((G •INV_IM S) * (G •INV_IM R)) = 0)
(214) Theorem 174: [Inverse image of a range element] (Y in range(G)) •imp ((G •INV_IM {Y}) /= 0)
(216) Theorem 176: [Single-valued inverse image as a setformer] Svm(inv(G)) •imp (G •INV_IM R = {inv(G)~[w]: w in (R * range(G))})
(217) Theorem 177: [Inverse image of a range element] (one_1_map(G) & (Y in range(G))) •imp (G •INV_IM {Y} = {inv(G)~[Y]})
(219) Theorem 179: [Range of a single-valued map restricted to an inverse image] Svm(G) •imp (range(G •ON (G •INV_IM A)) = range(G) * A)
(220) Theorem 180: [Inverse images by a single-valued map] Svm(G) •imp ((G •ON (G •INV_IM A)) •INV_IM B = (G •INV_IM A) * (G •INV_IM B))
(221) Theorem 181: [Monotonicity of inverse image] (B •incin A) •imp ((G •INV_IM B) •incin (G •INV_IM A))
(224) Theorem 184: [A subset of a finite set is finite] (Finite(S) & (S incs T)) •imp Finite(T)
(225) Theorem 185: [One-one maps preserve finiteness] one_1_map(F) •imp ((Finite(domain(F))) •imp (Finite(range(F))))
(226) Theorem 186: [One-one maps preserve finiteness, 2] one_1_map(F) •imp (Finite(domain(F)) •eq Finite(range(F)))
(227) Theorem 187: [A single_valued map with finite domain has a finite range] (Svm(F) & Finite(domain(F))) •imp Finite(range(F))
(230) Theorem 189: [Proper subsets of a finite set have fewer elements] (Finite(S) & (T •incin S) & (T /= S)) •imp (#T in #S)
(232) Theorem 191: [Members of a finite ordinal are finite] (Ord(S) & Finite(S) & (T in S)) •imp Finite(T)
(233) Theorem 192: [Any infinite ordinal is larger than any finite ordinal] (Ord(S) & Ord(T) & (not Finite(S)) & Finite(T)) •imp (T in S)
(234) Theorem 193: [Interchange lemma] ((X in S) & (Y in S)) •imp (EXISTS f | one_1_map(f) & (range(f) = S) & (domain(f) = S) & ((f~[X]) = Y) & ((f~[Y]) = X))
(236) Theorem 195: [Finiteness of successor set] Finite(S) •imp Finite(next(S))
(241) Theorem 200: [All finite ordinals are cardinals] (Ord(X) & Finite(X)) •imp Card(X)
(244) Theorem setformer_meet_join.3: [Implication in a setformer] (FORALL u in s, v in t | Q(u,v) •imp R(u,v)) •imp ({h(u,v): u in s, v in t | Q(u,v)} •incin {h(u,v): u in s, v in t | R(u,v)})
(246) Theorem setformer_meet_join.5: [Setformer finiteness implication, two-variable case] Finite({[u,v]: u in s, v in t | R(u,v)}) •imp Finite({h(u,v): u in s, v in t | R(u,v)})
(248) Theorem 202: [All integers are finite ordinals and cardinals] (X in Za) •imp ((X = #X) & Card(X) & Ord(X) & Finite(X))
(249) Theorem 203: [Transitivity of integer comparison] (({M,N} •incin Za) & (I in N)) •imp ((M in N) or (I in M))
(251) Theorem 205: [The successor of an integer is an integer] (I in Za) •imp (Card(next(I)) & (next(I) in Za))
(256) Theorem 210: [First Disjoint sum lemma] ((N * M = 0) & (K * J = 0) & (#N = #K) & (#M = #J)) •imp (#(N + M) = #(K + J))
(258) Theorem 212: [Monotonicity of arithmetic addition] ((N incs N1) and (M incs M1)) •imp (N •PLUS M incs N1 •PLUS M1)
(259) Theorem 213: [Disjoint sum lemma] (N * M = 0) •imp (N •PLUS M = #(N + M))
(261) Theorem 215: [Second Disjoint sum lemma] (N * M = 0) •imp (#N •PLUS #M = #(N + M))
(264) Theorem 218: [Cardinality of a Cartesian product union] (A /= B) •imp (#N •PLUS #M = #((N •PROD {A}) + (M •PROD {B})))
(267) Theorem 221: [Arithmetic associativity lemma] ((N * M = 0) & (N * K = 0) & (M * K = 0)) •imp (((N •PLUS M) •PLUS K) = #((N + M) + K))
(268) Theorem 222: [Arithmetic associativity lemma 2] ((N * M = 0) & (N * K = 0) & (M * K = 0)) •imp ((N •PLUS (M •PLUS K)) = #(N + (M + K)))
(274) Theorem 228: [Strict monotonicity of finite cardinality] (Finite(N) & (M •incin N) & (M /= N)) •imp (#M in #N)
(275) Theorem finite_induction1: [Induction principle for finite sets] (m_thryvar •incin n) & P(m_thryvar) & (FORALL k •incin m_thryvar | ((k /= m_thryvar) •imp (not P(k))))
(277) Theorem 230: [Removal of an initial segment from Za yields an infinite set] (N in Za) •imp (not Finite(Za - N))
(278) Theorem 231: [The union of finitely many finite sets is finite] ((FORALL x in S | Finite(x)) & Finite(S)) •imp Finite(Un(S))
(282) Theorem 235: [acyclicity of the closure of membership,2] ((X in Ult_membs({Y})) & (Y in Ult_membs({X}))) •imp (X = Y)
(283) Theorem 236: [existence of an in-maximal set in any finite set] (EXISTS v | Finite(F) •imp (((F = 0) or (v in F)) & ({y in (F-{v}) | v in Ult_membs({y})} = 0)))
(289) Theorem 242: [Monotonicity of multiplication] (M /= 0) •imp (#(N •PROD M) incs #N)
(290) Theorem 243: [Distributivity lemma] (A /= B) •imp (N •PLUS M = #((N •PROD {A}) + (M •PROD {B})))
(293) Theorem 246: [0 is bilateral additive identity] (X in Za) •imp (((X •PLUS 0) = X) & ((0 •PLUS X) = X))
(295) Theorem 248: [Cartesian product monotonicity] ((A •incin B) & (C •incin D)) •imp ((A •PROD C) •incin (B •PROD D))
(300) Theorem 253: [The arithmetic product of two finite sets is finite] (Finite(N) & Finite(M)) •imp Finite(N •TIMES M)
(301) Theorem 254: [The Cartesian product of two finite sets is finite] (Finite(N) & Finite(M)) •imp Finite(N •PROD M)
(307) Theorem 260: [Disjoint additivity lemma] ((N * M = 0) & (N2 * M2 = 0) & (#N = #N2) & (#M = #M2)) •imp (#(N + M) = #(N2 + M2))
(308) Theorem 261: [Excess subtraction lemma] (Ord(Y) & (X in Y)) •imp ((X •MINUS Y) = 0)
(309) Theorem 262: [Subtraction lemma] (M •incin N) •imp (#N = #M •PLUS (N •MINUS M))
(310) Theorem 263: [Subtraction in the non-negative case] (M •incin N) •imp (#N = (N •MINUS M) •PLUS M)
(311) Theorem 264: [Subtraction lemma 2] (#M in #N or #M = #N) •imp (#N = #M •PLUS (#N •MINUS #M))
(312) Theorem 265: [Union set as an upper bound] (FORALL x in S | x •incin Un(S)) & ((FORALL x in S | x •incin T) •imp (Un(S) •incin T))
(313) Theorem 266: [Monotonicity of the union-set operator] (S •incin T) •imp (Un(S) •incin Un(T))
(314) Theorem 267: [The union of a set of ordinals is an ordinal] (FORALL x in S | Ord(x)) •imp Ord(Un(S))
(315) Theorem 268: [Division monotonicity lemma] (M /= 0) •imp ((N •OVER M) •incin N)
(316) Theorem 269: [Extended division monotonicity lemma] ((M /= 0) & (N in Za)) •imp (((N •OVER M) in Za) & ((N •OVER M) •incin N))
(317) Theorem 270: [Closure properties of arithmetic operators] ((N in Za) & (M in Za)) •imp ((N •PLUS M in Za) & (N •TIMES M in Za) & (N •MINUS M in Za))
(318) Theorem 271: [Strict monotonicity of addition] ((M in Za) & (N in Za) & (N /= 0)) •imp (M in (M •PLUS N))
(319) Theorem 272: [Only the nullset has cardinality zero] (#N = 0) •imp (N = 0)
(320) Theorem 273: [Strict monotonicity of addition] ((M in Za) & (N in Za) & (K in N)) •imp (M •PLUS K in M •PLUS N)
(321) Theorem 274: [Strict monotonicity of addition] ((M in Za) & (N in Za) & (K in N)) •imp (M •PLUS K in M •PLUS N)
(322) Theorem 275: [Strict monotonicity of addition, 2] ((M in Za) & (N in Za) & (K in N)) •imp (K •PLUS M in N •PLUS M)
(323) Theorem 276: [Cancellation] ((M in Za) & (N in Za) & (K in Za) & (M •PLUS K = N •PLUS K)) •imp (M = N)
(324) Theorem 277: [Monotonicity of addition] (M •incin N) •imp ((M •PLUS K) •incin (N •PLUS K))
(325) Theorem 278: [Monotonicity of addition, 2] Card(M) •imp ((M •incin (I •PLUS M)) & (M •incin (M •PLUS I)))
(326) Theorem 279: [Monotonicity of addition, 3] (M in Za) •imp ((M •incin (I •PLUS M)) & (M •incin (M •PLUS I)) & ((M •PLUS I) notin M) & ((I •PLUS M) notin M))
(327) Theorem 280: [Monotonicity of multiplication] (M •incin N) •imp ((M •TIMES K) •incin (N •TIMES K))
(328) Theorem 281: [Strict monotonicity of integer multiplication] ((M in N) & (N in Za) & (K in Za) & (K /= 0)) •imp ((M •TIMES K) in (N •TIMES K))
(329) Theorem 282: [The sum of non-negative integers is at least as big at each addend] ((X in Za) & (Y in Za)) •imp ((X •PLUS Y) notin Y)
(330) Theorem 283: [Strict monotonicity of addition] ((M in Za) & (N in Za) & (K in Za)) •imp (((M •PLUS K) •incin (N •PLUS K)) •eq (M •incin N))
(331) Theorem 284: [Strict monotonicity of addition] ((M in Za) & (N in M) & (K in Za)) •imp ((N •PLUS K) in (M •PLUS K))
(332) Theorem 285: [Subtraction Lemma] (N in Za) •imp ((N •MINUS M) in Za)
(333) Theorem 286: [Strict monotonicity of subtraction] ((N in Za) & (M in Za) & (K in N) & (M incs N)) •imp ((M •MINUS N) in (M •MINUS K))
(334) Theorem 287: [Monotonicity of subtraction] (K incs M) •imp ((K •MINUS N) incs (M •MINUS N))
(335) Theorem 288: [Monotonicity of subtraction, 2] (M incs N) •imp ((K •MINUS N) incs (K •MINUS M))
(336) Theorem 289: [Strict monotonicity of subtraction, 2] ((N in Za) & (M in Za) & (K in M) & (K incs N)) •imp ((K •MINUS N) in (M •MINUS N))
(337) Theorem 290: [Addition-subtraction commutativity] ((M in Za) & (N in Za) & (K in Za) & (N incs M) & ((N •MINUS M) incs K)) •imp ((N incs (M •PLUS K)) & (N •MINUS (M •PLUS K) = (N •MINUS M) •MINUS K))
(338) Theorem 291: [Subtraction reverses addition] ((M in Za) & (N in Za)) •imp ((M •PLUS N) •MINUS N = M)
(340) Theorem 293: [Integer division with remainder] ((M in Za) & (N in Za) & (N /= 0)) •imp (((M •OVER N) in Za) & (M incs ((M •OVER N) •TIMES N)) & ((M •MOD N) in N))
(342) Theorem 295: [Subtraction monotonicity lemma] (N incs M) •imp ((N •MINUS K) incs (M •MINUS K))
(343) Theorem 296: [Cardinality of set difference] (Finite(N) & (N incs M)) •imp (#(N - M) = #(#N - #M))
(344) Theorem 297: [Strong monotonicity of integer addition] ((N in Za) & (M in Za) & (K in Za)) •imp ((N incs M) •eq ((N •PLUS K) incs (M •PLUS K)))
(345) Theorem 298: [Addition reverses subtraction] (N incs M) •imp (#N = #M •PLUS #(N - M))
(346) Theorem 299: [Addition-subtraction commutativity, 2] ((N in Za) & (M in Za) & (K in Za) & (N incs M)) •imp ((N •PLUS K) •MINUS (M •PLUS K) = N •MINUS M)
(347) Theorem 300: [Addition-subtraction lemma] ((N in Za) & (M in Za)) •imp (N = (M •PLUS (N •MINUS M)) or N = (M •MINUS (M •MINUS N)))
(349) Theorem 302: [The successor integer as a sum, 2] (N in Za) •imp ((next(N) in Za) & ((N •PLUS 1) = next(N)))
(350) Theorem 303: [The union set of a finite collection of integers is an integer] ((M •incin Za) & Finite(M)) •imp (((M /= 0) •imp (Un(M) in M)) & (Un(M) in Za))
(351) Theorem 304: [The union set of a set of integers is the least upper bound of its elements] (M in Za) •imp (((Un(M) in Za) & (Un(M) •incin M)) & ((M /= 0) •imp (Un(M) in M)))
(352) Theorem 305: [Every nonzero integer has a predecessor] ((M in Za) & (M /= 0)) •imp (M = (Un(M) •PLUS 1))
(353) Theorem 306: [The sum of integers as the union of smaller sums] ((X in Za) & (Y in Za)) •imp ((X •PLUS Y) = X + {(X •PLUS u): u in Y})
(354) Theorem 307: [The sum of integers as the union of smaller sums, 2] ((X in Za) & (Y in Za)) •imp ((X •PLUS Y) = X + {(u •PLUS X): u in Y})
(355) Theorem 308: [Subtraction reverses addition] ((X in Za) & (Y in Za) & (Y •incin X)) •imp (X = Y •PLUS (X •MINUS Y))
(356) Theorem 309: [Subtraction monotonicity lemma, 2] ((X in Za) & (Y in Za) & (U in (X •PLUS Y)) & (Y /= 0)) •imp ((U •MINUS X) in Y)
(357) Theorem 310: [The integer difference as a set of smaller differences] ((N in Za) & (M in Za)) •imp ((N •MINUS M) = {k •MINUS M: k in N | M •incin k})
(358) Theorem 311: [The integer difference as a set of smaller differences] ((N in Za) & (M in Za)) •imp ((N •MINUS M) = {k in Za | (k •PLUS M) in N})
(359) Theorem 312: ((J in Za - X) & (FORALL i | (next(i) in X) •imp (i in X))) •imp ({h in Za | (h notin J) & (h in X)} = 0)
(360) Theorem 313: ((X •incin Za) & (FORALL i | (next(i) in X) •imp (i in X))) •eq (X in next(Za))
(361) Theorem 314: (({X,Y} •incin next(Za)) & (#X in next(Y))) •imp (((X = Y) & (Y = Za)) or (X in (next(Y) * Za)))
(362) Theorem unsigned_integer_bynd.0: [Every finite set of unsigned integers has an upper bound] (bynd_thryvar in Za) & (FORALL i in Za | (Q1(i) •imp (i in bynd_thryvar)))
(363) Theorem unsigned_integer_bynd.1: [Every finite set of unsigned integers has an upper bound] (bynd_thryvar in Za) & (Za incs bynd_thryvar) & Ord(bynd_thryvar) & (FORALL i in Za | (Q1(i) •imp (i in bynd_thryvar))) & (not Finite(Za - bynd_thryvar))
(365) Theorem 315: [Ordinal member maximum and minimum] (Ord(U) & (S in U) & (T in U)) •imp ((S + T in U) & (S * T in U))
(366) Theorem 316: [Integer member maximum and minimum] ((S in Za) & (T in Za)) •imp ((S + T in Za) & (S * T in Za))
(367) Theorem cauchyseq_lemma2.1: (EXISTS k in Za | (FORALL i in Za, j in Za | ((i incs k) & (j incs k)) •imp (not (R(i,j)))))
(368) Theorem 317: ((N in Za) & (S •incin N) & (#S = N)) •imp (S = N)
(370) Theorem 319: [Other properties of finite sequences] (F in Fin_seqs(S)) •imp ((domain(F) = #domain(F)) & (domain(F) = #F) & (#F in Za) & Finite(F))
(371) Theorem 320: [Two single-valued functions with common domain are equal if all their values are equal] (Svm(F) & Svm(G) & (domain(F) = S) & (domain(G) = S) & (FORALL n0 in S | F~[n0] = G~[n0])) •imp (F = G)
(372) Theorem 321: [Two functions from a collection of single-valued functions with common domain are equal if all their values are equal] ((S /= 0) & (FORALL h in Mapset | ((domain(h) = S) & Svm(h)))) •imp ((FORALL n in S | ((F in Mapset) & (G in Mapset) & (F~[n] = G~[n]))) •imp (F = G))
(373) Theorem 322: [The shift-map of an integer is single-valued and maps Za into Za] ((M in Za) & (N in Za)) •imp (Svm(Shift(M)) & (domain(Shift(M)) = Za) & (range(Shift(M)) •incin Za) & (Shift(M)~[N] = M •PLUS N))
(374) Theorem 323: [Composition of shift-maps yields a shift-map] ((M in Za) & (N in Za)) •imp (Shift(M) @ Shift(N) = Shift(M •PLUS N))
(375) Theorem 324: [Double shifting can be emulated by a single shift] ((M in Za) & (N in Za)) •imp (shifted_seq(shifted_seq(F,M),N) = shifted_seq(F,M •PLUS N))
(376) Theorem 325: [Shift(0) is the identity map on Za] (Shift(0) = {[n,n]: n in Za}) & ((Is_map(F) & (domain(F) •incin Za)) •imp (F @ Shift(0) = F))
(377) Theorem 326: [Shift-by-0 is the identity map on sequences] (Is_map(F) & (domain(F) •incin Za)) •imp (shifted_seq(F,0) = F)
(378) Theorem 327: [Form of a shifted sequence] ((M in Za) & (domain(F) •incin Za)) •imp (shifted_seq(F,M) = {[car(x) •MINUS M,cdr(x)]: x in F | car(x) incs M})
(379) Theorem 328: [Properties of finite and shifted finite sequences] ((F in Fin_seqs(S)) & (G in Fin_seqs(S))) •imp (Svm({[car(x) •PLUS #F, cdr(x)]: x in G}) & (domain(F) * domain({[car(x) •PLUS #F, cdr(x)]: x in G}) = 0))
(380) Theorem 329: ((F in Fin_seqs(S)) & (M in Za)) •imp (((F •ON M) in Fin_seqs(S)) & (shifted_seq(F,M) in Fin_seqs(S)) & (domain(shifted_seq(F,M)) = (#F •MINUS M)))
(381) Theorem 330: [Concatenation of finite sequences] ((F in Fin_seqs(S)) & (G in Fin_seqs(S))) •imp ((concat(F,G) in Fin_seqs(S)) & (domain(concat(F,G)) = domain(F) •PLUS domain(G)) & (range(concat(F,G)) = range(F) + range(G))) & ((U in domain(F) •PLUS domain(G)) •imp (concat(F,G)~[U] = if U in domain(F) then F~[U] else G~[U •MINUS domain(F)] end if))
(382) Theorem 331: [0 is bilateral unit for sequence concatenation] (F in Fin_seqs(S)) •imp ((concat(F,0) = F) & (concat(0,F) = F))
(383) Theorem 332: [Associativity of sequence concatenation] ((F in Fin_seqs(S)) & (G in Fin_seqs(S)) & (H in Fin_seqs(S))) •imp (concat(F,concat(G,H)) = concat(concat(F,G),H))
(384) Theorem 333: [Concatenation of shifted sequences] ((F in Fin_seqs(S)) & (M in domain(F))) •imp ((shifted_seq(F,M) in Fin_seqs(S)) & (F = concat((F •ON M), shifted_seq(F,M))))
(385) Theorem subseq.1: (g = (f @ h_thryvar)) & one_1_map(h_thryvar) & (domain(h_thryvar) in next(Za)) & (range(h_thryvar) •incin domain(f)) & (FORALL i in domain(h_thryvar), j in domain(h_thryvar) | (i in j) •imp ((h_thryvar~[i]) in (h_thryvar~[j])))
(388) Theorem subseq.4: (domain(h_thryvar) /= Za) •imp Finite(g)
(389) Theorem 334: ((F in Fin_seqs(S)) & (G in Subseqs(F))) •imp ((G in Fin_seqs(S)) & (domain(G) in next(domain(F))))
(390) Theorem 335: (M in Za) •imp (shifted_seq(F,M) in Subseqs(F))
(391) Theorem 336: ((F in Fin_seqs(S)) & (M in Za)) •imp ((shifted_seq(F,M) in Fin_seqs(S)) & (domain(shifted_seq(F,M)) in next(domain(F))))
(392) Theorem 337: ((domain(F) = Za) & (M in Za)) •imp (domain(shifted_seq(F,M)) = Za)
(395) Theorem ordval_fcn3: (FORALL x in rng_thryvar, y in s | (f(x) = f(y)) •imp (y in rng_thryvar))
(396) Theorem well_founded_set.0: ((X in s) & (Y in s)) •imp ((not(arg1_bef_arg2(X,Y) & arg1_bef_arg2(Y,X))) & (not arg1_bef_arg2(X,X)))
(398) Theorem well_founded_set.0a: ((T •incin s) & (T /= 0)) •imp ((Minrel_thryvar(T) in T) & (FORALL y in T | (not arg1_bef_arg2(y,Minrel_thryvar(T)))))
(399) Theorem well_founded_set.0b: [Monotonicity of Minrel_thryvar] ((R •incin s) & (T •incin R) & (T /= 0)) •imp (not(arg1_bef_arg2(Minrel_thryvar(T),Minrel_thryvar(R))))
(400) Theorem well_founded_set.0c: ((S incs T) & (T /= 0)) •imp (Minrel_thryvar(T) in T)
(402) Theorem well_founded_set.1: (not(s •incin {ordenm_thryvar(y): y in X})) •imp ((ordenm_thryvar(X) in (s - {ordenm_thryvar(y): y in X})) & (FORALL y in (s - {ordenm_thryvar(y): y in X}) | not(arg1_bef_arg2(y,ordenm_thryvar(X)))))
(404) Theorem well_founded_set.3: (ordenm_thryvar(X) /= s) •imp (ordenm_thryvar(X) in s)
(405) Theorem well_founded_set.5: [Ordinal enumeration is monotone on ordinals] (Ord(U) & Ord(V) & (ordenm_thryvar(U) /= s) & arg1_bef_arg2(ordenm_thryvar(U),ordenm_thryvar(V))) •imp (U in V)
(407) Theorem well_founded_set.7: [Well-ordering is initially 1-1] (Ord(U) & Ord(V) & (ordenm_thryvar(U) /= s) & (ordenm_thryvar(V) /= s) & (U /= V)) •imp (ordenm_thryvar(U) /= ordenm_thryvar(V))
(410) Theorem well_ordered_set.0: ((X in s) & (Y in s)) •imp (arg1_bef_arg2(X,Y) or arg1_bef_arg2(Y,X) or (X = Y))
(411) Theorem well_ordered_set.0a: ((T •incin s) & (T /= 0)) •imp (EXISTS x in T | (FORALL y in T | (not arg1_bef_arg2(y,x))))
(412) Theorem well_ordered_set.100: (FORALL x,y | ((x in s) & (y in s)) •imp ((not (arg1_bef_arg2(x,y) & arg1_bef_arg2(y,x))) & (not arg1_bef_arg2(x,x)))) & (FORALL x | (not(s •incin {ordenm_thryvar(y): y in x})) •imp ((ordenm_thryvar(x) in (s - {ordenm_thryvar(y): y in x})) & (FORALL y in (s - {ordenm_thryvar(y): y in x}) | not(arg1_bef_arg2(y,ordenm_thryvar(x)))))) & (FORALL x | (s •incin {ordenm_thryvar(y): y in x}) •eq (ordenm_thryvar(x) = s)) & (FORALL x | (ordenm_thryvar(x) /= s) •imp (ordenm_thryvar(x) in s)) & (FORALL u, v | (Ord(u) & Ord(v) & (ordenm_thryvar(u) /= s) & arg1_bef_arg2(ordenm_thryvar(u),ordenm_thryvar(v))) •imp (u in v)) & (FORALL v | {u: u in s | arg1_bef_arg2(u,ordenm_thryvar(v))} •incin {ordenm_thryvar(x): x in v}) & (FORALL u, v | (Ord(u) & Ord(v) & (ordenm_thryvar(u) /= s) & (ordenm_thryvar(v) /= s) & (u /= v)) •imp (ordenm_thryvar(u) /= ordenm_thryvar(v))) & (EXISTS o in next(#pow(s)) | (Ord(o) & (s = {ordenm_thryvar(x): x in o}) & (FORALL x in o | (ordenm_thryvar(x) /= s)) & one_1_map({[x,ordenm_thryvar(x)]: x in o}))) & (FORALL x | ordenm_thryvar(x) = Minrel_thryvar(s - {ordenm_thryvar(y): y in x})) & (FORALL t | Minrel_thryvar(t) = if (t •incin s) & (t /= 0) then arb({m: m in t | (FORALL y in t | (not arg1_bef_arg2(y,m)))}) else s end if)
(412+) Theorem well_ordered_set.10: ((X in s) & (Y in s)) •imp ((arg1_bef_arg2(X,Y) •imp (not arg1_bef_arg2(Y,X))) & (not arg1_bef_arg2(X,X)))
(413) Theorem well_ordered_set.1: (not(s •incin {ordenm_thryvar(y): y in X})) •imp ((ordenm_thryvar(X) in (s - {ordenm_thryvar(y): y in X})) & (FORALL y in (s - {ordenm_thryvar(y): y in X}) | not(arg1_bef_arg2(y,ordenm_thryvar(X)))))
(415) Theorem well_ordered_set.3: ((ordenm_thryvar(X) /= s) •imp (ordenm_thryvar(X) in s))
(416) Theorem well_ordered_set.5a: (Ord(U) & Ord(V) & (ordenm_thryvar(U) /= s) & arg1_bef_arg2(ordenm_thryvar(U),ordenm_thryvar(V))) •imp (U in V)
(418) Theorem well_ordered_set.7: ((Ord(U) & Ord(V) & (ordenm_thryvar(U) /= s) & (ordenm_thryvar(V) /= s) & (U /= V)) •imp (ordenm_thryvar(U) /= ordenm_thryvar(V)))
(422) Theorem well_ordered_set.5: [Any well-ordering is isomorphic to an ordinal enumeration] (Ord(U) & Ord(V) & (ordenm_thryvar(U) /= s) & (ordenm_thryvar(V) /= s)) •imp (arg1_bef_arg2(ordenm_thryvar(U),ordenm_thryvar(V)) •eq (U in V))
(423) Theorem well_ordered_set.6: (Ord(V) & (ordenm_thryvar(V) /= s)) •imp ({u: u in s | arg1_bef_arg2(u,ordenm_thryvar(V))} = {ordenm_thryvar(x): x in V})
(424) Theorem well_ordered_set.9: (Ord(V) & (ordenm_thryvar(V) /= s)) •imp ( one_1_map({[x,ordenm_thryvar(x)]: x in V}) & (domain({[x,ordenm_thryvar(x)]: x in V}) = V) & (range({[x,ordenm_thryvar(x)]: x in V}) = {u: u in s | arg1_bef_arg2(u,ordenm_thryvar(V))}) & ({u: u in s | arg1_bef_arg2(u,ordenm_thryvar(V))} = {ordenm_thryvar(x): x in V}))
(425) Theorem product_order_1: [The first component of any member of a Cartesian product of ordinals is an ordinal] (X in o1 •PROD o2) •imp Ord(car(X))
(426) Theorem product_order_2: [The second component of any member of a Cartesian product of ordinals is an ordinal] (X in o1 •PROD o2) •imp Ord(cdr(X))
(427) Theorem product_order_3: [The maximum of the components of any member of a Cartesian product of ordinals is an ordinal] (X in o1 •PROD o2) •imp Ord(car(X) + cdr(X))
(428) Theorem product_order_4: ((X in o1 •PROD o2) & (Y in o1 •PROD o2)) •imp ((Ord1p2_thryvar(X,Y) or Ord1p2_thryvar(Y,X) or X = Y) & (not Ord1p2_thryvar(X,X)))
(429) Theorem product_order_5: ((X in o1 •PROD o2) & (Y in o1 •PROD o2) & (Z in o1 •PROD o2) & Ord1p2_thryvar(X,Y) & Ord1p2_thryvar(Y,Z)) •imp Ord1p2_thryvar(X,Z)
(430) Theorem product_order_6: ((T •incin (o1 •PROD o2)) & (T /= 0)) •imp (EXISTS x in T | (FORALL y in t | (Ord1p2_thryvar(x,y) or (x = y))))
(431) Theorem 338: ['One-more' lemma] (not Finite(S)) •imp (#S = #(S + {C}))
(432) Theorem 339: ['Few-more' lemma] ((not Finite(S)) & Finite(T)) •imp (#S = #(S + T))
(433) Theorem 340: [Any infinite cardinal is a limit ordinal] ((not Finite(S)) & (X in #S)) •imp (X + {X} in #S)
(434) Theorem 341: [If ordinal S dominates the members of an ordinal T, #S is no less than #T] (Ord(S) & Ord(T) & (not Finite(S)) & (FORALL u in T | #u in #S)) •imp (#T •incin #S)
(435) Theorem 342: [The cardinality of a non-null Cartesian product is at least the cardinality of its first factor] (T /= 0) •imp (#S •incin #(S •PROD T))
(436) Theorem 343: (Ord(O1) & Ord(O2)) •imp (EXISTS f in OM | one_1_map(f) & Ord(domain(f)) & (range(f) = (O1 •PROD O2)) & (FORALL x in domain(f), y in domain(f) | (x in y) •eq (((car(f~[x]) + cdr(f~[x])) in (car(f~[y]) + cdr(f~[y]))) or (((car(f~[x]) + cdr(f~[x])) = (car(f~[y]) + cdr(f~[y]))) & (car(f~[x]) in car(f~[y]))) or (((car(f~[x]) + cdr(f~[x])) = (car(f~[y]) + cdr(f~[y]))) & (car(f~[x]) = car(f~[y])) & (cdr(f~[x]) in cdr(f~[y]))))))
(437) Theorem 344: (Card(O1) & Card(O2) & (not Finite(O1 + O2))) •imp (EXISTS f in OM | one_1_map(f) & Ord(domain(f)) & (range(f) = (O1 •PROD O2)) & (FORALL x in domain(f) | (EXISTS y in (O1 + O2) | range(f •ON x) •incin (y •PROD y))))
(438) Theorem 345: [Cardinal Doubling Theorem] (not Finite(S)) •imp (#(S •PROD {0,1}) = #S)
(439) Theorem 346: [The sum of two infinite quantities is their maximum] (not Finite(S)) •imp ((S •PLUS T) = #S + #T)
(440) Theorem 347: [The cardinality of the union of two infinite quantities is the cardinality of the larger] (not Finite(S)) •imp (#(S + T) = #S + #T)
(441) Theorem 348: [Cardinal Square Theorem] (not Finite(S)) •imp (#(S •PROD S) = #S)
(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))
(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))
(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]))
(451) Theorem 358: [The intersection of two unsigned integers is the smaller of the two] ((N in Za) & (M in Za)) •imp (((N * M) in Za) & ((N * M) in {N,M}) & ((N •MINUS (N * M)) in Za) & ((M •MINUS (N * M)) in Za))
(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]))
(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)
(456) Theorem 363: [Commutativity lemma for signed integers, 2] ((J in Za) & (K in Za) & (N in Za) & (M in Za)) •imp ([J,K] •S_PLUS [N,M] = [N,M] •S_PLUS [J,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)
(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]))
(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))
(463) Theorem 370: [Reduction of a pair (N,0) gives (N,0)] (N in Za) •imp (Red([N,0]) = [N,0])
(464) Theorem 371: [Embedding of Integers in Signed Integers] ((N in Za) & (M in Za)) •imp (([N •PLUS M,0] = [N,0] •S_PLUS [M,0] & [N •TIMES M,0] = [N,0] •S_TIMES [M,0]) & ((N incs M) •imp ([N,0] •S_MINUS [M,0] = [N •MINUS M,0])))
(465) Theorem 372: [Sign-reversal of signed integers] ((N in Za) & (M in Za)) •imp (S_Rev(Red([M,N])) = Red([N,M]))
(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)
(470) Theorem 377: [Associativity lemma] ((N in Za) & (M in Za) & (K in Za)) •imp ([N,0] •S_TIMES ([M,0] •S_TIMES [K,0]) = ([N,0] •S_TIMES [M,0]) •S_TIMES [K,0])
(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)
(488) Theorem mathematical_induction0: [The minimum integer having a given property, preliminary version] (FORALL k | ((m_thryvar in Za) & P(m_thryvar)) & ((k in m_thryvar) •imp (not ((k in Za) & P(k)))))
(490) Theorem double_transfinite_induction.1: [Minimum first element in a double transfinite induction] (FORALL k | ((EXISTS i | R(m_thryvar,i)) & ((k in m_thryvar) •imp (not (EXISTS i | R(k,i))))))
(492+) Theorem double_transfinite_induction.4: [Minimal element properties in a double transfinite induction] (FORALL i | R(m_thryvar,j_thryvar) & ((i in j_thryvar) •imp (not R(m_thryvar,i))))
(493) Theorem double_transfinite_induction.5: [Minimal element properties in a double transfinite induction, 2] R(m_thryvar,j_thryvar) & ((K in m_thryvar) •imp (not R(K,I))) & ((I in j_thryvar) •imp (not R(m_thryvar,I)))
(496) Theorem double_mathematical_induction.4: (FORALL i | (j_thryvar in Za) & R(mm_thryvar,j_thryvar) & ((i in j_thryvar) •imp (not ((i in Za) & R(mm_thryvar,i)))))
(497) Theorem double_mathematical_induction.5: (mm_thryvar in Za) & (j_thryvar in Za) & R(mm_thryvar,j_thryvar) & (((K in mm_thryvar) & (I in Za)) •imp (not R(K,I))) & ((I in j_thryvar) •imp (not R(mm_thryvar,I)))
(498) Theorem confinedIncrSeq1: [global increase of a stepwise increasing sequence] ((I in J) & (J in Za)) •imp (e(I) •incin e(J))
(499) Theorem wellfounded_recursive_fcn.100: (FORALL u, v | (Ord(u) & Ord(v) & (orden(u) /= s) & arg1_bef_arg2(orden(u),orden(v))) •imp (u in v)) & (EXISTS o in next(#pow(s)) | (Ord(o) & (s = {orden(x): x in o}) & (FORALL x in o | (orden(x) /= s)) & one_1_map({[x,orden(x)]: x in o})))
(501) Theorem wellfounded_recursive_fcn.1: (V in s) •imp ((index(V) in o) & Ord(index(V)) & (orden(index(V)) = V))
(501+) Theorem wellfounded_recursive_fcn.2: (V in s) •imp ({j: j in index(V) | arg1_bef_arg2(orden(j),V)} = {index(w): w in s | arg1_bef_arg2(w,V)})
(502) Theorem wellfounded_recursive_fcn.3: (X in s) •imp (h2_thryvar(X,T) = f3({g4(h2_thryvar(y,T),y,X,T): y in s | arg1_bef_arg2(y,X) & P4(h2_thryvar(y,T),y,X,T)},X,T))
(503) Theorem wellfounded_recursive_fcn.4: (FORALL x, t | (x in s) •imp (rk_thryvar(x,t) = Un({next(rk_thryvar(y,t)): y in s | arg1_bef_arg2(y,x) & ([y,x] in t)})))
(504) Theorem 394: ((FORALL v in X | Finite(v)) & (U •incin X) & (U /= 0)) •imp (EXISTS w in U | (FORALL y in U | not((y •incin w) & (y /= w))))
(505) Theorem finite_recursion_coherence.1: ((X in q) & (X in r)) •imp (h_q(X,T) = h_r(X,T))
(505+) Theorem fin_well_founded.1: ((V •incin s) & (V /= 0)) •imp (EXISTS m in V | (FORALL y in V | not(arg1_bef_arg2(y,m))))
(506) Theorem finite_recursive_fcn.0: ((T •incin {y: y •incin S | Finite(y)}) & (T /= 0)) •imp (EXISTS x in T | (FORALL y in T | not((y •incin x) & (y /= x))))
(507) Theorem finite_recursive_fcn.1: (FORALL s,t | (EXISTS h | (FORALL x | ((x •incin s) & Finite(x)) •imp (h~[x] = f3({g4(h~[y],y,x,t): y •incin x | (y /= x) & P4(h~[y],y,x,t)},x,t)))))
(507+) Theorem finite_recursive_fcn.a: (FORALL s,t | (FORALL x | ((x •incin s) & Finite(x)) •imp (hsko(s,t)~[x] = f3({g4(hsko(s,t)~[y],y,x,t): y •incin x | (y /= x) & P4(hsko(s,t)~[y],y,x,t)},x,t))))
(508) Theorem finite_recursive_fcn.2: (FORALL x | ((x •incin S) & Finite(x)) •imp (hsko(S,T)~[x] = f3({g4(hsko(S,T)~[y],y,x,T): y •incin x | (y /= x) & P4(hsko(S,T)~[y],y,x,T)},x,T)))
(509) Theorem finite_recursive_fcn.3: Finite(S) •imp (h2_thryvar(S,T) = f3({g4(h2_thryvar(y,T),y,S,T): y •incin S | (y /= S) & P4(h2_thryvar(y,T),y,S,T)},S,T))
(510) Theorem finite_tailrecursive_fcn.0: (FORALL s,t | Finite(s) •imp (h2_thryvar(s,t) = if ({g3(h2_thryvar(y,t),s,t): y •incin s | (y /= s) & (y = sl(s))} = 0) then f(t) else arb({g3(h2_thryvar(y,t),s,t): y •incin s | (y /= s) & (y = sl(s))}) end if))
(511) Theorem finite_tailrecursive_fcn.1: Finite(S) •imp (h2_thryvar(S,T) = if (S = 0) then f(T) else g3(h2_thryvar(sl(S), T), S,T) end if)
(511+) Theorem finite_tailrecursive_fcn1.0: ((X - {arb(X)}) •incin X) & ((X /= 0) •imp ((X - {arb(X)}) /= X))
(512) Theorem finite_tailrecursive_fcn1.1: (FORALL s,t | Finite(s) •imp (h2_thryvar(s,t) = if (s = 0) then f(t) else g3(h2_thryvar(s - {arb(s)}, t), s,t) end if))
(513) Theorem finite_tailrecursive_fcn2.0: (FORALL s,t | Finite(s) •imp (h(s,t) = if s = 0 then f0 else g2(h(s - {arb(s)},t),s) end if))
(514) Theorem finite_tailrecursive_fcn2.1: Finite(S) •imp (h1_thryvar(S) = if S = 0 then f0 else g2(h1_thryvar(S - {arb(S)}),S) end if)
(515) Theorem sigma_theory0: [Recursive formula for generalized sum] (FORALL x | Finite(x) •imp (sigma_thryvar(x) = if x = 0 then e else pluz(sigma_thryvar(x - {arb(x)}),cdr(arb(x))) end if))
(517) Theorem sigma_theory2: [Summation of singleton map is range element] (cdr(X) in s) •imp (sigma_thryvar({X}) = cdr(X))
(517+) Theorem sigma_theory3: [Sum value belongs to closed range of map] (Finite(F) & (range(F) •incin s)) •imp (sigma_thryvar(F) in s)
(518) Theorem sigma_theory4: [Removal of single element from domain of a sum] ((C in F) & Finite(F) & (range(F) •incin s)) •imp (sigma_thryvar(F) = pluz(sigma_thryvar(F - {C}),cdr(C)))
(519) Theorem sigma_theory5: [The generalized sum of a union map is a sum of sums] (Finite(F) & Is_map(F) & (range(F) •incin s)) •imp (sigma_thryvar(F) = pluz(sigma_thryvar(F •ON (domain(F) * T)), sigma_thryvar(F •ON (domain(F) - T))))
(520) Theorem sigma_theory6: [Rearrangement-of-sums theorem] (Finite(F) & Svm(F) & Svm(G) & (domain(F) = domain(G)) & (range(F) •incin s)) •imp (sigma_thryvar(F) = sigma_thryvar({[y,sigma_thryvar(F •ON (G •INV_IM {y}))]: y in range(G)}))
(520+) Theorem sigma_theory7: [Sum permutation theorem] (Finite(F) & Svm(F) & one_1_map(G) & (domain(F) = domain(G)) & (range(F) •incin s)) •imp (sigma_thryvar(F) = sigma_thryvar({[y,F~[inv(G)~[y]]]: y in range(G)}))
(521) Theorem equivalence_classes1: [Elements are equivalent if and only if their equivalence classes are equal] ((X in s) & (Y in s)) •imp (R(X,Y) •eq (f_thryvar(X) = f_thryvar(Y)))
(522) Theorem equivalence_classes2: [The equivalence class of any element is an equivalence class] (X in s) •imp (f_thryvar(X) in Eqc_thryvar)
(523) Theorem equivalence_classes2b: [Any element of an equivalence class can represent the class] ((X in Eqc_thryvar) •imp ((arb(X) in s) & (f_thryvar(arb(X)) = X)))
(523+) Theorem equivalence_classes3: [Any two elements of an equivalence class are equivalent] (X in s) •imp R(x,arb(f_thryvar(x)))
(524) Theorem linear_order_1: (({U,V,W} •incin s0) & (U •le_thryvar V) & (V •le_thryvar W)) •imp (U •le_thryvar W)
(524+) Theorem linear_order_2: (({U,V} •incin s0) & (U •le_thryvar V) & (V •le_thryvar U)) •imp (U = V)
(526) Theorem linear_order_4: ({U,V} •incin s0) •imp ((U •le_thryvar V) or (V •le_thryvar U))
(526+) Theorem linear_order_5: ({U,V,W} •incin s0) •imp (((U •le_thryvar V) & (U •le_thryvar W)) or ((V •le_thryvar U) & (V •le_thryvar W)) or ((W •le_thryvar U) & (W •le_thryvar V)))
(527) Theorem linear_order_6: ({X,Y} •incin s0) •imp (smaller_thryvar(X,Y) in {X,Y})
(528) Theorem linear_order_7: (({X,Y} •incin s0) & (arg1_bef_arg2(X,Y) or (X = Y))) •imp ((smaller_thryvar(X,Y) = X) & (smaller_thryvar(Y,X) = X))
(529) Theorem linear_order_8: (X in next(s0)) •imp (smaller_thryvar(X,s0) = X)
(531) Theorem linear_order_10: ((X in next(s0)) & (Y in next(s0))) •imp (smaller_thryvar(X,Y) in next(s0))
(532) Theorem linear_order_11: (s0 in next(s0)) & (FORALL x,y,z | ((x in next(s0)) & (y in next(s0)) & (z in next(s0))) •imp (smaller_thryvar(x,smaller_thryvar(y,z)) = smaller_thryvar(smaller_thryvar(x,y),z))) & (FORALL x,y | ((x in next(s0)) & (y in next(s0))) •imp (smaller_thryvar(x,y) = smaller_thryvar(y,x)))
(533) Theorem linear_order_12: (FORALL f | (Finite(f) & (range(f) •incin next(s0))) •imp (min_over_thryvar(f) in next(s0))) & (FORALL x | (cdr(x) in next(s0)) •imp (min_over_thryvar({x}) = cdr(x))) & (FORALL f,t | (Finite(f) & Is_map(f) & (range(f) •incin next(s0))) •imp (min_over_thryvar(f) = smaller_thryvar(min_over_thryvar(f •ON (domain(f) * t)),min_over_thryvar(f •ON (domain(f) - t))))) & (FORALL c,f | ((c in f) & Finite(f) & (range(f) •incin next(s0))) •imp (min_over_thryvar(f) = smaller_thryvar(min_over_thryvar(f - {c}),cdr(c))))
(534) Theorem linear_order_13: (Svm(F) & (range(F) •incin s0) & Finite(F)) •imp (((P in F) •imp (min_over_thryvar({P}) = (F~[car(P)]))) & (min_over_thryvar(F) = smaller_thryvar(min_over_thryvar(F •ON (domain(F) * A)),min_over_thryvar(F •ON (domain(F) - A)))))
(535) Theorem linear_order_14: (Svm(F) & (range(F) •incin s0) & Finite(F) & (F /= 0)) •imp (min_over_thryvar(F) in range(F))
(536) Theorem linear_order_15: ({X,Y} •incin s0) •imp ((smaller_thryvar(X,Y) = X) •eq (arg1_bef_arg2(X,Y) or (X = Y)))
(539) Theorem linear_order_18: (Finite(T) & (X in T) & (T •incin s0)) •imp ((max_thryvar(T) in T) & ((X = max_thryvar(T)) or (arg1_bef_arg2(X,max_thryvar(T)))))
(540) Theorem linear_order_19: (FORALL x in s0, y in s0, z in s0 | (arg1_aft_arg2(x,y) & arg1_aft_arg2(y,z)) •imp arg1_aft_arg2(x,z)) & (FORALL x in s0 | not(arg1_aft_arg2(x,x))) & (FORALL x in s0, y in s0 | arg1_aft_arg2(x,y) or (x = y) or arg1_aft_arg2(y,x))
(541) Theorem linear_order_20: (FORALL x, y | larger_thryvar(x,y) = if ((x notin s0) & (y notin s0)) then s0 elseif (x notin s0) then y elseif (y notin s0) then x elseif arg1_aft_arg2(x,y) then x else y end if) & (FORALL x, y | larger_thryvar(x,y) = larger_thryvar(y,x)) & (FORALL x, y | ({x,y} •incin s0) •imp (larger_thryvar(x,y) in {x,y})) & (FORALL x | (x in next(s0)) •imp (larger_thryvar(x,s0) = x)) & (FORALL x, y, z | larger_thryvar(x,larger_thryvar(y,z)) = larger_thryvar(larger_thryvar(x,y),z)) & (FORALL x, y | ((x in next(s0)) & (y in next(s0))) •imp (larger_thryvar(x,y) in next(s0))) & (FORALL f,p,a | (Svm(f) & (range(f) •incin s0) & Finite(f)) •imp (((p in f) •imp (max_over_thryvar({p}) = (f~[car(p)]))) & (max_over_thryvar(f) = larger_thryvar(max_over_thryvar(f •ON (domain(f) * a)),max_over_thryvar(f •ON (domain(f) - a)))))) & (FORALL f | (Svm(f) & (range(f) •incin s0) & Finite(f) & (f /= 0)) •imp (max_over_thryvar(f) in range(f))) & (FORALL x, y | ({x,y} •incin s0) •imp ((larger_thryvar(x,y) = x) •eq (arg1_aft_arg2(x,y) or (x = y)))) & (FORALL t | lbs_thryvar(t) = {x in s0 | (FORALL y in (t * s0) | larger_thryvar(y,x) = y)}) & (FORALL t | min_thryvar(t) = arb({s0} + (t * lbs_thryvar(t)))) & (FORALL t | glb_thryvar(t) = arb({s0} + {x in lbs_thryvar(t) | lbs_thryvar(t) •incin lbs_thryvar({x})})) & (lbs_thryvar(0) = s0) & (min_thryvar(0) = s0) & (FORALL t | (lbs_thryvar(t) •incin s0) & (lbs_thryvar(t) = lbs_thryvar(t * s0)) & (min_thryvar(t) = min_thryvar(t * s0))) & (FORALL t, x | (Finite(t) & (x in t) & (t •incin s0)) •imp ((min_thryvar(t) in t) & ((x = min_thryvar(t)) or (arg1_aft_arg2(x,min_thryvar(t))))))
(544) Theorem 395: [Zorn's lemma] (FORALL x •incin T | ((FORALL u in x,v in x | (u incs v or v incs u)) •imp (EXISTS w in T | (FORALL y in x | w incs y)))) •imp (EXISTS y in T | (FORALL x in T | not ((x incs y) & (x /= y))))
(545) Theorem 396: [Zorn's lemma generalized form] (FORALL x •incin T | ((FORALL u in x,v in x | (u incs v or v incs u)) •imp (EXISTS w in T | (FORALL y in x | w incs y)))) •imp (FORALL u in T | (EXISTS y in T | (y incs u) & (FORALL x in T | not ((x incs y) & (x /= y)))))
(546) Theorem 397: [Zorn's lemma for union-closed collections] (FORALL x •incin T | ((FORALL u in x,v in x | (u incs v or v incs u)) •imp (Un(x) in T))) •imp (FORALL u in T | (EXISTS y in T | (y incs u) & (FORALL x in T | not ((x incs y) & (x /= y)))))
(547) Theorem 398: ((FORALL t in TP | Filter(t,S)) & (FORALL u in TP, v in TP | (u incs v or v incs u))) •imp Filter(Un(TP),S)
(548) Theorem 399: (S /= 0) •imp ((Filter(T,S) & (FORALL x •incin pow(S) | ((x incs T) & Filter(x,S)) •imp (x = T))) •eq Ultrafilter(T,S))
(549) Theorem 400: [Every filter on a set S can be extended to an ultrafilter on S] (Filter(T,S) & (S /= 0)) •imp (EXISTS u | ((u incs T) & Ultrafilter(u,S)))
(550) Theorem 402: [Equivalence of fractions is transitive] (FORALL x in Fr, y in Fr, wz in Fr | (Same_frac(x,y) & Same_frac(y,wz)) •imp Same_frac(x,wz))
(551) Theorem 403: [Fractions are equivalent if and only if the rational numbers they define are equal] (FORALL x, y | ((x in Fr) & (y in Fr)) •imp ((Same_frac(x,y) •eq (Fr_to_Ra(x) = Fr_to_Ra(y))))) & (FORALL x | (x in Ra) •imp ((arb(x) in Fr) & (Fr_to_Ra(arb(x)) = x))) & (FORALL x | (x in Fr) •imp (Fr_to_Ra(x) in Ra)) & (FORALL x | (x in Fr) •imp Same_frac(x,arb(Fr_to_Ra(x))))
(552) Theorem 404: [Every fraction is equivalent to every member of its rational number class] (X in Fr) •imp ((Fr_to_Ra(X) in Ra) & Same_frac(X,arb(Fr_to_Ra(X))))
(553) Theorem 405: [Alternate version of Theorem 403] ((X in Fr) & (Y in Fr)) •imp (Same_frac(X,Y) •eq (Fr_to_Ra(X) = Fr_to_Ra(Y)))
(554) Theorem 406: [Alternate version of Theorem 404] (Y in Ra) •imp ((arb(Y) in Fr) & (Fr_to_Ra(arb(Y)) = Y))
(556) Theorem Ordered_add.1: [Interface to Otter-based THEORY of orderedGroups] (LE_thryvar(X,Y) •eq nneg(pluz(Y,rvz(X)))) & (((X in g) & (Y in g)) •imp (GT_thryvar(X,Y) •eq (nneg(pluz(X,rvz(Y))) & (X /= Y)))) & (((X in g) & (Y in g)) •imp (GT_thryvar(X,Y) •eq (nneg(minz(X,Y)) & (X /= Y))))
(557) Theorem Ordered_add.2: [The ordering by GE_thryvar is a linear ordering] ((X in g) & (Y in g) & ((X = Y) or (not GE_thryvar(X,Y)))) •imp GE_thryvar(Y,X)
(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))
(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]))
(567) Theorem 417: [Fractions are equivalent if their cross-products are equal] ((X in Fr) & (Y in Fr) & Same_frac(X,Y) & (W in Fr) & (Z in Fr) & Same_frac(W,Z)) •imp Same_frac([(car(X) •S_TIMES cdr(W)) •S_PLUS (car(W) •S_TIMES cdr(X)),cdr(X) •S_TIMES cdr(W)], [(car(Y) •S_TIMES cdr(Z)) •S_PLUS (car(Z) •S_TIMES cdr(Y)),cdr(Y) •S_TIMES cdr(Z)])
(568) Theorem 418: [If two pair of fractions are equivalent, their formal sums are also equivalent] ((X in Fr) & (Y in Fr) & Same_frac(X,Y) & (W in Fr) & (Z in Fr) & Same_frac(W,Z)) •imp (Fr_to_Ra([(car(X) •S_TIMES cdr(W)) •S_PLUS (car(W) •S_TIMES cdr(X)),cdr(X) •S_TIMES cdr(W)]) = Fr_to_Ra([(car(Y) •S_TIMES cdr(Z)) •S_PLUS (car(Z) •S_TIMES cdr(Y)),cdr(Y) •S_TIMES cdr(Z)]))
(568+) Theorem 419: [If two pairs of fractions are equivalent, their formal products are also equivalent] ((X in Fr) & (Y in Fr) & Same_frac(X,Y) & (W in Fr) & (Z in Fr) & Same_frac(W,Z)) •imp Same_frac([car(X) •S_TIMES car(W),cdr(X) •S_TIMES cdr(W)],[car(Y) •S_TIMES car(Z),cdr(Y) •S_TIMES cdr(Z)])
(569) Theorem 420: [If two pairs of fractions are equivalent, their formal sums define the same rational number] ((X in Fr) & (Y in Fr) & Same_frac(X,Y) & (W in Fr) & (Z in Fr) & Same_frac(W,Z)) •imp (Fr_to_Ra([car(X) •S_TIMES car(W),cdr(X) •S_TIMES cdr(W)]) = Fr_to_Ra([car(Y) •S_TIMES car(Z),cdr(Y) •S_TIMES cdr(Z)]))
(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]))
(572) Theorem 423: [Reversing both the numerator and denominator of a formal fraction does not change the rational it represents] (X in Fr) •imp Same_frac(X,[S_Rev(car(X)),S_Rev(cdr(X))])
(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)))
(575) Theorem 426: [?] (X in Fr) •imp (Fr_is_nonneg(X) •eq Fr_is_nonneg([S_Rev(car(X)),S_Rev(cdr(X))]))
(576) Theorem 427: [?] ((X in Fr) & (Y in Fr) & Same_frac(X,Y)) •imp (Fr_is_nonneg(X) •eq Fr_is_nonneg(Y))
(577) Theorem 428: [Commutativity of rational addition] ((N in Ra) & (M in Ra)) •imp ((N •Ra_PLUS M in Ra) & (N •Ra_PLUS M = M •Ra_PLUS N))
(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]))
(579) Theorem 431: [Commutativity of rational multiplication] ((N in Ra) & (M in Ra)) •imp ((N •Ra_TIMES M in Ra) & (N •Ra_TIMES M = M •Ra_TIMES N))
(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]))
(581) Theorem 433: [Associative law for rational addition] ((K in Ra) & (N in Ra) & (M in Ra)) •imp (N •Ra_PLUS (M •Ra_PLUS K) = (N •Ra_PLUS M) •Ra_PLUS K)
(582) Theorem 434: [The zero rational is the identity for rational addition] (Ra_0 in Ra) & (Ra_1 in Ra) & ((M in Ra) •imp (M = M •Ra_PLUS Ra_0))
(583) Theorem 435: [The sum of a rational number and its additive inverse is zero] (M in Ra) •imp ((Ra_Rev(M) in Ra) & ((M •Ra_PLUS Ra_Rev(M)) = Ra_0))
(584) Theorem 436: [The sum of a rational number and its additive inverse is zero, 2] (M in Ra) •imp ((Ra_Rev(M) in Ra) & ((Ra_Rev(M) •Ra_PLUS M) = Ra_0))
(585) Theorem 437: [The difference of two rationals is rational] ((N in Ra) & (M in Ra)) •imp ((N •Ra_MINUS M) in Ra)
(586) Theorem 438: [Rational subtraction is equivalent to addition of the rational negative] ((N in Ra) & (M in Ra)) •imp (N = M •Ra_PLUS (N •Ra_MINUS M))
(587) Theorem 439: [Associative law for rational multiplication] ((K in Ra) & (N in Ra) & (M in Ra)) •imp (N •Ra_TIMES (M •Ra_TIMES K) = (N •Ra_TIMES M) •Ra_TIMES K)
(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]))
(589) Theorem 441: [Distributive law for rationals] ((K in Ra) & (N in Ra) & (M in Ra)) •imp (N •Ra_TIMES (M •Ra_PLUS K) = (N •Ra_TIMES M) •Ra_PLUS (N •Ra_TIMES K))
(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))
(592) Theorem 444: [The unit rational is the rational multiplicative identity] (M in Ra) •imp (M = M •Ra_TIMES Ra_1)
(593) Theorem 445: [Multiplication of a rational by its reciprocal gives 1] ((M in Ra) & (M /= Ra_0)) •imp ((Recip(M) in Ra) & (M •Ra_TIMES Recip(M) = Ra_1))
(594) Theorem 446: ((N in Ra) & (M in Ra) & (M /= Ra_0)) •imp (((N •Ra_TIMES (M •Ra_TIMES M)) •Ra_TIMES (Recip(M) •Ra_TIMES Recip(M))) = N)
(595) Theorem 447: [Rational division is multiplication by the reciprocal] ((N in Ra) & (M in Ra) & (M /= Ra_0)) •imp (N = M •Ra_TIMES (N •Ra_OVER M))
(597) Theorem 449: [One of a rational and its additive inverse is always non-negative, and both are non-negative only if the rational is zero] (X in Ra) •imp ((Ra_is_nonneg(X) or Ra_is_nonneg(Ra_Rev(X))) & ((Ra_is_nonneg(X) & Ra_is_nonneg(Ra_Rev(X))) •imp (X = Ra_0)))
(598) Theorem 450: [?] (FORALL x,y | ((x •Ra_GE y) •eq Ra_is_nonneg(x •Ra_PLUS Ra_Rev(y)))) & (FORALL x,y | ((x •Ra_LE y) •eq (y •Ra_GE x))) & (FORALL x,y | ((x •Ra_GT y) •eq ((x •Ra_GE y) & (x /= y)))) & (FORALL x,y | ((x •Ra_LT y) •eq (y •Ra_GT x))) & (FORALL x,y | ((x •Ra_LE y) •eq Ra_is_nonneg(y •Ra_PLUS Ra_Rev(x)))) & (FORALL x,y | (((x in Ra) & (y in Ra)) •imp ((x •Ra_GT y) •eq (Ra_is_nonneg(x •Ra_PLUS Ra_Rev(y)) & (x /= y))))) & (FORALL x,y | (((y in Ra) & (y in Ra)) •imp ((x •Ra_GT y) •eq (Ra_is_nonneg(x •Ra_MINUS y) & (x /= y))))) & (FORALL x,y | (((x in Ra) & (y in Ra) & ((x = y) or (not(x •Ra_GE y)))) •imp (y •Ra_GE x)))
(599) Theorem 451: [Various basic properties of rational comparison] ((X •Ra_GE Y) •eq Ra_is_nonneg(X •Ra_PLUS Ra_Rev(Y))) & ((X •Ra_LE Y) •eq (Y •Ra_GE X)) & ((X •Ra_GT Y) •eq ((X •Ra_GE Y) & (X /= Y))) & ((X •Ra_LT Y) •eq (Y •Ra_GT X)) & ((X •Ra_LE Y) •eq Ra_is_nonneg(Y •Ra_PLUS Ra_Rev(X))) & (((X in Ra) & (Y in Ra)) •imp ((X •Ra_GT Y) •eq (Ra_is_nonneg(X •Ra_PLUS Ra_Rev(Y)) & (X /= Y)))) & (((X in Ra) & (Y in Ra)) •imp ((X •Ra_GT Y) •eq (Ra_is_nonneg(X •Ra_MINUS Y) & (X /= Y)))) & (((X in Ra) & (Y in Ra) & ((X = Y) or (not(X •Ra_GE Y)))) •imp (Y •Ra_GE X))
(600) Theorem 452: [Greater_than_equal is greater-than and equal] ((X in Ra) & (Y in Ra)) •imp ((X •Ra_GE Y) •eq ((X •Ra_GT Y) or (X = Y)))
(601) Theorem 453: [Less_than_equal is less-than and equal] ((X in Ra) & (Y in Ra)) •imp ((X •Ra_LE Y) •eq ((X •Ra_LT Y) or (X = Y)))
(602) Theorem 454: [The rationals are a linearly ordered set] ((X in Ra) & (Y in Ra)) •imp ((X •Ra_GT Y) or (X = Y) or (Y •Ra_GT X))
(603) Theorem 455: [The rationals are a linearly ordered set, 2] ((X in Ra) & (Y in Ra)) •imp ((X •Ra_LT Y) or (X = Y) or (Y •Ra_LT X))
(604) Theorem 456: [The rationals are a linearly ordered set,3] ((X in Ra) & (Y in Ra)) •imp ((X •Ra_GT Y) or (Y •Ra_GE X))
(605) Theorem 457: [The rationals are a linearly ordered set,4] ((X in Ra) & (Y in Ra)) •imp ((X •Ra_LT Y) or (Y •Ra_LE X))
(606) Theorem 458: [The unit rational is the identity for multiplication] (X in Ra) •imp (X = X •Ra_TIMES Ra_1)
(607) Theorem 459: [The zero rational is represented by any fraction whose numerator is 0] (X in Ra) •imp ((X = Ra_0) •eq (car(arb(X)) = [0,0]))
(608) Theorem 460: [The sum and product of two non-negative rationals is non-negative] ((X in Ra) & (Y in Ra) & Ra_is_nonneg(X) & Ra_is_nonneg(Y)) •imp (Ra_is_nonneg(X •Ra_PLUS Y) & Ra_is_nonneg(X •Ra_TIMES Y))
(609) Theorem 461: [Transitivity of ordering] ((X in Ra) & (Y in Ra) & (Z in Ra)) •imp (((X •Ra_GE Y) & (Y •Ra_GE Z)) •imp (X •Ra_GE Z))
(611) Theorem 463: [Alternate characterization of non-negativity for rationals] (X in Ra) •imp ((Ra_is_nonneg(X) •eq (X •Ra_GE Ra_0)) & ((X •Ra_GT Ra_0) •imp Ra_is_nonneg(X)))
(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]))
(614) Theorem 466: [First law of signs for rational multiplication] ((X in Ra) & (Y in Ra)) •imp ((X •Ra_TIMES Ra_Rev(Y)) = Ra_Rev(X •Ra_TIMES Y))
(615) Theorem 467: [The reverse of a rational X is the reverse of 1, times X] (X in Ra) •imp (Ra_Rev(X) = (Ra_Rev(Ra_1) •Ra_TIMES X))
(616) Theorem 468: ((X in Ra) & (Y in Ra) & (Z in Ra)) •imp ((X •Ra_TIMES (Y •Ra_MINUS Z)) = (X •Ra_TIMES Y) •Ra_MINUS (X •Ra_TIMES Z))
(617) Theorem 469: [Strict monotonicity of rational multiplication over 1st argument] ((X in Ra) & (Y in Ra) & (X1 in Ra) & (X •Ra_GT Y) & (X1 •Ra_GT Ra_0)) •imp ((X •Ra_TIMES X1) •Ra_GT (Y •Ra_TIMES X1))
(618) Theorem 470: (X in Ra) •imp (X •Ra_TIMES Ra_0 = Ra_0)
(618+) Theorem 471: ((X in Ra) & (Y in Ra) & (X •Ra_GT Ra_0) & (Y •Ra_GT Ra_0)) •imp ((X •Ra_TIMES Y) •Ra_GT Ra_0)
(619) Theorem 472: ((X in Ra) & (X •Ra_GT Ra_0)) •imp (Recip(X) •Ra_GT Ra_0)
(620) Theorem 473: ((X in Ra) & (Y in Ra)) •imp (Ra_Rev(X •Ra_PLUS Y) = (Ra_Rev(X) •Ra_PLUS Ra_Rev(Y)))
(621) Theorem 474: ((X in Ra) & (Y in Ra) & (XP in Ra) & (YP in Ra) & (X •Ra_GE Y) & (XP •Ra_GE YP)) •imp ((X •Ra_PLUS XP) •Ra_GE (Y •Ra_PLUS YP))
(622) Theorem 475: (X in Ra) •imp (Ra_Rev(Ra_Rev(X)) = X)
(623) Theorem 476: ((X in Ra) & (Y in Ra)) •imp (((X •Ra_GE Y) or (Y •Ra_GE X)) & (((X •Ra_GE Y) & (Y •Ra_GE X)) •imp (X = Y)))
(624) Theorem 477: [Transitivity of ordering, strict case] ((X in Ra) & (Y in Ra) & (Z in Ra)) •imp (((X •Ra_GE Y) & (Y •Ra_GT Z)) •imp (X •Ra_GT Z))
(625) Theorem 478: [Transitivity of ordering, strict case 2] ((X in Ra) & (Y in Ra) & (Z in Ra)) •imp (((X •Ra_GT Y) & (Y •Ra_GE Z)) •imp (X •Ra_GT Z))
(626) Theorem 479: [Transitivity of ordering, strict case 3] ((X in Ra) & (Y in Ra) & (Z in Ra)) •imp (((X •Ra_GT Y) & (Y •Ra_GT Z)) •imp (X •Ra_GT Z))
(627) Theorem 480: [Transitivity of ordering by 'less than'] ((X in Ra) & (Y in Ra) & (Z in Ra)) •imp (((X •Ra_LE Y) & (Y •Ra_LT Z)) •imp (X •Ra_LT Z))
(628) Theorem 481: [Transitivity of ordering by 'less than', 2] ((X in Ra) & (Y in Ra) & (Z in Ra)) •imp (((X •Ra_LT Y) & (Y •Ra_LE Z)) •imp (X •Ra_LT Z))
(629) Theorem 482: [Transitivity of ordering by 'less than', 3] ((X in Ra) & (Y in Ra) & (Z in Ra)) •imp (((X •Ra_LT Y) & (Y •Ra_LT Z)) •imp (X •Ra_LT Z))
(630) Theorem 483: ((X in Ra) & (Y in Ra) & (X •Ra_GE Y)) •imp (Ra_Rev(Y) •Ra_GE Ra_Rev(X))
(631) Theorem 484: ((X in Ra) & (Y in Ra) & (X •Ra_GT Y)) •imp (Ra_Rev(Y) •Ra_GT Ra_Rev(X))
(632) Theorem 485: ((X in Ra) & (Y in Ra) & (XP in Ra) & (YP in Ra) & (X •Ra_GE Y) & (XP •Ra_GT YP)) •imp ((X •Ra_PLUS XP) •Ra_GT (Y •Ra_PLUS YP))
(633) Theorem 486: ((X in Ra) & (Y in Ra) & (XP in Ra) & (YP in Ra) & (X •Ra_GT Y) & (XP •Ra_GE YP)) •imp ((X •Ra_PLUS XP) •Ra_GT (Y •Ra_PLUS YP))
(634) Theorem 487: ((X in Ra) & (X /= Ra_0)) •imp ((Recip(X) /= Ra_0) & Recip(Recip(X)) = X)
(636) Theorem 489: ((X in Ra) & (Y in Ra) & (Z in Ra) & (X •Ra_GE Y) & (Y •Ra_GE Z)) •imp (X •Ra_GE Z)
(637) Theorem 490: ((X in Ra) & (Y in Ra) & (Z in Ra) & (X •Ra_GT Y) & (Y •Ra_GE Z)) •imp (X •Ra_GT Z)
(638) Theorem 491: ((X in Ra) & (Y in Ra) & (Z in Ra) & (X •Ra_GE Y) & (Y •Ra_GT Z)) •imp (X •Ra_GT Z)
(639) Theorem 492: ((X in Ra) & (Y in Ra) & (Z in Ra) & (X •Ra_GT Y) & (Y •Ra_GT Z)) •imp (X •Ra_GT Z)
(640) Theorem 493: (FORALL x in Ra, y in Ra, z in Ra | ((x •Ra_LT y) & (y •Ra_LT z)) •imp (x •Ra_LT z))
(643) Theorem 496: (FORALL x, y | smaller_Ra(x,y) = if ((x notin Ra) & (y notin Ra)) then Ra elseif (x notin Ra) then y elseif (y notin Ra) then x elseif (x •Ra_LT y) then x else y end if) & (FORALL x, y | smaller_Ra(x,y) = smaller_Ra(y,x)) & (FORALL x, y | ({x,y} •incin Ra) •imp (smaller_Ra(x,y) in {x,y})) & (FORALL x | (x in next(Ra)) •imp (smaller_Ra(x,Ra) = x)) & (FORALL x, y, z | smaller_Ra(x,smaller_Ra(y,z)) = smaller_Ra(smaller_Ra(x,y),z)) & (FORALL x, y | ((x in next(Ra)) & (y in next(Ra))) •imp (smaller_Ra(x,y) in next(Ra))) & (FORALL f,p,a | (Svm(f) & (range(f) •incin Ra) & Finite(f)) •imp (((p in f) •imp (min_over_Ra({p}) = (f~[car(p)]))) & (min_over_Ra(f) = smaller_Ra(min_over_Ra(f •ON (domain(f) * a)),min_over_Ra(f •ON (domain(f) - a)))))) & (FORALL f | (Svm(f) & (range(f) •incin Ra) & Finite(f) & (f /= 0)) •imp (min_over_Ra(f) in range(f))) & (FORALL x, y | ({x,y} •incin Ra) •imp ((smaller_Ra(x,y) = x) •eq ((x •Ra_LT y) or (x = y)))) & (FORALL t | ubs_Ra(t) = {x in Ra | (FORALL y in (t * Ra) | smaller_Ra(y,x) = y)}) & (FORALL t | max_Ra(t) = arb({Ra} + (t * ubs_Ra(t)))) & (FORALL t | lub_Ra(t) = arb({Ra} + {x in ubs_Ra(t) | ubs_Ra(t) •incin ubs_Ra({x})})) & (ubs_Ra(0) = Ra) & (max_Ra(0) = Ra) & (FORALL t | (ubs_Ra(t) •incin Ra) & (ubs_Ra(t) = ubs_Ra(t * Ra)) & (max_Ra(t) = max_Ra(t * Ra))) & (FORALL t, x | (Finite(t) & (x in t) & (t •incin Ra)) •imp ((max_Ra(t) in t) & ((x = max_Ra(t)) or ((x •Ra_LT max_Ra(t))))))
(644) Theorem 497: ((X in Ra) & (Y in Ra) & (XP in Ra) & (YP in Ra) & (X •Ra_GE Y) & (Y •Ra_GE Ra_0) & (YP •Ra_GE Ra_0) & (XP •Ra_GE YP)) •imp ((X •Ra_TIMES XP) •Ra_GE (Y •Ra_TIMES YP))
(645) Theorem 498: ((X in Ra) & (Y in Ra) & (XP in Ra) & (YP in Ra) & (X •Ra_GT Y) & (Y •Ra_GT Ra_0) & (YP •Ra_GT Ra_0) & (XP •Ra_GE YP)) •imp ((X •Ra_TIMES XP) •Ra_GT (Y •Ra_TIMES YP))
(646) Theorem 499: [The rational reciprocal is monotone decreasing for positive rationals] ((X in Ra) & (Y in Ra) & (X •Ra_GT Y) & (Y •Ra_GT Ra_0)) •imp (Recip(Y) •Ra_GT Recip(X))
(647) Theorem 500: [The average of two rational numbers lies between them] ((X in Ra) & (Y in Ra) & (X •Ra_GT Y)) •imp ((X •Ra_GT ((X •Ra_PLUS Y) •Ra_OVER (Ra_1 •Ra_PLUS Ra_1))) & (((X •Ra_PLUS Y) •Ra_OVER (Ra_1 •Ra_PLUS Ra_1)) •Ra_GT Y))
(648) Theorem 501: [Properties of the rational number 2] ((Ra_1 •Ra_PLUS Ra_1) in Ra) & ((Ra_1 •Ra_PLUS Ra_1) •Ra_GT Ra_0) & (Recip(Ra_1 •Ra_PLUS Ra_1) in Ra) & ((X in Ra) •imp ((X •Ra_OVER (Ra_1 •Ra_PLUS Ra_1)) in Ra))
(649) Theorem 502: [Any rational number can be divided into two equal halves] (X in Ra) •imp (X = ((X •Ra_OVER (Ra_1 •Ra_PLUS Ra_1)) •Ra_PLUS (X •Ra_OVER (Ra_1 •Ra_PLUS Ra_1))))
(650) Theorem 503: [Every positive rational exceeds the sum of two smaller positive rationals] ((X in Ra) & (X •Ra_GT Ra_0)) •imp (EXISTS e in Ra, e0 in Ra | (X •Ra_GT e) & (e •Ra_GT e0) & (e0 •Ra_GT Ra_0) & (e •Ra_GT Ra_0) & (X •Ra_GT (e •Ra_PLUS e0)))
(651) Theorem 504: [Every positive rational exceeds some smaller positive rational] ((X in Ra) & (X •Ra_GT Ra_0)) •imp (EXISTS e in Ra | (X •Ra_GT e) & (e •Ra_GT Ra_0))
(652) Theorem 505: [?] (X in Ra) •imp ((X •Ra_TIMES X) •Ra_GE Ra_0)
(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)))
(654) Theorem 507: ((X in Ra) & (Y in Ra) & (not(X •Ra_LE Y))) •imp (X •Ra_GT 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)))
(659) Theorem 512: [If the product of two rationals is 0, one of them is 0] ((X in Ra) & (Y in Ra)) •imp (((X •Ra_TIMES Y) = Ra_0) •eq ((X = Ra_0) or (Y = Ra_0)))
(660) Theorem 513: [Cancellation rule for rational multiplication] ((X in Ra) & (Y in Ra) & (U in Ra) & (X /= Ra_0) & ((X •Ra_TIMES Y) = (X •Ra_TIMES U))) •imp (Y = U)
(661) Theorem 514: [The reciprocal of a rational product is the product of the reciprocals] ((X in Ra) & (Y in Ra) & (X /= Ra_0) & (Y /= Ra_0)) •imp (Recip(X •Ra_TIMES Y) = (Recip(X) •Ra_TIMES Recip(Y)))
(662) Theorem 515: [Formula for the sum of two rational quotients] ((X in Ra) & (Y in Ra) & (U in Ra) & (V in Ra) & (X /= Ra_0) & (Y /= Ra_0)) •imp (((U •Ra_OVER X) •Ra_PLUS (V •Ra_OVER Y)) = (((Y •Ra_TIMES U) •Ra_PLUS (X •Ra_TIMES V)) •Ra_OVER (X •Ra_TIMES Y)))
(663) Theorem 516: ((X in Ra) & (Y in Ra) & (X /= Ra_0) & (Y /= Ra_0)) •imp ((Recip(X) •Ra_MINUS Recip(Y)) = ((Y •Ra_MINUS X) •Ra_OVER (X •Ra_TIMES 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))))
(667) Theorem 521: [The range of a rational sequence is included in the set of rationals] (F in RaSeq) •imp ((domain(F) = Za) & (range(F) •incin Ra) & ((X in Za) •imp (F~[X] in Ra)))
(668) Theorem 522: [Reformulation of condition for sequence equivalence] ({F,G} •incin RaSeq) •imp (Ra_eqseq(F,G) •eq (FORALL eps in Ra | (eps •Ra_GT Ra_0) •imp Finite({x : x in Za | Ra_ABS((F~[x]) •Ra_MINUS (G~[x])) •Ra_GT eps})))
(669) Theorem 523: [Condition for rational sequence equality] (FORALL n in Za | ((F in RaSeq) & (G in RaSeq) & (F~[n] = G~[n]))) •imp (F = G)
(675) Theorem 524: (X in Ra) •imp ((Za •PROD {X}) in RaCauchy)
(676) Theorem 525: (X in Ra) •imp (Ras_ABS(Za •PROD {X}) = (Za •PROD {Ra_ABS(X)}))
(678) Theorem 527: (F in RaSeq) •imp ((domain(F) = Za) & Svm(F) & (range(F) •incin Ra) & Ra_eqseq(F,F))
(679) Theorem 528: ((F in RaSeq) & (N in Za) & (I in Za)) •imp ((shifted_seq(F,N)~[I]) = (F~[N •PLUS I]))
(680) Theorem 529: (U in Za) •imp (((Ra0Seq~[U]) = Ra_0) & ((Ra1Seq~[U]) = Ra_1))
(681) Theorem 530: ((F in RaCauchy) & (G in Subseqs(F)) & (not Finite(G))) •imp ((G in RaCauchy) & Ra_eqseq(F,G))
(682) Theorem 531: (F in RaCauchy) •imp ((H in Za) •imp (F~[H] in Ra))
(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])))) ))
(685) Theorem 534: (({F,G,H} •incin RaSeq) & Ra_eqseq(F,G) & Ra_eqseq(G,H)) •imp Ra_eqseq(H,F)
(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])))))
(688) Theorem 537: ({F,G} •incin RaCauchy) •imp (((F •Ras_PLUS G) in RaCauchy) & (Ras_ABS(F) in RaCauchy) & (Ras_Rev(F) in RaCauchy))
(689) Theorem 538: ((S •incin Ra) & Finite(S)) •imp (EXISTS u in Ra | (FORALL y in S | u •Ra_GE y))
(690) Theorem 539: [Every finite set of integers has a strict upper bound] ((S •incin Za) & Finite(S)) •imp (EXISTS u in Za | (FORALL y in S | y in u))
(691) Theorem 540: [Every Cauchy sequence has an upper bound] (F in RaCauchy) •imp (EXISTS x in Ra | (FORALL y in range(F) | y •Ra_LE x))
(692) Theorem 541: (F in RaCauchy) •imp (EXISTS x in Ra | (FORALL y in range(F) | Ra_ABS(y) •Ra_LT x ))
(693) Theorem 542: ({F,G} •incin RaCauchy) •imp (((F •Ras_MINUS G) in RaCauchy) & ((F •Ras_TIMES G) in RaCauchy))
(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]))))))
(697) Theorem 546: ((G in RaCauchy) & (not Ra_eqseq(G,Ra0Seq))) •imp ({h in Za | (FORALL i in (Za - h) | (G~[i]) /= Ra_0)} /= 0)
(698) Theorem 547: ((F in RaSeq) & (M = arb({h in Za | (FORALL i in (Za - h) | (F~[i]) /= Ra_0)}))) •imp (Ras_Recip(F) = Ras_Recip(shifted_seq(F,M)))
(699) Theorem 548: ((F in RaCauchy) & (M in Za)) •imp ((shifted_seq(F,M) in RaCauchy) & Ra_eqseq(F,shifted_seq(F,M)))
(700) Theorem 549: ((F in RaCauchy) & (not Ra_eqseq(F,Ra0Seq))) •imp (EXISTS g in RaCauchy | Ra_eqseq(F,g) & (Ras_Recip(F) = Ras_Recip(g)) & (FORALL i in Za | ((g~[i]) /= Ra_0) & (Ras_Recip(g)~[i] = Recip(g~[i]))))
(701) Theorem 550: [The reciprocal of a non-null rational sequence is a rational sequence] ((G in RaCauchy) & (not Ra_eqseq(G,Ra0Seq))) •imp (Ras_Recip(G) in RaSeq)
(702) Theorem 551: [Reciprocal and quotient of rational Cauchy sequences are, when defined, Cauchy sequences] (({F,G} •incin RaCauchy) & (not Ra_eqseq(G,Ra0Seq))) •imp ((Ras_Recip(G) in RaCauchy) & ((F •Ras_OVER G) in RaCauchy))
(703) Theorem 552: (({F,G,Fp,Gp} •incin RaSeq) & Ra_eqseq(F,G) & Ra_eqseq(Fp,Gp)) •imp Ra_eqseq(F •Ras_PLUS Fp, G •Ras_PLUS Gp)
(704) Theorem 553: (({F,G,Fp,Gp} •incin RaCauchy) & Ra_eqseq(F,G) & Ra_eqseq(Fp,Gp)) •imp Ra_eqseq(F •Ras_PLUS Fp, G •Ras_PLUS Gp)
(705) Theorem 554: (({F,Fp,G} •incin RaCauchy) & Ra_eqseq(F,Fp)) •imp Ra_eqseq(F •Ras_TIMES G, Fp •Ras_TIMES G)
(706) Theorem 555: (({F,G,Fp,Gp} •incin RaCauchy) & Ra_eqseq(F,G) & Ra_eqseq(Fp,Gp)) •imp Ra_eqseq(F •Ras_TIMES Fp, G •Ras_TIMES Gp)
(707) Theorem 556: (({F,G} •incin RaCauchy) & Ra_eqseq(F,G)) •imp Ra_eqseq(Ras_Rev(F),Ras_Rev(G))
(708) Theorem 557: (({F,G} •incin RaCauchy) & Ra_eqseq(F,G)) •imp Ra_eqseq(Ras_ABS(F),Ras_ABS(G))
(709) Theorem 558: (({F,G} •incin RaCauchy) & Ra_eqseq(F,G) & (not(Ra_eqseq(F,Ra0Seq)))) •imp Ra_eqseq(Ras_Recip(F),Ras_Recip(G))
(710) Theorem 559: ({F,G} •incin RaSeq) •imp (F •Ras_PLUS G = G •Ras_PLUS F)
(711) Theorem 560: ({F,G} •incin RaSeq) •imp (F •Ras_TIMES G = G •Ras_TIMES F)
(712) Theorem 561: ({F,G,H} •incin RaSeq) •imp ((F •Ras_PLUS G) •Ras_PLUS H = F •Ras_PLUS (G •Ras_PLUS H))
(713) Theorem 562: ({F,G,H} •incin RaSeq) •imp ((F •Ras_TIMES G) •Ras_TIMES H = F •Ras_TIMES (G •Ras_TIMES H))
(714) Theorem 563: [Double-inversion law for rational sequences] (X in RaSeq) •imp (Ras_Rev(Ras_Rev(X))=X)
(715) Theorem 564: [Distributive law for multiplication of rational sequences] ({X,Y,V} •incin RaSeq) •imp ((X •Ras_TIMES (Y •Ras_PLUS V)) = ((X •Ras_TIMES Y) •Ras_PLUS (X •Ras_TIMES V)))
(716) Theorem 565: [Law of signs for multiplication of rational sequences] ({X,Y} •incin RaSeq) •imp ((X •Ras_TIMES Ras_Rev(Y)) = Ras_Rev(X •Ras_TIMES Y))
(717) Theorem 566: [Law of signs for multiplication of rational sequences, 2] ({X,Y} •incin RaSeq) •imp (((Ras_Rev(X) •Ras_TIMES Y) = Ras_Rev(X •Ras_TIMES Y)) & ((Ras_Rev(X) •Ras_TIMES Ras_Rev(Y)) = (X •Ras_TIMES Y)))
(718) Theorem 567: [Any rational sequence times 0 is 0] (X in RaSeq) •imp ((X •Ras_TIMES Ra0Seq) = Ra0Seq)
(719) Theorem 568: [0 is a right additive identity for rational sequences] (X in RaSeq) •imp (X •Ras_PLUS Ra0Seq = X)
(720) Theorem 569: [1 is a left multiplicative identity for rational sequences] (X in RaSeq) •imp (X •Ras_TIMES Ra1Seq = X)
(721) Theorem 570: [0 is right subtractive identity for rational sequence subtraction] (X in RaSeq) •imp (X •Ras_MINUS Ra0Seq = X)
(722) Theorem 571: [Basic properties of the signed negative for rational sequences] (X in RaSeq) •imp ((Ras_Rev(X) in RaSeq) & ((Ras_Rev(X) •Ras_PLUS X) = Ra0Seq) & (Ras_Rev(Ras_Rev(X)) = X))
(723) Theorem 572: [Reciprocal sequence principle] ((X in RaCauchy) & (not Ra_eqseq(X,Ra0Seq))) •imp Ra_eqseq(X •Ras_TIMES Ras_Recip(X),Ra1Seq)
(724) Theorem 573: [The negative of a sum of rational sequences is the sum of the negatives] ((X in RaSeq) & (Y in RaSeq)) •imp (Ras_Rev(X •Ras_PLUS Y) = Ras_Rev(X) •Ras_PLUS Ras_Rev(Y))
(725) Theorem 574: [A rational sequence minus itself gives 0] (X in RaSeq) •imp ((X •Ras_MINUS X) = Ra0Seq)
(726) Theorem 575: [Multiplication by Ras_Rev(Ra1Seq)] (X in RaSeq) •imp (Ras_Rev(X) = (Ras_Rev(Ra1Seq) •Ras_TIMES X))
(729) Theorem 578: [?] ((H in RaCauchy) & Ra_eqseq(H,Ra0Seq)) •imp (Ra_eqseq(Ras_ABS(H),Ra0Seq) & (Ra_eqseq(Ras_Rev(H),Ra0Seq)))
(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) ))
(731) Theorem 580: [All terms of a Cauchy sequence not equivalent to zero have the same sign beyond a certain point] ((F in RaCauchy) & (not Ra_eqseq(F,Ra0Seq))) •imp (EXISTS n in Za | shifted_seq(Ras_ABS(F),n) = if ((F~[n]) •Ra_GE Ra_0) then shifted_seq(F,n) else shifted_seq(Ras_Rev(F),n) end if)
(732) Theorem 581: [One of a Cauchy sequence F and its additive inverse is always equivalent to a non-negative sequence, and both are equivalent to non-negative sequences only if F is equivalent to zero] (F in RaCauchy) •imp (((Ra_eqseq(Ras_ABS(F),F) or Ra_eqseq(Ras_ABS(F),Ras_Rev(F)))) & (((Ra_eqseq(Ras_ABS(F),F) & Ra_eqseq(Ras_ABS(F),Ras_Rev(F)))) •imp Ra_eqseq(F,Ra0Seq)))
(734) Theorem 583: [A rational sequence F and its additive inverse have the same absolute value] (F in RaSeq) •imp (Ras_ABS(Ras_Rev(F)) = Ras_ABS(F))
(735) Theorem 584: (F in RaSeq) •imp (((F •Ras_PLUS Ra0Seq) = F) & ((F •Ras_TIMES Ra1Seq) = F))
(737) Theorem 586: ((F in RaCauchy) & (G in RaCauchy)) •imp ((Ra_eqseq(F,G) •eq Ra_eqseq(G,F)) & Ra_eqseq(F,F))
(738) Theorem 587: (FORALL f in RaCauchy, g in RaCauchy, h in RaCauchy | (Ra_eqseq(f,g) & Ra_eqseq(g,h)) •imp Ra_eqseq(f,h))
(739) Theorem 588: (FORALL x, y | ((x in RaCauchy) & (y in RaCauchy)) •imp ((Ra_eqseq(x,y) •eq (Cauchy_to_Re(x) = Cauchy_to_Re(y))))) & (FORALL x | (x in Re) •imp ((arb(x) in RaCauchy) & (Cauchy_to_Re(arb(x)) = x))) & (FORALL x | (x in RaCauchy) •imp (Cauchy_to_Re(x) in Re)) & (FORALL x | (x in RaCauchy) •imp Ra_eqseq(x,arb(Cauchy_to_Re(x))))
(740) Theorem 589: ((X in RaCauchy) & (Y in RaCauchy)) •imp ((Ra_eqseq(X,Y) •eq (Cauchy_to_Re(X) = Cauchy_to_Re(Y))) & (Cauchy_to_Re(X) in Re) & Ra_eqseq(X,arb(Cauchy_to_Re(X))))
(741) Theorem 590: (X in Re) •imp ((arb(X) in RaCauchy) & (arb(X) in RaSeq) & (Cauchy_to_Re(arb(X)) = X))
(743) Theorem 592: ({X,Y} •incin Re) •imp (((X •R_PLUS Y) in Re) & (R_Rev(X) in Re))
(744) Theorem 593: ({X,Y} •incin Re) •imp (((X •R_MINUS Y) in Re) & ((X •R_TIMES Y) in Re))
(745) Theorem 594: [Commutative law for real addition] ({X,Y} •incin Re) •imp ((X •R_PLUS Y) = (Y •R_PLUS X))
(746) Theorem 595: [Elementary algebraic lemma for real addition] ((X in RaCauchy) & (Y in RaCauchy)) •imp (Cauchy_to_Re(X •Ras_PLUS Y) = (Cauchy_to_Re(X) •R_PLUS Cauchy_to_Re(Y)))
(747) Theorem 596: [Associative law for real addition] ({X,Y,V} •incin Re) •imp ((X •R_PLUS (Y •R_PLUS V)) = ((X •R_PLUS Y) •R_PLUS V))
(748) Theorem 597: [Commutative law for real multiplication] ({X,Y} •incin Re) •imp ((X •R_TIMES Y) = (Y •R_TIMES X))
(749) Theorem 598: [Elementary algebraic lemma for real multiplication] ((X in RaCauchy) & (Y in RaCauchy)) •imp (Cauchy_to_Re(X •Ras_TIMES Y) = (Cauchy_to_Re(X) •R_TIMES Cauchy_to_Re(Y)))
(750) Theorem 599: [Associative law for real multiplication] ({X,Y,V} •incin Re) •imp ((X •R_TIMES (Y •R_TIMES V)) = ((X •R_TIMES Y) •R_TIMES V))
(751) Theorem 600: [Distributive law for real multiplication] ({X,Y,V} •incin Re) •imp ((X •R_TIMES (Y •R_PLUS V)) = ((X •R_TIMES Y) •R_PLUS (X •R_TIMES V)))
(752) Theorem 601: [Lemma for law of signs] (X in RaCauchy) •imp (Cauchy_to_Re(Ras_Rev(X)) = R_Rev(Cauchy_to_Re(X)))
(753) Theorem 602: [Law of signs for real multiplication] ({X,Y} •incin Re) •imp (((X •R_TIMES R_Rev(Y)) = R_Rev(X •R_TIMES Y)) & ((R_Rev(X) •R_TIMES Y) = R_Rev(X •R_TIMES Y)) & ((R_Rev(X) •R_TIMES R_Rev(Y)) = (X •R_TIMES Y)))
(754) Theorem 603: [Any real times 0 is 0] (X in Re) •imp ((X •R_TIMES R_0) = R_0)
(755) Theorem 604: [0 times any real is 0] (X in Re) •imp (R_0 •R_TIMES X = R_0)
(756) Theorem 605: [0 is a right and left additive identity for reals] (X in Re) •imp ((X •R_PLUS R_0 = X) & (R_0 •R_PLUS X = X))
(757) Theorem 606: [1 is a right multiplicative identity for reals] (X in Re) •imp (X •R_TIMES R_1 = X)
(758) Theorem 607: [1 is a left multiplicative identity for reals] (X in Re) •imp (R_1 •R_TIMES X = X)
(760) Theorem 609: [0 is right identity for real subtraction] (X in Re) •imp (X •R_MINUS R_0 = X)
(761) Theorem 610: [Real subtraction principle] (X in Re) •imp (X •R_MINUS X = R_0)
(762) Theorem 611: [Basic properties of the signed negative for reals] (X in Re) •imp ((R_Rev(X) in Re) & ((R_Rev(X) •R_PLUS X) = R_0))
(762+) Theorem 612: [Basic properties of the signed negative for reals, 2] (X in Re) •imp (R_Rev(R_Rev(X)) = X)
(763) Theorem 613: [Real additive Cancellation] ((X in Re) & (Y in Re) & (V in Re) & (X •R_PLUS V = Y •R_PLUS V)) •imp (X = Y)
(764) Theorem 614: [Real subtraction is addition of the negative] ((X in Re) & (Y in Re)) •imp ((X •R_MINUS Y) = (X •R_PLUS R_Rev(Y)))
(765) Theorem 615: [The sum of a real number and its additive inverse is zero] (X in Re) •imp ((R_Rev(X) in Re) & ((X •R_PLUS R_Rev(X)) = R_0))
(766) Theorem 616: [The negative of a real x is zero iff x is zero] (X in Re) •imp ((R_Rev(X) = R_0) •eq (X = R_0))
(767) Theorem 617: [The negative of a real sum is the sum of the negatives] ((X in Re) & (Y in Re)) •imp (R_Rev(X •R_PLUS Y) = R_Rev(X) •R_PLUS R_Rev(Y))
(768) Theorem 618: [Real addition-subtraction commutativity] ((X in Re) & (Y in Re) & (V in Re)) •imp (X •R_MINUS (Y •R_PLUS V) = (X •R_MINUS Y) •R_MINUS V)
(769) Theorem 619: [Real subtraction reverses addition] ((X in Re) & (Y in Re)) •imp ((X •R_PLUS Y) •R_MINUS Y = X)
(770) Theorem 620: [Real subtraction reverses addition, 2] ((X in Re) & (Y in Re)) •imp (X = (Y •R_PLUS (X •R_MINUS Y)))
(771) Theorem 621: [Multiplication by R_Rev(R_1)] (X in Re) •imp (R_Rev(X) = R_Rev(R_1) •R_TIMES X)
(772) Theorem 622: [Distributivity of multiplication over subtraction] ((X in Re) & (Y in Re) & (V in Re)) •imp ((X •R_TIMES (Y •R_MINUS V)) = ((X •R_TIMES Y) •R_MINUS (X •R_TIMES V)))
(773) Theorem 623: [Additive inverse of real difference] ((X in Re) & (Y in Re)) •imp (R_Rev(X •R_MINUS Y) = (Y •R_MINUS X))
(774) Theorem 624: [Real reciprocal principle] ((X in Re) & (X /= R_0)) •imp (X •R_TIMES R_Recip(X) = R_1)
(775) Theorem 625: [Real division principle] ((X in Re) & (X /= R_0)) •imp (X •R_OVER X = R_1)
(776) Theorem 626: [Basic properties of the reciprocal for reals] ((X in Re) & (X /= R_0)) •imp ((R_Recip(X) in Re) & (R_Recip(X) /= R_0) & ((R_Recip(X) •R_TIMES X) = R_1))
(777) Theorem 627: [Basic properties of the reciprocal for reals, 2] ((X in Re) & (X /= R_0)) •imp (R_Recip(R_Recip(X)) = X)
(778) Theorem 628: [Reverse of real reciprocal] ((X in Re) & (X /= R_0)) •imp (R_Recip(R_Rev(X)) = R_Rev(R_Recip(X)))
(779) Theorem 629: [Real multiplicative Cancellation] ((X in Re) & (Y in Re) & (V in Re) & (X •R_TIMES V = Y •R_TIMES V) & (V /= R_0)) •imp (X = Y)
(780) Theorem 630: [Reals are closed under division] ((X in Re) & (Y in Re) & (Y /= R_0)) •imp ((X •R_OVER Y in Re) & ((X /= R_0) •imp ((X •R_OVER Y /= R_0) & (X •R_TIMES Y /= R_0))))
(781) Theorem 631: [Real division is multiplication by the reciprocal] ((X in Re) & (Y in Re) & (Y /= R_0)) •imp ((X •R_OVER Y) = (X •R_TIMES R_Recip(Y)))
(782) Theorem 632: [The reciprocal of a real product is the product of the reciprocals] ((X in Re) & (Y in Re) & (X /= R_0) & (Y /= R_0)) •imp ((X •R_TIMES Y /= R_0) & R_Recip(X •R_TIMES Y) = R_Recip(X) •R_TIMES R_Recip(Y))
(783) Theorem 633: [Real multiplication-division commutativity] ((X in Re) & (Y in Re) & (Y /= R_0) & (V in Re) & (V /= R_0)) •imp (X •R_OVER (Y •R_TIMES V) = (X •R_OVER Y) •R_OVER V)
(784) Theorem 634: [A real divided by itself gives 1] ((X in Re) & (X /= R_0)) •imp (X •R_OVER X = R_1)
(785) Theorem 635: [Real reciprocal as a quotient] ((X in Re) & (X /= R_0)) •imp (R_Recip(X) = R_1 •R_OVER X)
(786) Theorem 636: [Distributivity of division over addition] ((X in Re) & (Y in Re) & (V in Re) & (V /= R_0)) •imp ((X •R_PLUS Y) •R_OVER V = ((X •R_OVER V) •R_PLUS (Y •R_OVER V)))
(787) Theorem 637: [Real division reverses multiplication] ((X in Re) & (Y in Re) & (Y /= R_0)) •imp ((X •R_TIMES Y) •R_OVER Y = X)
(788) Theorem 638: [Real division reverses multiplication,2] ((X in Re) & (Y in Re) & (Y /= R_0)) •imp (X = (Y •R_TIMES (X •R_OVER Y)))
(789) Theorem 639: [Distributivity of division over subtraction] ((X in Re) & (Y in Re) & (V in Re) & (V /= R_0)) •imp (((X •R_MINUS Y) •R_OVER V) = ((X •R_OVER V) •R_MINUS (Y •R_OVER V)))
(790) Theorem 640: (X in Re) •imp ((R_Rev(X) = Cauchy_to_Re(arb(R_Rev(X)))) & Ra_eqseq(Ras_ABS(arb(X)),arb(Cauchy_to_Re(Ras_ABS(arb(X))))))
(791) Theorem 641: ((X in Re) & (Y in Re)) •imp Ra_eqseq((arb(X) •Ras_PLUS arb(Y)),arb(Cauchy_to_Re(arb(X) •Ras_PLUS arb(Y))))
(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))
(797) Theorem 647: [Transitivity of ordering] ((X in Re) & (Y in Re) & (Z in Re) & (X •R_GE Y) & (Y •R_GE Z)) •imp (X •R_GE Z)
(798) Theorem 648: [The reals are a linearly ordered set] ((X in Re) & (Y in Re)) •imp ((X •R_GT Y) or (X = Y) or (Y •R_GT X))
(799) Theorem 649: [The reals are a linearly ordered set, 2] ((X in Re) & (Y in Re)) •imp ((X •R_LT Y) or (X = Y) or (Y •R_LT X))
(801) Theorem 651: [The reals are a linearly ordered set, 3] ((X in Re) & (Y in Re)) •imp (((X •R_GE Y) or (Y •R_GE X)) & (((X •R_GE Y) & (Y •R_GE X)) •imp (X = Y)))
(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))
(805) Theorem 655: [Transitivity of ordering, strict case] ((X in Re) & (Y in Re) & (Z in Re) & (X •R_GT Y) & (Y •R_GE Z)) •imp (X •R_GT Z)
(806) Theorem 656: [Transitivity of ordering, strict case 2] ((X in Re) & (Y in Re) & (Z in Re) & (X •R_GE Y) & (Y •R_GT Z)) •imp (X •R_GT Z)
(807) Theorem 657: [Transitivity of ordering,strict case 3] ((X in Re) & (Y in Re) & (Z in Re) & (X •R_GT Y) & (Y •R_GT Z)) •imp (X •R_GT Z)
(808) Theorem 658: [Greater_than_equal is greater-than and equal] ((X in Re) & (Y in Re)) •imp ((X •R_GE Y) •eq ((X •R_GT Y) or (X = Y)))
(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))
(810) Theorem 660: [Less_than_equal is less-than and equal] ((X in Re) & (Y in Re)) •imp ((X •R_LE Y) •eq ((X •R_LT Y) or (X = Y)))
(811) Theorem 661: [Transitivity of ordering by 'less than'] ((X in Re) & (Y in Re) & (Z in Re)) •imp (((X •R_LE Y) & (Y •R_LT Z)) •imp (X •R_LT Z))
(812) Theorem 662: [Transitivity of ordering by 'less than', 2] ((X in Re) & (Y in Re) & (Z in Re)) •imp (((X •R_LT Y) & (Y •R_LE Z)) •imp (X •R_LT Z))
(813) Theorem 663: [Transitivity of ordering by 'less than', 3] ((X in Re) & (Y in Re) & (Z in Re)) •imp (((X •R_LT Y) & (Y •R_LT Z)) •imp (X •R_LT Z))
(815) Theorem 665: [Sign reversal inverts comparisons] ((X in Re) & (Y in Re) & (X •R_GE Y)) •imp (R_Rev(Y) •R_GE R_Rev(X))
(816) Theorem 666: [Sign reversal inverts comparisons,2] ((X in Re) & (Y in Re)) •imp (((X •R_GE Y) •eq (R_Rev(Y) •R_GE R_Rev(X))) & ((X •R_GT Y) •eq (R_Rev(Y) •R_GT R_Rev(X))))
(818) Theorem 668: [Monotonicity of addition over 2nd argument] ((X in Re) & (XP in Re) & (YP in Re) & (XP •R_GE YP)) •imp ((X •R_PLUS XP) •R_GE (X •R_PLUS YP))
(819) Theorem 669: [Monotonicity of addition] ((X in Re) & (Y in Re) & (XP in Re) & (YP in Re) & (X •R_GE Y) & (XP •R_GE YP)) •imp ((X •R_PLUS XP) •R_GE (Y •R_PLUS YP))
(820) Theorem 670: [Strict monotonicity of addition] ((X in Re) & (Y in Re) & (XP in Re) & (YP in Re) & (X •R_GE Y) & (XP •R_GT YP)) •imp ((X •R_PLUS XP) •R_GT (Y •R_PLUS YP))
(821) Theorem 671: [Strict monotonicity of addition, 2] ((X in Re) & (Y in Re) & (V in Re) & (X •R_GE Y)) •imp (((Y •R_PLUS V) •R_GE (X •R_PLUS V)) •eq (X = Y))
(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))
(823) Theorem 672: [The product of two reals is 0 if and only if one of them is 0] ((X in Re) & (Y in Re)) •imp (((X •R_TIMES Y) = R_0) •eq ((X = R_0) or (Y = R_0)))
(824) Theorem 673: [Monotonicity of multiplication over 2nd argument] ((X in Re) & (XP in Re) & (YP in Re) & (X •R_GE R_0) & (XP •R_GE YP)) •imp ((X •R_TIMES XP) •R_GE (X •R_TIMES YP))
(825) Theorem 674: [Monotonicity of multiplication] ((X in Re) & (Y in Re) & (XP in Re) & (YP in Re) & (X •R_GE Y) & (Y •R_GE R_0) & (YP •R_GE R_0) & (XP •R_GE YP)) •imp ((X •R_TIMES XP) •R_GE (Y •R_TIMES YP))
(826) Theorem 675: [Strict monotonicity of multiplication over 2nd argument] ((X in Re) & (XP in Re) & (YP in Re) & (X •R_GT R_0) & (XP •R_GT YP)) •imp ((X •R_TIMES XP) •R_GT (X •R_TIMES YP))
(827) Theorem 676: [Strict monotonicity of multiplication] ((X in Re) & (Y in Re) & (XP in Re) & (YP in Re) & (X •R_GE Y) & (Y •R_GT R_0) & (YP •R_GT R_0) & (XP •R_GT YP)) •imp ((X •R_TIMES XP) •R_GT (Y •R_TIMES YP))
(828) Theorem 677: [Multiplication by a positive real is strictly monotone] ((X in Re) & (Y in Re) & (Z in Re) & (X •R_GT Y) & (Z •R_GT R_0)) •imp ((X •R_TIMES Z) •R_GT (Y •R_TIMES Z))
(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)
(831) Theorem 680: [Condition for positiveness of a product of reals] ((X in Re) & (Y in Re)) •imp (((X •R_TIMES Y) •R_GT R_0) •eq (((X •R_GT R_0) & (Y •R_GT R_0)) or ((R_0 •R_GT X) & (R_0 •R_GT Y))))
(832) Theorem 681: [The reciprocal of a positive real is positive] ((X in Re) & (X •R_GT R_0)) •imp (R_Recip(X) •R_GT R_0)
(833) Theorem 682: [The sum of non-negative reals is at least as big at each addend] ((X in Re) & (Y in Re) & (X •R_GE R_0)) •imp ((X •R_PLUS Y) •R_GE Y)
(834) Theorem 683: [The reciprocal is monotone decreasing for positive reals] ((X in Re) & (Y in Re) & (X •R_GT Y) & (Y •R_GT R_0)) •imp (R_Recip(Y) •R_GT R_Recip(X))
(835) Theorem 683a: [Two non-null reals are equal iff their reciprocals are equal] ((X in Re) & (X /= R_0) & (Y in Re) & (Y /= R_0) & (R_Recip(X) = R_Recip(Y))) •imp (X = Y)
(836) Theorem 684: [The square of any real is non-negative] (X in Re) •imp R_is_nonneg(X •R_TIMES X)
(837) Theorem 684a: [Monotonicity of squaring] ((X in Re) & (Y in Re) & (X •R_GE R_0) & (Y •R_GE R_0)) •imp ((X •R_GE Y) •eq ((X •R_TIMES X) •R_GE (Y •R_TIMES Y)))
(838) Theorem 685: [Properties of the real number 2] ((R_1 •R_PLUS R_1) in Re) & ((R_1 •R_PLUS R_1) •R_GT R_0) & (R_Recip(R_1 •R_PLUS R_1) in Re) & (R_Recip(R_1 •R_PLUS R_1) /= R_0) & ((X in Re) •imp ((X •R_OVER (R_1 •R_PLUS R_1)) in Re))
(839) Theorem 686: [Any real number can be divided into two equal halves] (X in Re) •imp (X = (X •R_OVER (R_1 •R_PLUS R_1)) •R_PLUS (X •R_OVER (R_1 •R_PLUS R_1)))
(840) Theorem 687: [The average of two real numbers lies between them] ((X in Re) & (Y in Re) & (X •R_GT Y)) •imp ((X •R_GT ((X •R_PLUS Y) •R_OVER (R_1 •R_PLUS R_1))) & (((X •R_PLUS Y) •R_OVER (R_1 •R_PLUS R_1)) •R_GT Y))
(841) Theorem 688: [Every positive real exceeds the sum of two smaller positive reals] ((X in Re) & (X •R_GT R_0)) •imp (EXISTS E in Re , E0 in Re | (X •R_GT E) & (E •R_GT E0) & (E0 •R_GT R_0) & (E •R_GT R_0) & (X •R_GT (E •R_PLUS E0)))
(842) Theorem 689: [Every positive real exceeds some smaller positive real] ((X in Re) & (X •R_GT R_0)) •imp (EXISTS E in Re | (X •R_GT E) & (E •R_GT R_0))
(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)
(848) Theorem 695: [The absolute value of a real product is the product of absolute values] ((X in Re) & (Y in Re)) •imp (abs(X •R_TIMES Y) = (abs(X) •R_TIMES abs(Y)))
(849) Theorem 696: [x and -x have the same absolute value] (X in Re) •imp (abs(X) = abs(R_Rev(X)))
(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)))
(852) Theorem 699: ((X in Re) & (Y in Re)) •imp (((X •R_PLUS abs(Y)) •R_GE X))
(853) Theorem 700: ((X in Re) & (Y in Re)) •imp (((abs(X) •R_PLUS abs(Y)) •R_GT abs(X •R_PLUS Y)) or ((abs(X) •R_PLUS abs(Y)) = abs(X •R_PLUS Y)))
(854) Theorem 701: [The absolute value of a real quotient is the quotient of absolute values] ((X in Re) & (Y in Re) & (Y /= R_0)) •imp ((abs(X) •R_OVER abs(Y)) = abs(X •R_OVER Y))
(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))))
(858) Theorem 705: [The embedding of rationals into reals preserves all elementary algebraic operations, 2] ((X in Ra) & (Y in Ra)) •imp ((ReRa(X) in Re) & (ReRa(Y) in Re) & (ReRa(X •Ra_PLUS Y) = ReRa(X) •R_PLUS ReRa(Y)) & (ReRa(X •Ra_TIMES Y) = ReRa(X) •R_TIMES ReRa(Y)))
(859) Theorem 706: [The embedding of rationals into reals preserves all elementary algebraic operations, 3] ((X in Ra) & (Y in Ra)) •imp (ReRa(X •Ra_MINUS Y) = (ReRa(X) •R_MINUS ReRa(Y)))
(860) Theorem 707: [The embedding of rationals into reals is 1-1] ((X in Ra) & (Y in Ra)) •imp ((ReRa(X) = ReRa(Y)) •eq (X = Y))
(862) Theorem 709: [The embedding of rationals into reals preserves quotients by nonzero quantities] ((X in Ra) & (Y in Ra) & (Y /= Ra_0)) •imp ((R_Recip(ReRa(Y)) = ReRa(Recip(Y))) & ((ReRa(X) •R_OVER ReRa(Y)) = ReRa(X •Ra_OVER Y)))
(863) Theorem 710: [The embedding of rationals into reals preserves ordering] ((X in Ra) & (Y in Ra)) •imp (((ReRa(X) •R_GE ReRa(Y)) •eq (X •Ra_GE Y)) & ((ReRa(X) •R_GT ReRa(Y)) •eq (X •Ra_GT Y)) & ((ReRa(Y) •R_LE ReRa(X)) •eq (Y •Ra_LE X)) & ((ReRa(Y) •R_LT ReRa(X)) •eq (Y •Ra_LT X)))
(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))))
(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)))
(871) Theorem 718: [The embedding of integers into signed integers is 1-1] ((X in Za) & (Y in Za) & (SiZa(X) = SiZa(Y))) •imp (X = Y)
(873) Theorem 720: [The embedding of integers into signed integers preserves ordering] ((X in Za) & (Y in Za)) •imp (((SiZa(X) •S_GE SiZa(Y)) •eq (X incs Y)) & ((SiZa(X) •S_GT SiZa(Y)) •eq (Y in X)) & ((SiZa(Y) •S_LE SiZa(X)) •eq (Y •incin X)) & ((SiZa(Y) •S_LT SiZa(X)) •eq (Y in X)))
(874) Theorem 721: [Elementary properties of the real absolute value] ((X in Re) & (Y in Re)) •imp ((abs(X) in Re) & (abs(Y) in Re) & (abs(X •R_TIMES Y) = (abs(X) •R_TIMES abs(Y))) & ((abs(X) •R_PLUS abs(Y)) •R_GE abs(X •R_PLUS Y) & (abs(R_Rev(X)) = abs(X))))
(875) Theorem 722a: [Every real Cauchy sequence can be approximated by a rational sequence] (F in ReCauchy) •imp (Ra_approx(F) in {g in RaCauchy | Ra_apseq(F,g)})
(876) Theorem 722b: [Every real Cauchy sequence has a real limit] (F in ReCauchy) •imp ((Ra_approx(F) in RaCauchy) & (Ra_approx(F) in RaSeq) & Ra_apseq(F,Ra_approx(F)) & (limit(F) in Re))
(877) Theorem 722: [The limit of a real Cauchy sequence is the real defined by any of its rational approximations] ((F in ReCauchy) & (G in RaSeq) & Ra_apseq(F,G)) •imp ((G in RaCauchy) & (Cauchy_to_Re(G) = limit(F)))
(878) Theorem 723: [The elementary operations on reals map Cauchy sequences into Cauchy sequences] ((F in ReCauchy) & (G in ReCauchy) & (Fp in RaCauchy) & (Gp in RaCauchy) & Ra_apseq(F,Fp) & Ra_apseq(G,Gp)) •imp ((((F •Res_PLUS G in ReCauchy) & Ra_apseq(F •Res_PLUS G,Fp •Ras_PLUS Gp))) & (((F •Res_MINUS G in ReCauchy) & Ra_apseq(F •Res_MINUS G,Fp •Ras_MINUS Gp))) & (((F •Res_TIMES G in ReCauchy) & Ra_apseq(F •Res_TIMES G,Fp •Ras_TIMES Gp))))
(879) Theorem 724: [The limit of a sum is the sum of limits] ((F in ReCauchy) & (G in ReCauchy)) •imp (limit(F •Res_PLUS G) = (limit(F) •R_PLUS limit(G)))
(880) Theorem 725: [The limit of a difference is the difference of limits] ((F in ReCauchy) & (G in ReCauchy)) •imp (limit(F •Res_MINUS G) = limit(F) •R_MINUS limit(G))
(881) Theorem 726: [The limit of a product is the product of limits] ((F in ReCauchy) & (G in ReCauchy)) •imp (limit(F •Res_TIMES G) = limit(F) •R_TIMES limit(G))
(882) Theorem 727: [The limit of a quotient is the quotient of limits, provided that the denominator limit is non-zero] ((F in ReCauchy) & (G in ReCauchy) & (limit(G) /= R_0)) •imp (limit(F •Res_OVER G) = limit(F) •R_OVER limit(G))
(883) Theorem 728: [Any real x is included between two rationals which can be arbitrarily close together] ((X in Re) & (EPS in Re) & (EPS •R_GT R_0)) •imp (EXISTS r1 in Ra, r2 in Ra | ((ReRa(r1) •R_GT X) & (X •R_GT ReRa(r2)) & (ReRa(r1 •Ra_MINUS r2) •R_LE EPS)))
(884) Theorem 729: [For any real x, there exists a rational r such that r >= x] (x in Re) •imp (EXISTS r in Ra | ReRa(r) •R_GT x)
(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))))
(886) Theorem 731: [For any rational r, there exists an integer n such that n >= r] (r in Ra) •imp (EXISTS n in Za | RaSi(SiZa(n)) •R_GE x)
(887) Theorem 732: [For any real x, there exists an integer n such that n > x] (x in Re) •imp (EXISTS n in Za | ReRa(RaSi(SiZa(n))) •R_GT x)
(888) Theorem 733: [For any real x and eps > 0, there exists an integer n such that n • eps > x] ((x in Re) & (eps in Re) & (eps •R_GT R_0)) •imp (EXISTS n in Za | ((ReRa(RaSi(SiZa(n))) •R_TIMES e) •R_GT x))
(889) Theorem 734: [For any real x and eps > 0, there exists an integer n such that eps > x/n] ((x in Re) & (eps in Re) & (eps •R_GT R_0)) •imp (EXISTS n in Za | (eps •R_GT (x •R_OVER ReRa(RaSi(SiZa(n))))))
(890) Theorem 735: [For any non-negative real x and eps > 0, there exists an integer n such that n •R_TIMES eps > x and (n - 1) • eps <= x] ((x in Re) & (eps in Re) & (eps •R_GT R_0)) •imp (EXISTS n in Za | (e •R_GT (x •R_OVER ReRa(RaSi(SiZa(n))))))
(891) Theorem 736: [Every positive real is bounded below by a rational fraction of the form 1/n] ((x in Re) & (x •R_GT R_0)) •imp (EXISTS n in Za | (R_1 •R_OVER ReRa(RaSi(SiZa(n)))) •R_LT x)
(892) Theorem 737: [Every real Cauchy sequence is approximated by a rational Cauchy sequence] (F in ReCauchy) •imp (EXISTS g in RaCauchy | Ra_apseq(F,g))
(893) Theorem 738: [Any two approximating rational sequences for a given real Cauchy sequence are equivalent] ((F in ReCauchy) & Ra_apseq(F,G) & Ra_apseq(F,GP)) •imp ((G in RaCauchy) & (GP in RaCauchy) & (Cauchy_to_Re(G) = Cauchy_to_Re(GP)))
(894) Theorem 739: [For any non-empty set s of reals which is bounded above, and for any positive real eps, there exists an u in s such that u + eps is an upper bound of s] ((s •incin Re) & (s /= 0) & (eps in Re) & (eps •R_GT R_0) & (y in Re) & (FORALL x in s | y •R_GE x)) •imp (EXISTS u in s | (FORALL x in s | u •R_GE x))
(895) Theorem 740: [Any bounded set of reals has a least upper bound] ((S •incin Re) & (S /= 0) & (EXISTS y in Re | (FORALL x in s | y •R_GE x))) •imp (EXISTS u in Re | ((FORALL x in s | u •R_GE x) & (FORALL v in Re | (v •R_LT u •imp (not (FORALL x in s | v •R_GE x))))))
(896) Theorem 741: (FORALL s, x | (Finite(s) •imp (ToThe1(s,x) = if (s = 0) then R_1 else ToThe1(s - {arb(s)},x) •R_TIMES x end if)))
(897) Theorem 742: ((N in Za) & (X in Re)) •imp (X •ToThe N = if (N = 0) then R_1 else X •R_TIMES (X •ToThe (N - 1)) end if)
(898) Theorem 743: (X in Re) •imp ((X •ToThe 0 = R_0) & (X •ToThe 1 = X) & (((M in Za) & (N in Za)) •imp (X •ToThe (M •PLUS N) = (X •ToThe M) •R_TIMES (X •ToThe N))))
(899) Theorem 744: ((X in Re) & (M in Za) & (N in Za)) •imp (((X •ToThe M) •ToThe N) = (X •ToThe (M •TIMES N)))
(900) Theorem 745: (R_SIGMA(0) = R_0) & (FORALL x in OM | (cdr(x) in Re) •imp (R_SIGMA({x}) = cdr(x))) & (FORALL f in OM | (Finite(f) & (range(f) •incin Re)) •imp (R_SIGMA(f) in Re)) & (FORALL f in OM, c in f | (Finite(f) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA(f - {c}) •R_PLUS cdr(c))) & (FORALL f in OM | (Finite(f) & Is_map(f) & (range(f) •incin Re)) •imp (FORALL t | R_SIGMA(f) = R_SIGMA(f •ON (domain(f) * t)) •R_PLUS R_SIGMA(f •ON (domain(f) - t)))) & (FORALL f in OM, g | (Finite(f) & Svm(f) & Svm(g) & (domain(f) = domain(g)) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA({[y,R_SIGMA(f •ON (g •INV_IM {y}))]: y in range(g)}))) & (FORALL f in OM, g | (Finite(f) & Svm(f) & one_1_map(g) & (domain(f) = domain(g)) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA({[y,f~[inv(g)~[y]]]: y in range(g)})))
(901) Theorem 746: (R_SIGMA(0) = R_0) & ((cdr(X) in Re) •imp (R_SIGMA({X}) = cdr(X))) & ((Finite(F) & (range(F) •incin Re)) •imp (R_SIGMA(F) in Re)) & ((Finite(F) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA(F - {c}) •R_PLUS cdr(c))) & ((Finite(F) & Is_map(F) & (range(F) •incin Re)) •imp R_SIGMA(F) = R_SIGMA(F •ON (domain(F) * T)) •R_PLUS R_SIGMA(F •ON (domain(F) - T))) & ((Finite(F) & Svm(F) & Svm(G) & (domain(F) = domain(G)) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA({[y,R_SIGMA(F •ON (G •INV_IM {y}))]: y in range(G)}))) & ((Finite(F) & Svm(F) & one_1_map(G) & (domain(F) = domain(G)) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA({[y,F~[inv(G)~[y]]]: y in range(G)})))
(902) Theorem 747: ((F in Fin_Seqs(Re)) & (G in Fin_Seqs(Re)) & (X in Re)) •imp (((Polval(F,X) •R_PLUS Polval(G,X)) = Polval(F •PolPlus G,X)) & ((Polval(F,X) •R_MINUS Polval(G,X)) = Polval(F •PolMinus G,X)) & ((Polval(F,X) •R_TIMES Polval(G,X)) = Polval(F •PolTimes G,X)))
(903) Theorem 748: ((F in Fin_Seqs(Re)) & (G in Fin_Seqs(Re))) •imp (((PolFcn(F) •F_PLUS PolFcn(G)) = PolFcn(F •PolPlus G)) & ((PolFcn(F) •F_MINUS PolFcn(G)) = PolFcn(F •PolMinus G)) & ((PolFcn(F) •F_TIMES PolFcn(G)) = PolFcn(F •PolTimes G)))
(904) Theorem 749: [Continuous functions map limits into limits] (Cf_RR(F,S) & (G in ReCauchy) & (range(G) •incin S)) •imp ((F @ G in ReCauchy) & (limit(F @ G) = F~[limit(G)]))
(905) Theorem 750: [The pointwise sum and product of two real continuous functions on two sets is continuous on their intersection] (Cf_RR(F,S) & Cf_RR(G,S2)) •imp (Cf_RR(F •Res_PLUS G,S * S2) & Cf_RR(F •Res_TIMES G,S * S2))
(906) Theorem 751: [The quotient of two real continuous functions on two sets is continuous on the set of points in their intersection at which the denominator is nonzero] (Cf_RR(F,S) & Cf_RR(G,S2)) •imp Cf_RR(F •Res_OVER G,{x in S * S2 | G~[x] /= R_0})
(907) Theorem 752: [The composition of two real continuous functions is continuous.] (Cf_RR(F,S) & Cf_RR(G,T) & (range(G •ON T) •incin S)) •imp Cf_RR(F @ G,T)
(908) Theorem 753: [Polynomial functions are continuous everywhere] (F in Fin_Seqs(Re)) •imp Cf_RR(PolFcn(F),Re)
(909) Theorem 754: [Polynomial quotients are continuous wherever their denominator is nonzero] ((F in Fin_Seqs(Re)) & (G in Fin_Seqs(Re))) •imp Cf_RR(F •F_OVER G,{x in Re | G~[x] /= R_0})
(910) Theorem 755: [Crossing-completness principle for the real numbers] ((Cf_RR(F,I(X,Y)) & (X in Re) & (Y in Re) & (R_0 •R_GE F~[X]) & (R_0 •R_LE F~[Y]) & (X •R_LE Y)) •imp (EXISTS v | ((X •R_LE V) & (V •R_LE Y) & (F~[v] = R_0))))
(911) Theorem 756: (Cf_RR(F,S) & BoundedClosedRe(S)) •imp (EXISTS u in S | (FORALL v in S | F~[u] •R_GE F~[v]))
(912) Theorem 757: (Cf_RR(F,S) & BoundedClosedRe(S)) •imp (EXISTS u in I(X,Y) | (FORALL v in S | F~[u] •R_LE F~[v]))
(913) Theorem 758: (Cf_RR(F,I(X,Y)) & (X in Re) & (Y in Re)) •imp (EXISTS u in I(X,Y), v in I(X,Y) | range(F •ON I(X,Y)) = I(f~[u],f~[v]))
(914) Theorem 759: (BoundedClosedRe(S) & (S •incin Un({OI(car(ends),cdr(ends)): ends in T})) & (FORALL ends in T | ends in (Re •PROD Re))) •imp (EXISTS T1 | (T1 •incin T) & Finite(T1) & (S •incin Un({OI(car(ends),cdr(ends)): ends in T1})))
(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)))
(919) Theorem 763a: [The square of the square root of any real w=(x •R_TIMES x) •R_PLUS (y •R_TIMES y) is w] ((X in Re) & (Y in Re)) •imp (sqrt((X •R_TIMES X) •R_PLUS (Y •R_TIMES Y)) •R_TIMES sqrt((X •R_TIMES X) •R_PLUS (Y •R_TIMES Y)) = ((X •R_TIMES X) •R_PLUS (Y •R_TIMES Y)))
(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)
(921) Theorem 20001: ((N in Re) & (M in Re)) •imp (((abs(N) •R_PLUS abs(M)) •R_GT abs(N •R_MINUS M)) or ((abs(N) •R_PLUS abs(M)) = abs(N •R_MINUS M)))
(921+) Theorem 20002: ((N in Re) & (M in Re) & (M /= R_0)) •imp (abs(N) •R_OVER abs(M) = abs(N •R_OVER M))
(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))
(923) Theorem 20004: ((X in Re) & (Y in Re) & (X1 in Re) & (X •R_GT Y) & (X1 •R_GT R_0)) •imp ((X •R_TIMES X1) •R_GT (Y •R_TIMES X1))
(924) Theorem 20005: ((X in Re) & (Y in Re) & (X •R_GT Y)) •imp (X •R_GT ((X •R_PLUS Y) •R_OVER (R_1 •R_PLUS R_1)) & (((X •R_PLUS Y) •R_OVER (R_1 •R_PLUS R_1)) •R_GT Y))
(925) Theorem 804a: ((X in Re) & (Y in Re)) •imp ([X,Y] in Cm)
(928) Theorem 805: ((N in Cm) & (M in Cm)) •imp ((N •C_PLUS M in Cm) & (N •C_TIMES M in Cm))
(929) Theorem 806: ((N in Cm) & (M in Cm)) •imp (N •C_PLUS M = M •C_PLUS N)
(930) Theorem 807: (N in Cm) •imp ((N = N •C_PLUS C_0) & (N = C_0 •C_PLUS N))
(931) Theorem 808: (N in Cm) •imp ((C_Rev(N) in Cm) & (C_Rev(C_Rev(N)) = N))
(932) Theorem 809: (N in Cm) •imp (C_Rev(N) •C_PLUS N = C_0)
(933) Theorem 810: ((N in Cm) & (M in Cm)) •imp (N = M •C_PLUS (N •C_MINUS M))
(934) Theorem 811: ((N in Cm) & (M in Cm)) •imp (N •C_TIMES M = M •C_TIMES N)
(935) Theorem 812: (N in Cm) •imp ((C_abs(N) in Re) & R_is_nonneg(C_abs(N)))
(936) Theorem 813: (N in Cm) •imp (C_abs(N) = C_abs(C_Rev(N)))
(937) Theorem 814: ((N in Cm) & (M in Cm)) •imp (((C_abs(N) •R_PLUS C_abs(M)) •R_GT C_abs(N •C_PLUS M)) or (C_abs(N) •R_PLUS C_abs(M) = C_abs(N •C_PLUS M)))
(938) Theorem 815: ((N in Cm) & (M in Cm)) •imp (((C_abs(N) •R_PLUS C_abs(M)) •R_GT C_abs(N •C_MINUS M)) or (C_abs(N) •R_PLUS C_abs(M) = C_abs(N •C_MINUS M)))
(939) Theorem 816: ((N in Cm) & (M in Cm)) •imp (C_abs(N) •R_TIMES C_abs(M) = C_abs(N •C_TIMES M))
(940) Theorem 817: ((N in Cm) & (M in Cm) & (M /= C_0)) •imp (C_abs(N) •R_OVER C_abs(M) = C_abs(N •C_OVER M))
(941) Theorem 819: ((K in Cm) & (N in Cm) & (M in Cm)) •imp (N •C_PLUS (M •C_PLUS K) = (N •C_PLUS M) •C_PLUS K)
(942) Theorem 820: ((K in Cm) & (N in Cm) & (M in Cm)) •imp ((N •C_TIMES (M •C_TIMES K)) = ((N •C_TIMES M) •C_TIMES K))
(943) Theorem 821: ((K in Cm) & (N in Cm) & (M in Cm)) •imp ((N •C_TIMES (M •C_PLUS K)) = ((N •C_TIMES M) •C_PLUS (N •C_TIMES K)))
(944) Theorem 822: (M in Cm) •imp ((M = (M •C_TIMES C_1)) & (M = (C_1 •C_TIMES M)))
(945) Theorem 823: ((M in Cm) & (M /= C_0)) •imp ((C_Recip(M) in Cm) & ((M •C_TIMES C_Recip(M)) = C_1))
(946) Theorem 824: ((N in Cm) & (M in Cm) & (M /= C_0)) •imp (N = M •C_TIMES (N •C_OVER M))
(947) Theorem real_sigma0: (FORALL f | (Finite(f) & (range(f) •incin Re)) •imp (Sig(f) in Re)) & (FORALL x | (cdr(x) in Re) •imp (Sig({x}) = cdr(x))) & (FORALL f,t | (Finite(f) & Is_map(f) & (range(f) •incin Re)) •imp (Sig(f) = (Sig(f •ON (domain(f) * t)) •R_PLUS Sig(f •ON (domain(f) - t)))))
(948) Theorem real_sigma: (Svm(F) & (range(F) •incin Re) & Finite(F)) •imp ((Sig(F) in Re) & ((P in F) •imp (Sig({P}) = (F~[car(P)]))) & (Sig(F) = (Sig(F •ON (domain(F) * A)) •R_PLUS Sig(F •ON (domain(F) - A)))))
(949) Theorem 20006: ((N in RF) & (M in RF)) •imp (N •F_PLUS M = M •F_PLUS N)
(950) Theorem 20007: ((N in RF) & (M in RF)) •imp (N •F_PLUS M = M •F_PLUS N)
(951) Theorem 20008: ((N in RF) & (M in RF)) •imp (N •F_TIMES M = M •F_TIMES N)
(952) Theorem 20009: ((K in RF) & (N in RF) & (M in RF)) •imp (N •F_PLUS (M •F_PLUS K) = (N •F_PLUS M) •F_PLUS K)
(953) Theorem 20010: ((K in RF) & (N in RF) & (M in RF)) •imp (N •F_TIMES (M •F_TIMES K) = (N •F_TIMES M) •F_TIMES K)
(954) Theorem 20011: ((K in RF) & (N in RF) & (M in RF)) •imp (N •F_TIMES (M •F_PLUS K) = (N •F_TIMES M) •F_PLUS (N •F_TIMES K))
(955) Theorem real_function_sigma: (Svm(ser) & (range(ser) •incin RF) & Finite(ser)) •imp ((FSig(ser) in RF & (p in ser) •imp (Sig({p}) = ser(car(p)))) &(FORALL a | Sig(ser) = Sig(ser •ON (domain(ser) * a)) •R_PLUS Sig(ser •ON domain(ser) - a)))
(956) Theorem 20012: [Cauchy integral theorem] is_analytic_CF(f) •imp (EXISTS eps in Re | (eps •R_GT R_0) & (FORALL crv1, crv2 | (is_CD_curv(crv1,R_0,R_1) & is_CD_curv(crv2,R_0,R_1) & ((crv1~[R_0]) = (crv1~[R_1])) & ((crv2~[R_0]) = (crv2~[R_1])) & (FORALL x in Interval(R_0,R_1) | eps •R_GE C_abs((crv1~[x]) •C_MINUS (crv2~[x])))) •imp (Line_Int(f,crv1,R_0,R_1) = Line_Int(f,crv2,R_0,R_1)) ))
(957) Theorem 20013: [Cauchy integral formula] (is_analytic_CF(f) & (domain(f) incs {w in Cm | C_abs(w) •R_GE R_1})) •imp (FORALL w in Cm | (C_abs(w) •R_GT R_1) •imp ((f~[w]) = (Line_Int({[x,(f~[x]) •C_OVER (x •C_MINUS w)]: x in (Cm -{w})}, {[x,C_exp_fcn([R_0,x])]: x in Re}, R_0, pi •R_PLUS pi) •C_OVER ([R_0,pi •R_PLUS pi])) ))