Nuprl Lemma : tsqrt-property

[n:ℕ]. ((t(tsqrt(n)) ≤ n) ∧ n < t(tsqrt(n) 1))


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 and: P ∧ Q add: m natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T tsqrt: tsqrt(n) 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 implies:  Q not: ¬A top: Top and: P ∧ Q prop: le: A ≤ B subtype_rel: A ⊆B less_than': less_than'(a;b) guard: {T} uiff: uiff(P;Q) so_lambda: λ2x.t[x] so_apply: x[s] sq_type: SQType(T) has-value: (a)↓ bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  bfalse: ff bnot: ¬bb assert: b squash: T true: True iff: ⇐⇒ Q rev_implies:  Q cand: c∧ B
Lemmas referenced :  isqrt_wf nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermMultiply_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_mul_lemma int_term_value_var_lemma int_formula_prop_wf le_wf nat_wf equal_wf less_than'_wf triangular-num_wf tsqrt_wf member-less_than add_nat_wf false_wf add-is-int-iff itermAdd_wf intformeq_wf int_term_value_add_lemma int_formula_prop_eq_lemma value-type-has-value set-value-type int-value-type isqrt-property subtype_base_sq set_subtype_base int_subtype_base le_int_wf bool_wf eqtt_to_assert assert_of_le_int eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot less_than_wf squash_wf true_wf triangular-num-add1 iff_weakening_equal twice-triangular multiply-is-int-iff decidable__lt intformless_wf int_formula_prop_less_lemma decidable__equal_int subtract_wf subtract-add-cancel itermSubtract_wf int_term_value_subtract_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin dependent_set_memberEquality multiplyEquality natural_numberEquality setElimination rename hypothesisEquality hypothesis dependent_functionElimination unionElimination independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation computeAll lambdaFormation equalityTransitivity equalitySymmetry independent_functionElimination productElimination independent_pairEquality applyEquality axiomEquality addEquality applyLambdaEquality pointwiseFunctionality promote_hyp baseApply closedConclusion baseClosed because_Cache instantiate cumulativity callbyvalueReduce equalityElimination addLevel imageElimination imageMemberEquality universeEquality productEquality

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



Date html generated: 2019_06_20-PM-02_38_39
Last ObjectModification: 2019_06_12-PM-00_26_57

Theory : num_thy_1


Home Index