Logiweb codex of sup2 in pyk

Up Help

ref-0-id-0	sup2
ref-0-id-1	lemma leqTotality(R)
ref-0-id-2	lemma positiveToLeft(Eq)
ref-0-id-3	lemma expZero exact
ref-0-id-4	lemma sameExp base
ref-0-id-5	lemma sameExp indu
ref-0-id-6	lemma sameExp
ref-0-id-7	lemma (1/2)(x+y)-x=(1/2)(y-x)
ref-0-id-8	lemma y-(1/2)(x+y)=(1/2)(y-x)
ref-0-id-9	lemma base(1/2)Sum zero exact
ref-0-id-10	lemma sameBase(1/2)Sum second base
ref-0-id-11	lemma sameBase(1/2)Sum second indu
ref-0-id-12	lemma sameBase(1/2)Sum second
ref-0-id-13	lemma negativeToLeft(Less)(1 term)
ref-0-id-14	lemma base(1/2)Sum(+1)
ref-0-id-15	lemma base(1/2)Sum exact bound base
ref-0-id-16	lemma base(1/2)Sum exact bound indu
ref-0-id-17	lemma base(1/2)Sum exact bound
ref-0-id-18	lemma base(1/2)Sum bound
ref-0-id-19	lemma UStelescope zero exact
ref-0-id-20	lemma sameTelescope second base
ref-0-id-21	lemma sameTelescope second indu
ref-0-id-22	lemma sameTelescope second
ref-0-id-23	lemma exp(+1)
ref-0-id-24	lemma positiveBase base
ref-0-id-25	lemma positiveBase indu
ref-0-id-26	lemma positiveBase
ref-0-id-27	lemma telescopeNumerical base
ref-0-id-28	lemma telescopeNumerical indu
ref-0-id-29	lemma telescopeNumerical
ref-0-id-30	lemma +1IsPositive(N)
ref-0-id-31	lemma distributionOut(Minus)
ref-0-id-32	lemma positiveToRight(Eq)(1 term)
ref-0-id-33	lemma sameSeries(NumDiff)
ref-0-id-34	prop lemma to negated double imply
ref-0-id-35	pred lemma addNegatedAll
ref-0-id-36	pred lemma (A)to(~E~)(Imply)
ref-0-id-37	pred lemma (E)to(~A~)(Imply)
ref-0-id-38	pred lemma (E~)to(~A)(Imply)
ref-0-id-39	pred lemma toNegatedAEA
ref-0-id-40	lemma three2threeTerms(R)
ref-0-id-41	lemma lessNeq(F) helper
ref-0-id-42	lemma lessNeq(F)
ref-0-id-43	lemma lessNeq(R)
ref-0-id-44	lemma x=x+(y-y)(R)
ref-0-id-45	lemma x=x+y-y(R)
ref-0-id-46	lemma subtractEquations(R)
ref-0-id-47	lemma neqAddition(R)
ref-0-id-48	lemma positiveToRight(Less)(R)
ref-0-id-49	lemma positiveToRight(Less)(1 term)(R)
ref-0-id-50	lemma leqNeqLess(R)
ref-0-id-51	lemma subLeqLeft(R)
ref-0-id-52	lemma toLeq(Advanced)(R)
ref-0-id-53	lemma leqLessTransitivity(R)
ref-0-id-54	lemma negativeToLeft(Eq)(R)
ref-0-id-55	lemma negativeToRight(Less)(R)
ref-0-id-56	lemma !!==Symmetry
ref-0-id-57	lemma switchTerms(x<=y-z)
ref-0-id-58	lemma plus0Left(R)
ref-0-id-59	lemma positiveToRight(Eq)(R)
ref-0-id-60	lemma eqAdditionLeft(R)
ref-0-id-61	lemma three2twoTerms(R)
ref-0-id-62	lemma to!!==
ref-0-id-63	lemma positiveToRight(Less)(1 term)
ref-0-id-64	pred lemma (A~)to(~E)
ref-0-id-65	lemma negativeToRight(Eq)(R)
ref-0-id-66	lemma negativeToRight(Eq)(1 term)(R)
ref-0-id-67	lemma doubleMinus(R)
ref-0-id-68	lemma uniqueNegative(R)
ref-0-id-69	lemma subtractEquationsLeft(R)
ref-0-id-70	lemma eqNegated(R)
ref-0-id-71	lemma neqNegated(R)
ref-0-id-72	lemma -0=0(R)
ref-0-id-73	lemma negativeNegated(R)
ref-0-id-74	lemma from leqGeq(R)
ref-0-id-75	lemma 0<=|x|(R)
ref-0-id-76	lemma positiveNegated(R)
ref-0-id-77	lemma addEquations(R)
ref-0-id-78	lemma times(-1)(R)
ref-0-id-79	lemma times(-1)Left(R)
ref-0-id-80	lemma -x-y=-(x+y)(R)
ref-0-id-81	lemma lessTotality(R)
ref-0-id-82	lemma sameNumerical(R)
ref-0-id-83	lemma minusNegated(R)
ref-0-id-84	lemma positiveNumerical(R)
ref-0-id-85	lemma signNumerical(+)(R)
ref-0-id-86	lemma nonnegativeNumerical(R)
ref-0-id-87	lemma negativeNumerical(R)
ref-0-id-88	lemma leqNegated(R)
ref-0-id-89	lemma lessNegated(R)
ref-0-id-90	lemma subLeqRight(R)
ref-0-id-91	lemma fromLess(R)
ref-0-id-92	lemma distributionOut(R)
ref-0-id-93	lemma x*0+x=x(R)
ref-0-id-94	lemma x*0=0(R)fff
ref-0-id-95	lemma signNumerical(R)
ref-0-id-96	lemma numericalDifference(R)
ref-0-id-97	lemma x<=|x|(R)
ref-0-id-98	lemma USlimitIsUpperBound helper
ref-0-id-99	lemma USlimitIsUpperBound
ref-0-id-100	lemma (-1)*(-1)+(-1)*1=0(R)
ref-0-id-101	lemma (-1)*(-1)=1(R)
ref-0-id-102	lemma 0<1Helper(R)
ref-0-id-103	lemma 0<1(R)
ref-0-id-104	lemma expZero exact(R)
ref-0-id-105	lemma positiveBase(R) base
ref-0-id-106	lemma three2twoFactors(R)
ref-0-id-107	lemma x=x*y*(1/y)(R)
ref-0-id-108	lemma neqMultiplication(R)
ref-0-id-109	lemma lessTransitivity(R)
ref-0-id-110	lemma 0<2(R)
ref-0-id-111	lemma sameExp(R) base
ref-0-id-112	lemma sameExp(R) indu
ref-0-id-113	lemma sameExp(R)
ref-0-id-114	lemma subNeqLeft(R)
ref-0-id-115	lemma subNeqRight(R)
ref-0-id-116	lemma nonzeroFactors(R)
ref-0-id-117	lemma nonnegativeFactors(R)
ref-0-id-118	lemma positiveFactors(R)
ref-0-id-119	lemma lessDivision(R)
ref-0-id-120	lemma 0<1/2(R)
ref-0-id-121	lemma positiveToRight(Eq)(1 term)(R)
ref-0-id-122	lemma exp(+1)(R)
ref-0-id-123	lemma positiveBase(R) indu
ref-0-id-124	lemma positiveBase(R)
ref-0-id-125	lemma -x*y=-(x*y)(R)
ref-0-id-126	lemma positiveToLeft(Eq)(R)
ref-0-id-127	lemma times1Left(R)
ref-0-id-128	lemma x+x=2*x(R)
ref-0-id-129	lemma (1/2)x+(1/2)x=x(R)
ref-0-id-130	lemma distributionOut(Minus)(R)
ref-0-id-131	lemma (1/2)(x+y)-x=(1/2)(y-x)(R)
ref-0-id-132	lemma intervalSize(R) base
ref-0-id-133	lemma lessMultiplicationLeft(R)
ref-0-id-134	lemma negativeToLeft(Less)(R)
ref-0-id-135	lemma negativeToLeft(Less)(1 term)(R)
ref-0-id-136	lemma y-(1/2)(x+y)=(1/2)(y-x)(R)
ref-0-id-137	lemma intervalSize(R) indu
ref-0-id-138	lemma intervalSize(R)
ref-0-id-139	lemma XSlessUS(R)
ref-0-id-140	lemma USdecreasing(+1)(R)
ref-0-id-141	lemma expUnbounded base
ref-0-id-142	lemma expUnbounded indu
ref-0-id-143	lemma expUnbounded
ref-0-id-144	lemma 1<=x+1(N)
ref-0-id-145	lemma expNonzero base
ref-0-id-146	lemma expNonzero indu
ref-0-id-147	lemma expNonzero
ref-0-id-148	lemma expNonzero(2)
ref-0-id-149	lemma halfBase base
ref-0-id-150	lemma halfBase indu
ref-0-id-151	lemma multiplyEquations(R)
ref-0-id-152	lemma nonreciprocalToRight(Eq)(1 term)(R)
ref-0-id-153	lemma positiveNonzero(R)
ref-0-id-154	lemma nonzeroProduct(2)(R)
ref-0-id-155	lemma halfBase
ref-0-id-156	lemma three2threeFactors(R)
ref-0-id-157	lemma x*y=zBackwards(R)
ref-0-id-158	lemma positiveInverted(R)
ref-0-id-159	lemma reciprocalToRight(Less)(R)
ref-0-id-160	lemma reciprocalToRight(Less)(1 term)(R)
ref-0-id-161	lemma nonreciprocalToLeft(Less)(R)
ref-0-id-162	lemma 1
ref-0-id-163	lemma switchFactors(1/x
ref-0-id-164	lemma smallHalving
ref-0-id-165	lemma intervalSize(anyPositive)
ref-0-id-166	lemma USdecreasing(+n) base
ref-0-id-167	lemma USdecreasing(+n) indu
ref-0-id-168	lemma USdecreasing(+n)
ref-0-id-169	lemma USdecreasing
ref-0-id-170	lemma leqAdditionLeft(R)
ref-0-id-171	lemma toNotLess(R)
ref-0-id-172	lemma limitOfUSIsLeq
ref-0-id-173	lemma subtractEquations(Less)(R)
ref-0-id-174	lemma subtractEquationsLeft(Less)(R)
ref-0-id-175	lemma lessNegated(Negative)(R)
ref-0-id-176	prop lemma from negated and (imply)
ref-0-id-177	prop lemma remove double neg (consequent)
ref-0-id-178	lemma fromNotUpperBound
ref-0-id-179	lemma leqNUB
ref-0-id-180	lemma USlimitIsLeastUpperBound helper
ref-0-id-181	lemma USlimitIsLeastUpperBound
ref-0-id-182	pred lemma exist mp3
ref-0-id-183	lemma greaterPositive(N)
ref-0-id-184	lemma ysFClose helper
ref-0-id-185	lemma ysFClose
ref-0-id-186	lemma ysFCauchy helper
ref-0-id-187	lemma ysFCauchy
ref-0-id-188	lemma from<<==
ref-0-id-189	lemma to<<==
ref-0-id-190	lemma nonnegativeNumerical(F)
ref-0-id-191	lemma negativeNumerical(F)
ref-0-id-192	tester1
ref-0-id-193	tester2
ref-0-id-194	tester3
ref-0-id-195	tester4
ref-0-id-196	tester5
ref-0-id-197	tester6