Nuprl Lemma : ratLegendreSign_wf
∀[n:ℕ]. ∀[k:ℤ]. ∀[m:ℕ+]. (ratLegendreSign(n;k;m) ∈ {-1..2-})
Proof
Definitions occuring in Statement :
ratLegendreSign: ratLegendreSign(n;k;m),
int_seg: {i..j-},
nat_plus: ℕ+,
nat: ℕ,
uall: ∀[x:A]. B[x],
member: t ∈ T,
minus: -n,
natural_number: $n,
int: ℤ
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
ratLegendreSign: ratLegendreSign(n;k;m),
subtype_rel: A ⊆r B
Lemmas referenced :
ratsign_wf,
ratLegendre_wf,
nat_plus_wf,
istype-int,
istype-nat
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
independent_pairEquality,
hypothesisEquality,
hypothesis,
applyEquality,
lambdaEquality_alt,
setElimination,
rename,
inhabitedIsType,
equalityTransitivity,
equalitySymmetry,
axiomEquality,
universeIsType,
isect_memberEquality_alt,
isectIsTypeImplies
Latex:
\mforall{}[n:\mBbbN{}]. \mforall{}[k:\mBbbZ{}]. \mforall{}[m:\mBbbN{}\msupplus{}]. (ratLegendreSign(n;k;m) \mmember{} \{-1..2\msupminus{}\})
Date html generated:
2019_10_31-AM-06_21_35
Last ObjectModification:
2019_02_17-PM-00_55_19
Theory : reals_2
Home
Index