|
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
|
