Logiweb codex of sup in pyk

Up Help

ref-3-id-28	Nat( {MissingArg} )
ref-3-id-63	meta-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-3-id-64	meta-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-3-id-65	meta-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-3-id-313	lemma plus0Left
ref-3-id-314	lemma times1Left
ref-3-id-316	lemma eqMultiplicationLeft
ref-3-id-354	lemma eqLeq(R)
ref-3-id-357	lemma =f to sameF
ref-3-id-358	lemma plusF(Sym)
ref-3-id-359	lemma timesF(Sym)
ref-3-id-433	{MissingArg} ^ {MissingArg}
ref-0-id-0	sup
ref-0-id-1	lemma to!!==
ref-0-id-2	prop lemma to negated double imply
ref-0-id-3	prop lemma to negated and(1)
ref-0-id-4	pred lemma addNegatedAll
ref-0-id-5	pred lemma (A)to(~E~)(Imply)
ref-0-id-6	pred lemma (E)to(~A~)(Imply)
ref-0-id-7	pred lemma (E~)to(~A)(Imply)
ref-0-id-8	pred lemma toNegatedAEA
ref-0-id-9	lemma uniqueNegative
ref-0-id-10	lemma doubleMinus
ref-0-id-11	lemma minusNegated
ref-0-id-12	lemma eqReflexivity
ref-0-id-13	lemma eqSymmetry
ref-0-id-14	lemma eqTransitivity
ref-0-id-15	lemma eqTransitivity4
ref-0-id-16	lemma eqTransitivity5
ref-0-id-17	lemma eqTransitivity6
ref-0-id-18	lemma addEquations
ref-0-id-19	lemma subtractEquations
ref-0-id-20	lemma subtractEquationsLeft
ref-0-id-21	lemma multiplyEquations
ref-0-id-22	lemma eqNegated
ref-0-id-23	lemma positiveToRight(Eq)
ref-0-id-24	lemma positiveToLeft(Eq)
ref-0-id-25	lemma positiveToLeft(Eq)(1 term)
ref-0-id-26	lemma negativeToLeft(Eq)
ref-0-id-27	lemma nonreciprocalToRight(Eq)(1 term)
ref-0-id-28	lemma distributionOut(Minus)
ref-0-id-29	lemma positiveToRight(Eq)(1 term)
ref-0-id-30	lemma sameSeries(NumDiff)
ref-0-id-31	lemma plusAssociativity(4 terms)
ref-0-id-32	lemma lessNeq
ref-0-id-33	lemma neqSymmetry
ref-0-id-34	lemma neqNegated
ref-0-id-35	lemma subNeqRight
ref-0-id-36	lemma subNeqLeft
ref-0-id-37	lemma negativeToRight(Neq)(1 term)
ref-0-id-38	lemma neqAddition
ref-0-id-39	lemma neqMultiplication
ref-0-id-40	lemma nonzeroProduct(2)
ref-0-id-41	lemma switchTerms(x<=y-z)
ref-0-id-42	lemma negativeToLeft(Less)(1 term)
ref-0-id-43	lemma +1IsPositive(N)
ref-0-id-44	lemma (1/2)(x+y)-x=(1/2)(y-x)
ref-0-id-45	lemma y-(1/2)(x+y)=(1/2)(y-x)
ref-0-id-46	lemma expZero exact
ref-0-id-47	lemma sameExp base
ref-0-id-48	lemma sameExp indu
ref-0-id-49	lemma sameExp
ref-0-id-50	lemma exp(+1)
ref-0-id-51	lemma positiveBase base
ref-0-id-52	lemma positiveBase indu
ref-0-id-53	lemma positiveBase
ref-0-id-54	lemma base(1/2)Sum zero exact
ref-0-id-55	lemma sameBase(1/2)Sum second base
ref-0-id-56	lemma sameBase(1/2)Sum second indu
ref-0-id-57	lemma sameBase(1/2)Sum second
ref-0-id-58	lemma base(1/2)Sum(+1)
ref-0-id-59	lemma base(1/2)Sum exact bound base
ref-0-id-60	lemma base(1/2)Sum exact bound indu
ref-0-id-61	lemma base(1/2)Sum exact bound
ref-0-id-62	lemma base(1/2)Sum bound
ref-0-id-63	lemma UStelescope zero exact
ref-0-id-64	lemma sameTelescope second base
ref-0-id-65	lemma sameTelescope second indu
ref-0-id-66	lemma sameTelescope second
ref-0-id-67	lemma UStelescope(+1)
ref-0-id-68	lemma telescopeNumerical base
ref-0-id-69	lemma telescopeNumerical indu
ref-0-id-70	lemma telescopeNumerical
ref-0-id-71	lemma telescopeBound base
ref-0-id-72	lemma telescopeBound indu
ref-0-id-73	lemma telescopeBound
ref-0-id-74	lemma lessNeq(F) helper
ref-0-id-75	lemma lessNeq(F)
ref-0-id-76	lemma lessNeq(R)
ref-0-id-77	lemma intervalSize base
ref-0-id-78	lemma intervalSize indu
ref-0-id-79	lemma intervalSize
ref-0-id-80	lemma XSlessUS
ref-0-id-81	lemma USdecreasing(+1)
ref-0-id-82	lemma closeUS
ref-0-id-83	lemma closeUS(n+1)
ref-0-id-84	pred lemma allNegated(Imply)
ref-0-id-85	pred lemma existNegated(Imply)
ref-0-id-86	pred lemma intro exist helper
ref-0-id-87	pred lemma intro exist
ref-0-id-88	pred lemma exist mp
ref-0-id-89	pred lemma exist mp2
ref-0-id-90	pred lemma 2exist mp
ref-0-id-91	pred lemma 2exist mp2
ref-0-id-92	pred lemma EAE mp
ref-0-id-93	pred lemma addAll
ref-0-id-94	pred lemma addExist helper1
ref-0-id-95	pred lemma addExist helper2
ref-0-id-96	pred lemma addExist
ref-0-id-97	pred lemma addExist(SimpleAnt)
ref-0-id-98	pred lemma addExist(Simple)
ref-0-id-99	pred lemma addEAE
ref-0-id-100	pred lemma AEAnegated
ref-0-id-101	pred lemma EEAnegated
ref-0-id-102	lemma induction
ref-0-id-103	lemma leqAntisymmetry
ref-0-id-104	lemma leqTransitivity
ref-0-id-105	lemma leqAddition
ref-0-id-106	lemma leqMultiplication
ref-0-id-107	lemma reciprocal
ref-0-id-108	lemma equality
ref-0-id-109	lemma eqLeq
ref-0-id-110	lemma eqAddition
ref-0-id-111	lemma eqMultiplication
ref-0-id-112	lemma leqMultiplicationLeft
ref-0-id-113	lemma leqLessEq
ref-0-id-114	lemma lessLeq
ref-0-id-115	lemma from leqGeq
ref-0-id-116	lemma subLeqRight
ref-0-id-117	lemma subLeqLeft
ref-0-id-118	lemma leqPlus1
ref-0-id-119	lemma positiveToRight(Leq)
ref-0-id-120	lemma positiveToRight(Leq)(1 term)
ref-0-id-121	lemma negativeToRight(Leq)
ref-0-id-122	lemma positiveToLeft(Leq)
ref-0-id-123	lemma negativeToLeft(Leq)
ref-0-id-124	lemma negativeToLeft(Leq)(1 term)
ref-0-id-125	lemma leqAdditionLeft
ref-0-id-126	lemma leqSubtraction
ref-0-id-127	lemma leqSubtractionLeft
ref-0-id-128	lemma thirdGeq
ref-0-id-129	lemma leqNegated
ref-0-id-130	lemma addEquations(Leq)
ref-0-id-131	lemma multiplyEquations(Leq)
ref-0-id-132	lemma thirdGeqSeries
ref-0-id-133	lemma leqNeqLess
ref-0-id-134	lemma fromLess
ref-0-id-135	lemma toLess
ref-0-id-136	lemma fromNotLess
ref-0-id-137	lemma toNotLess
ref-0-id-138	lemma negativeLessPositive
ref-0-id-139	lemma leqLessTransitivity
ref-0-id-140	lemma lessLeqTransitivity
ref-0-id-141	lemma lessTransitivity
ref-0-id-142	lemma lessTotality
ref-0-id-143	lemma subLessRight
ref-0-id-144	lemma subLessLeft
ref-0-id-145	lemma switchTerms(x
ref-0-id-146	lemma switchTerms(x-y
ref-0-id-147	lemma lessAddition
ref-0-id-148	lemma lessAdditionLeft
ref-0-id-149	lemma lessMultiplication
ref-0-id-150	lemma lessMultiplicationLeft
ref-0-id-151	lemma lessDivision
ref-0-id-152	lemma positiveToRight(Less)
ref-0-id-153	lemma positiveToLeft(Less)
ref-0-id-154	lemma negativeToLeft(Less)
ref-0-id-155	lemma negativeToRight(Less)
ref-0-id-156	lemma addEquations(Less)
ref-0-id-157	lemma addEquations(LeqLess)
ref-0-id-158	lemma reciprocalToLeft(Less)
ref-0-id-159	lemma lessNegated
ref-0-id-160	lemma positiveNonzero
ref-0-id-161	lemma positiveNegated
ref-0-id-162	lemma nonpositiveNegated
ref-0-id-163	lemma negativeNegated
ref-0-id-164	lemma nonnegativeNegated
ref-0-id-165	lemma positiveHalved
ref-0-id-166	lemma positiveInverted
ref-0-id-167	lemma nonnegativeNumerical
ref-0-id-168	lemma negativeNumerical
ref-0-id-169	lemma positiveNumerical
ref-0-id-170	lemma nonpositiveNumerical
ref-0-id-171	lemma |0|=0
ref-0-id-172	lemma 0<=|x|
ref-0-id-173	lemma x<=|x|
ref-0-id-174	lemma fromPositiveNumerical
ref-0-id-175	lemma sameNumerical
ref-0-id-176	lemma signNumerical(+)
ref-0-id-177	lemma signNumerical
ref-0-id-178	lemma toNumericalLess
ref-0-id-179	lemma fromNumericalGreater
ref-0-id-180	lemma numericalDifference
ref-0-id-181	lemma numericalDifferenceLess helper
ref-0-id-182	lemma numericalDifferenceLess
ref-0-id-183	lemma splitNumericalSumHelper
ref-0-id-184	lemma splitNumericalSum(++)
ref-0-id-185	lemma splitNumericalSum(--)
ref-0-id-186	lemma splitNumericalSum(+-, smallNegative)
ref-0-id-187	lemma splitNumericalSum(+-, bigNegative)
ref-0-id-188	lemma splitNumericalSum(+-)
ref-0-id-189	lemma splitNumericalSum(-+)
ref-0-id-190	lemma splitNumericalSum
ref-0-id-191	lemma splitNumericalProduct(++)
ref-0-id-192	lemma splitNumericalProduct(+-)
ref-0-id-193	lemma splitNumericalProduct
ref-0-id-194	lemma insertMiddleTerm(Numerical)
ref-0-id-195	lemma insertTwoMiddleTerms(Numerical)
ref-0-id-196	lemma three2twoTerms
ref-0-id-197	lemma three2threeTerms
ref-0-id-198	lemma three2twoFactors
ref-0-id-199	lemma three2threeFactors
ref-0-id-200	lemma times(-1)
ref-0-id-201	lemma times(-1)Left
ref-0-id-202	lemma leqMax1
ref-0-id-203	lemma leqMax2
ref-0-id-204	lemma lessThanMax
ref-0-id-205	lemma x+y=zBackwards
ref-0-id-206	lemma x*y=zBackwards
ref-0-id-207	lemma x=x+(y-y)
ref-0-id-208	lemma x=x+y-y
ref-0-id-209	lemma x=x*y*(1/y)
ref-0-id-210	lemma insertMiddleTerm(Sum)
ref-0-id-211	lemma insertTwoMiddleTerms(Sum)
ref-0-id-212	lemma insertMiddleTerm(Difference)
ref-0-id-213	lemma x*0+x=x
ref-0-id-214	lemma x*0=0
ref-0-id-215	lemma nonnegativeFactors
ref-0-id-216	lemma nonzeroFactors
ref-0-id-217	lemma positiveFactors
ref-0-id-218	lemma plusTimesMinus
ref-0-id-219	lemma minusTimesMinus
ref-0-id-220	lemma (-1)*(-1)+(-1)*1=0
ref-0-id-221	lemma (-1)*(-1)=1
ref-0-id-222	lemma 0<1Helper
ref-0-id-223	lemma 0<1
ref-0-id-224	lemma 0<2
ref-0-id-225	lemma 0<3
ref-0-id-226	lemma 0<1/2
ref-0-id-227	lemma 0<1/3
ref-0-id-228	lemma x+x=2*x
ref-0-id-229	lemma x+x+x=3*x
ref-0-id-230	lemma (1/2)x+(1/2)x=x
ref-0-id-231	lemma (1/3)x+(1/3)x+(1/3)x=x
ref-0-id-232	lemma -x-y=-(x+y)
ref-0-id-233	lemma -x*y=-(x*y)
ref-0-id-234	lemma -0=0
ref-0-id-235	lemma sameFsymmetry
ref-0-id-236	lemma sameFtransitivity
ref-0-id-237	lemma f2R(Plus)
ref-0-id-238	lemma f2R(Times)
ref-0-id-239	lemma <
ref-0-id-240	lemma <
ref-0-id-241	lemma <<==Reflexivity
ref-0-id-242	lemma <<==AntisymmetryHelper(Q)
ref-0-id-243	lemma fromNot
ref-0-id-244	lemma fromNot
ref-0-id-245	lemma fromNot
ref-0-id-246	lemma fromNot
ref-0-id-247	lemma fromNot
ref-0-id-248	lemma fromNotSameF(Strongest) helper2
ref-0-id-249	lemma fromNotSameF(Strongest) helper
ref-0-id-250	lemma fromNotSameF(Strongest)
ref-0-id-251	lemma toLess(F) helper
ref-0-id-252	lemma toLess(F)
ref-0-id-253	lemma fromNot<<
ref-0-id-254	lemma toLess(R)
ref-0-id-255	lemma leqTotality(R)
ref-0-id-256	lemma fromNotSameF(Weak)(Helper)
ref-0-id-257	lemma fromNotSameF(Weak)
ref-0-id-258	lemma fromNotLess(F)
ref-0-id-259	lemma ==Addition
ref-0-id-260	lemma ==AdditionLeft
ref-0-id-261	lemma fpart-Bounded base
ref-0-id-262	lemma fpart-Bounded indu helper
ref-0-id-263	lemma fpart-Bounded indu
ref-0-id-264	lemma fpart-Bounded
ref-0-id-265	lemma f-Bounded helper
ref-0-id-266	lemma f-Bounded
ref-0-id-267	lemma sameFmultiplication helper
ref-0-id-268	lemma sameFmultiplication
ref-0-id-269	lemma eqMultiplication(R)
ref-0-id-270	lemma eqMultiplicationLeft(R)
ref-0-id-271	lemma x*0=0(F)
ref-0-id-272	lemma x*0=0(R)
ref-0-id-273	lemma lessMultiplication(F) helper2
ref-0-id-274	lemma lessMultiplication(F) helper
ref-0-id-275	lemma lessMultiplication(F)
ref-0-id-276	lemma lessMultiplication(R)
ref-0-id-277	lemma leqMultiplication(R)
ref-0-id-278	lemma plusAssociativity(F)
ref-0-id-279	lemma plus0(F)
ref-0-id-280	lemma plusCommutativity(F)
ref-0-id-281	lemma timesAssociativity(F)
ref-0-id-282	lemma times1f
ref-0-id-283	lemma 2cauchy helper
ref-0-id-284	lemma 2cauchy
ref-0-id-285	lemma reciprocalF nonzero
ref-0-id-286	lemma reciprocalFny nonzero
ref-0-id-287	lemma eventually=f to sameF helper
ref-0-id-288	lemma eventually=f to sameF
ref-0-id-289	lemma fromNotSameF(Strong) helper2
ref-0-id-290	lemma fromNotSameF(Strong) helper
ref-0-id-291	lemma fromNotSameF(Strong)
ref-0-id-292	lemma sameFreciprocal helper
ref-0-id-293	lemma sameFreciprocal
ref-0-id-294	lemma from!!==
ref-0-id-295	lemma reciprocal(R)
ref-0-id-296	lemma timesCommutativity(F)
ref-0-id-297	lemma distribution(F)
ref-0-id-298	lemma fromMax(1)
ref-0-id-299	lemma fromMax(2)
ref-0-id-300	prop lemma to negated and
ref-0-id-301	lemma positiveToRight(Less)(1 term)
ref-0-id-302	pred lemma (A~)to(~E)
ref-0-id-303	lemma ==Transitivity4
ref-0-id-304	lemma plus0Left(R)
ref-0-id-305	lemma x=x+(y-y)(R)
ref-0-id-306	lemma x=x+y-y(R)
ref-0-id-307	lemma positiveToRight(Eq)(R)
ref-0-id-308	lemma subtractEquations(R)
ref-0-id-309	lemma neqAddition(R)
ref-0-id-310	lemma eqAdditionLeft(R)
ref-0-id-311	lemma three2twoTerms(R)
ref-0-id-312	lemma positiveToRight(Less)(R)
ref-0-id-313	lemma three2threeTerms(R)
ref-0-id-314	lemma positiveToRight(Less)(1 term)(R)
ref-0-id-315	lemma toLeq(Advanced)(R)
ref-0-id-316	lemma leqNeqLess(R)
ref-0-id-317	lemma subLeqLeft(R)
ref-0-id-318	lemma leqLessTransitivity(R)
ref-0-id-319	lemma negativeToLeft(Eq)(R)
ref-0-id-320	lemma negativeToRight(Less)(R)
ref-0-id-321	lemma !!==Symmetry
ref-0-id-322	lemma negativeToRight(Eq)(R)
ref-0-id-323	lemma negativeToRight(Eq)(1 term)(R)
ref-0-id-324	lemma doubleMinus(R)
ref-0-id-325	lemma uniqueNegative(R)
ref-0-id-326	lemma subtractEquationsLeft(R)
ref-0-id-327	lemma eqNegated(R)
ref-0-id-328	lemma neqNegated(R)
ref-0-id-329	lemma leqNegated(R)
ref-0-id-330	lemma lessNegated(R)
ref-0-id-331	lemma -0=0(R)
ref-0-id-332	lemma negativeNegated(R)
ref-0-id-333	lemma from leqGeq(R)
ref-0-id-334	lemma subLeqRight(R)
ref-0-id-335	lemma fromLess(R)
ref-0-id-336	lemma nonnegativeNumerical(R)
ref-0-id-337	lemma negativeNumerical(R)
ref-0-id-338	lemma 0<=|x|(R)
ref-0-id-339	lemma positiveNegated(R)
ref-0-id-340	lemma addEquations(R)
ref-0-id-341	lemma distributionOut(R)
ref-0-id-342	lemma ==Transitivity5
ref-0-id-343	lemma x*0+x=x(R)
ref-0-id-344	lemma x*0=0(R)fff
ref-0-id-345	lemma times(-1)(R)
ref-0-id-346	lemma times(-1)Left(R)
ref-0-id-347	lemma -x-y=-(x+y)(R)
ref-0-id-348	lemma lessTotality(R)
ref-0-id-349	lemma positiveNumerical(R)
ref-0-id-350	lemma signNumerical(+)(R)
ref-0-id-351	lemma sameNumerical(R)
ref-0-id-352	lemma minusNegated(R)
ref-0-id-353	lemma signNumerical(R)
ref-0-id-354	lemma numericalDifference(R)
ref-0-id-355	lemma x<=|x|(R)
ref-0-id-356	lemma USlimitIsUpperBound helper
ref-0-id-357	lemma USlimitIsUpperBound
ref-0-id-358	lemma (-1)*(-1)+(-1)*1=0(R)
ref-0-id-359	lemma (-1)*(-1)=1(R)
ref-0-id-360	lemma 0<1Helper(R)
ref-0-id-361	lemma 0<1(R)
ref-0-id-362	lemma expZero exact(R)
ref-0-id-363	lemma positiveBase(R) base
ref-0-id-364	lemma three2twoFactors(R)
ref-0-id-365	lemma x=x*y*(1/y)(R)
ref-0-id-366	lemma neqMultiplication(R)
ref-0-id-367	lemma lessTransitivity(R)
ref-0-id-368	lemma 0<2(R)
ref-0-id-369	lemma sameExp(R) base
ref-0-id-370	lemma sameExp(R) indu
ref-0-id-371	lemma sameExp(R)
ref-0-id-372	lemma subNeqLeft(R)
ref-0-id-373	lemma subNeqRight(R)
ref-0-id-374	lemma nonzeroFactors(R)
ref-0-id-375	lemma nonnegativeFactors(R)
ref-0-id-376	lemma positiveFactors(R)
ref-0-id-377	lemma lessDivision(R)
ref-0-id-378	lemma 0<1/2(R)
ref-0-id-379	lemma positiveToRight(Eq)(1 term)(R)
ref-0-id-380	lemma exp(+1)(R)
ref-0-id-381	lemma positiveBase(R) indu
ref-0-id-382	lemma positiveBase(R)
ref-0-id-383	lemma -x*y=-(x*y)(R)
ref-0-id-384	lemma positiveToLeft(Eq)(R)
ref-0-id-385	lemma times1Left(R)
ref-0-id-386	lemma ==Transitivity6
ref-0-id-387	lemma x+x=2*x(R)
ref-0-id-388	lemma (1/2)x+(1/2)x=x(R)
ref-0-id-389	lemma distributionOut(Minus)(R)
ref-0-id-390	lemma (1/2)(x+y)-x=(1/2)(y-x)(R)
ref-0-id-391	lemma intervalSize(R) base
ref-0-id-392	lemma lessMultiplicationLeft(R)
ref-0-id-393	lemma negativeToLeft(Less)(R)
ref-0-id-394	lemma negativeToLeft(Less)(1 term)(R)
ref-0-id-395	lemma y-(1/2)(x+y)=(1/2)(y-x)(R)
ref-0-id-396	lemma intervalSize(R) indu
ref-0-id-397	lemma intervalSize(R)
ref-0-id-398	lemma XSlessUS(R)
ref-0-id-399	lemma USdecreasing(+1)(R)
ref-0-id-400	lemma expUnbounded base
ref-0-id-401	lemma expUnbounded indu
ref-0-id-402	lemma expUnbounded
ref-0-id-403	lemma 1<=x+1(N)
ref-0-id-404	lemma nonzeroProduct(2)(R)
ref-0-id-405	lemma positiveNonzero(R)
ref-0-id-406	lemma nonreciprocalToRight(Eq)(1 term)(R)
ref-0-id-407	lemma expNonzero base
ref-0-id-408	lemma expNonzero indu
ref-0-id-409	lemma expNonzero
ref-0-id-410	lemma expNonzero(2)
ref-0-id-411	lemma multiplyEquations(R)
ref-0-id-412	lemma halfBase base
ref-0-id-413	lemma halfBase indu
ref-0-id-414	lemma halfBase
ref-0-id-415	lemma three2threeFactors(R)
ref-0-id-416	lemma x*y=zBackwards(R)
ref-0-id-417	lemma positiveInverted(R)
ref-0-id-418	lemma reciprocalToRight(Less)(R)
ref-0-id-419	lemma reciprocalToRight(Less)(1 term)(R)
ref-0-id-420	lemma nonreciprocalToLeft(Less)(R)
ref-0-id-421	lemma 1
ref-0-id-422	lemma switchFactors(1/x
ref-0-id-423	lemma smallHalving
ref-0-id-424	lemma intervalSize(anyPositive)
ref-0-id-425	lemma USdecreasing(+n) base
ref-0-id-426	lemma USdecreasing(+n) indu
ref-0-id-427	lemma USdecreasing(+n)
ref-0-id-428	lemma USdecreasing
ref-0-id-429	lemma leqAdditionLeft(R)
ref-0-id-430	lemma toNotLess(R)
ref-0-id-431	lemma limitOfUSIsLeq
ref-0-id-432	lemma subtractEquations(Less)(R)
ref-0-id-433	lemma subtractEquationsLeft(Less)(R)
ref-0-id-434	lemma lessNegated(Negative)(R)
ref-0-id-435	prop lemma from negated and (imply)
ref-0-id-436	prop lemma remove double neg (consequent)
ref-0-id-437	lemma fromNotUpperBound
ref-0-id-438	lemma distributionOut
ref-0-id-439	lemma distributionOutLeft
ref-0-id-440	lemma distributionLeft
ref-0-id-441	lemma leqNUB
ref-0-id-442	lemma USlimitIsLeastUpperBound helper
ref-0-id-443	lemma USlimitIsLeastUpperBound
ref-0-id-444	lemma fromNotLess(R)
ref-0-id-445	pred lemma exist mp3
ref-0-id-446	lemma greaterPositive(N)
ref-0-id-447	lemma ysFClose helper
ref-0-id-448	lemma ysFClose
ref-0-id-449	lemma ysFCauchy helper
ref-0-id-450	lemma ysFCauchy
ref-0-id-451	lemma cartProdIsRelation
ref-0-id-452	lemma fromSubset
ref-0-id-453	lemma subsetIsRelation
ref-0-id-454	lemma toSeries
ref-0-id-455	lemma fromSeries
ref-0-id-456	lemma seriesSubsetCP
ref-0-id-457	lemma valueType
ref-0-id-458	prop lemma remove or
ref-0-id-459	lemma fromSingleton
ref-0-id-460	lemma inPair(1)
ref-0-id-461	lemma inPair(2)
ref-0-id-462	lemma sameMember(2)
ref-0-id-463	lemma toBinaryUnion(1)
ref-0-id-464	lemma toBinaryUnion(2)
ref-0-id-465	lemma fromOrderedPair(twoLevels)
ref-0-id-466	lemma toCartProd helper
ref-0-id-467	lemma toCartProd
ref-0-id-468	lemma nonreciprocalToRight(Eq)
ref-0-id-469	lemma nonreciprocalToLeft(Eq)(1 term)
ref-0-id-470	lemma sameReciprocal
ref-0-id-471	lemma CPseparationIsRelation
ref-0-id-472	lemma orderedPairEquality
ref-0-id-473	lemma reciprocalIsFunction
ref-0-id-474	lemma reciprocalIsTotal
ref-0-id-475	lemma reciprocalIsRationalSeries
ref-0-id-476	lemma crsIsRelation
ref-0-id-477	lemma crsIsFunction
ref-0-id-478	lemma crsIsTotal
ref-0-id-479	lemma crsIsSeries
ref-0-id-480	lemma crsLookup
ref-0-id-481	lemma 0f
ref-0-id-482	lemma 1f
ref-0-id-483	lemma toSingleton
ref-0-id-484	lemma fromSameSingleton
ref-0-id-485	lemma singletonmembersEqual
ref-0-id-486	lemma unequalsNotInSingleton
ref-0-id-487	lemma nonsingletonmembersUnequal
ref-0-id-488	lemma fromOrderedPair
ref-0-id-489	lemma fromOrderedPair(1)
ref-0-id-490	lemma fromOrderedPair(2)
ref-0-id-491	lemma fromCartProd
ref-0-id-492	lemma fromCartProd(1)
ref-0-id-493	lemma fromCartProd(2)
ref-0-id-494	lemma sameOrderedPair
ref-0-id-495	lemma inSeries helper
ref-0-id-496	lemma inSeries
ref-0-id-497	lemma to=f subset helper
ref-0-id-498	lemma to=f subset
ref-0-id-499	lemma to=f
ref-0-id-500	lemma productIsFunction
ref-0-id-501	lemma productIsTotal
ref-0-id-502	lemma productIsRationalSeries
ref-0-id-503	lemma timesF
ref-0-id-504	lemma -x+(1/2)x=-(1/2)x
ref-0-id-505	lemma positiveTripled
ref-0-id-506	lemma positiveDividedBy3
ref-0-id-507	lemma |x-x|=0
ref-0-id-508	lemma 1<2
ref-0-id-509	lemma 1/3<2/3
ref-0-id-510	lemma (1/3)x+(1/3)x=(2/3)x
ref-0-id-511	lemma (2/3)x+(1/3)x=x
ref-0-id-512	lemma -x+(2/3)x=-(1/3)x
ref-0-id-513	lemma -(1/3)x-(1/3)x=-(2/3)x
ref-0-id-514	lemma -x+(1/3)x=-(2/3)x
ref-0-id-515	lemma preserveLessGreater
ref-0-id-516	lemma closetolessIsLess
ref-0-id-517	lemma subLessLeft(F)
ref-0-id-518	lemma subLessLeft(R)
ref-0-id-519	lemma closetogreaterIsGreater
ref-0-id-520	lemma subLessRight(F)
ref-0-id-521	lemma subLessRight(R)
ref-0-id-522	tester1
ref-0-id-523	tester2
ref-0-id-524	tester3
ref-0-id-525	tester4
ref-0-id-526	tester5
ref-0-id-527	tester6