Nuprl Lemma : square-iff-isqrt

x:ℕ(∃y:ℕ((y y) x ∈ ℤ⇐⇒ (isqrt(x) isqrt(x)) x ∈ ℤ)


Proof




Definitions occuring in Statement :  isqrt: isqrt(x) nat: all: x:A. B[x] exists: x:A. B[x] iff: ⇐⇒ Q multiply: m int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q exists: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a sq_type: SQType(T) guard: {T} prop: so_lambda: λ2x.t[x] nat: so_apply: x[s] rev_implies:  Q subtype_rel: A ⊆B decidable: Dec(P) or: P ∨ Q isqrt: isqrt(x) integer-sqrt-ext genrec-ap: genrec-ap ge: i ≥  less_than: a < b squash: T satisfiable_int_formula: satisfiable_int_formula(fmla) false: False not: ¬A top: Top nat_plus: + le: A ≤ B uiff: uiff(P;Q) less_than': less_than'(a;b) true: True subtract: m
Lemmas referenced :  integer-sqrt-ext int_entire int_formula_prop_or_lemma intformor_wf less_than_wf minus-zero minus-add add-commutes condition-implies-le le-add-cancel zero-add add-zero add-associates add_functionality_wrt_le not-equal-2 not-lt-2 false_wf multiply-is-int-iff mul_preserves_lt int_formula_prop_eq_lemma int_term_value_mul_lemma intformeq_wf itermMultiply_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_term_value_add_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformless_wf itermConstant_wf itermVar_wf itermAdd_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt le_wf decidable__le nat_properties mul_preserves_le decidable__lt decidable__equal_int isqrt-property isqrt_wf equal_wf nat_wf exists_wf int_subtype_base subtype_base_sq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut sqequalHypSubstitution productElimination thin instantiate lemma_by_obid isectElimination cumulativity intEquality independent_isectElimination hypothesis dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination sqequalRule lambdaEquality multiplyEquality setElimination rename hypothesisEquality dependent_pairFormation applyEquality because_Cache natural_numberEquality unionElimination addEquality dependent_set_memberEquality imageElimination int_eqEquality isect_memberEquality voidElimination voidEquality computeAll introduction baseApply closedConclusion baseClosed minusEquality pointwiseFunctionality promote_hyp

Latex:
\mforall{}x:\mBbbN{}.  (\mexists{}y:\mBbbN{}.  ((y  *  y)  =  x)  \mLeftarrow{}{}\mRightarrow{}  (isqrt(x)  *  isqrt(x))  =  x)



Date html generated: 2019_06_20-PM-02_37_05
Last ObjectModification: 2019_06_12-PM-00_25_57

Theory : num_thy_1


Home Index