Nuprl Lemma : l_sum_nonneg
∀[L:ℤ List]. ((∀x∈L.0 ≤ x) ⇒ (0 ≤ l_sum(L)))
Proof
Definitions occuring in Statement :
l_sum: l_sum(L),
l_all: (∀x∈L.P[x]),
list: T List,
uall: ∀[x:A]. B[x],
le: A ≤ B,
implies: P ⇒ Q,
natural_number: $n,
int: ℤ
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
so_lambda: λ2x.t[x],
prop: ℙ,
so_apply: x[s]
Lemmas referenced :
l_sum-lower-bound,
zero-mul,
length_wf,
l_all_wf,
le_wf,
istype-int,
l_member_wf,
list_wf
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
dependent_functionElimination,
thin,
natural_numberEquality,
Error :isect_memberFormation_alt,
hypothesis,
isectElimination,
hypothesisEquality,
Error :lambdaFormation_alt,
independent_functionElimination,
sqequalRule,
intEquality,
Error :universeIsType,
Error :lambdaEquality_alt,
setElimination,
rename,
Error :setIsType
Latex:
\mforall{}[L:\mBbbZ{} List]. ((\mforall{}x\mmember{}L.0 \mleq{} x) {}\mRightarrow{} (0 \mleq{} l\_sum(L)))
Date html generated:
2019_06_20-PM-01_43_58
Last ObjectModification:
2019_02_22-PM-00_00_13
Theory : list_1
Home
Index