Nuprl Lemma : tsqrt-unique

[n,x:ℕ].  (((t(x) ≤ n) ∧ n < t(x 1))  (x tsqrt(n) ∈ ℤ))


Proof




Definitions occuring in Statement :  tsqrt: tsqrt(n) triangular-num: t(n) nat: less_than: a < b uall: [x:A]. B[x] le: A ≤ B implies:  Q and: P ∧ Q add: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T implies:  Q and: P ∧ Q prop: subtype_rel: A ⊆B nat: ge: i ≥  all: x:A. B[x] decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top less_than: a < b squash: T le: A ≤ B less_than': less_than'(a;b) guard: {T}
Lemmas referenced :  tsqrt-property le_wf triangular-num_wf less_than_wf nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_wf nat_wf decidable__lt tsqrt_wf triangular-num-le intformless_wf int_formula_prop_less_lemma decidable__equal_int intformeq_wf int_formula_prop_eq_lemma add_nat_wf false_wf equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalHypSubstitution productElimination thin extract_by_obid isectElimination hypothesisEquality hypothesis productEquality applyEquality because_Cache sqequalRule setElimination rename dependent_set_memberEquality addEquality natural_numberEquality dependent_functionElimination unionElimination independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll axiomEquality imageElimination equalityTransitivity equalitySymmetry applyLambdaEquality independent_functionElimination

Latex:
\mforall{}[n,x:\mBbbN{}].    (((t(x)  \mleq{}  n)  \mwedge{}  n  <  t(x  +  1))  {}\mRightarrow{}  (x  =  tsqrt(n)))



Date html generated: 2019_06_20-PM-02_38_45
Last ObjectModification: 2019_06_12-PM-00_27_02

Theory : num_thy_1


Home Index