List of theorems referencing the symbol TILDE_

(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))
(95) Theorem fcn_symbol.2a: [Image by a mapformer, quantified form] (FORALL x in s | g~[x] = f(x))
(96) Theorem fcn_symbol.3: [Elements not in a mapformer domain] (XX notin s) •imp (g~[XX] = 0)
(97) Theorem fcn_symbol.4: [Mapformer image in general] g~[XX] = if XX in s then f(XX) else 0 end if
(98) Theorem fcn_symbol.4a: [Image by a mapformer, quantified form] (FORALL x | g~[x] = if x in s then f(x) else 0 end if)
(102) Theorem 72: [Form of a single-valued map] Svm(F) •eq (F = {[x,F~[x]]: x in domain(F)})
(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))
(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)))
(123) Theorem 91: [Singletons as maps] Svm({[X,Y]}) & one_1_map({[X,Y]}) & (({[X,Y]}~[X]) = Y)
(124) Theorem 92: [Doubletons as maps] (X /= Z) •imp ({[X,Y],[Z,W]}~[X] = Y)
(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)))
(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))))
(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)
(159) Theorem 120: [Value of a restriction map] (F •ON S)~[X] = if X in domain(F •ON S) then F~[X] else 0 end if
(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)
(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])
(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))))
(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)))
(176) Theorem 137: [Image of Cartesian product by a singleton] (U in Z) •imp (((Z •PROD {V})~[U]) = V)
(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]})
(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))
(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))
(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))
(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])))
(386) Theorem subseq.2: {i in domain(h_thryvar) | i •nincin (h_thryvar~[i])} = 0
(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]))))))
(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)))
(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)}))
(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)))))
(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))))))
(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))))))
(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)))
(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)
(670) Theorem pointwiseU.1: h = {[u,uop(fp~[u])]: u in d}
(672) Theorem pointwiseU.3: (FORALL x in d | h~[x] = uop(fp~[x]))
(673) Theorem pointwise.1: h = {[u,bop(fq~[u],fp~[u])]: u in d}
(674+) Theorem pointwise.3: (FORALL x in d | h~[x] = bop(fq~[x],fp~[x]))
(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))
(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])))) ))
(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])))))
(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)))
(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]))))
(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)
(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}) )
(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)})))
(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)]))
(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})
(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]))
(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)))))
(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])) ))