Nuprl Lemma : two-squares-iff

x:ℕ
  (∃y,z:ℕ(((y y) (z z)) x ∈ ℤ)
  ⇐⇒ ∃y:ℕisqrt(x) 1. ((isqrt(x y) isqrt(x y)) (x y) ∈ ℤ))


Proof




Definitions occuring in Statement :  isqrt: isqrt(x) int_seg: {i..j-} nat: all: x:A. B[x] exists: x:A. B[x] iff: ⇐⇒ Q multiply: m subtract: m add: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T implies:  Q iff: ⇐⇒ Q and: P ∧ Q exists: x:A. B[x] subtype_rel: A ⊆B nat: so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a rev_implies:  Q int_seg: {i..j-} prop: or: P ∨ Q decidable: Dec(P) lelt: i ≤ j < k top: Top false: False satisfiable_int_formula: satisfiable_int_formula(fmla) not: ¬A ge: i ≥  guard: {T} sq_type: SQType(T) less_than': less_than'(a;b) le: A ≤ B uiff: uiff(P;Q)
Lemmas referenced :  isqrt-property isqrt_wf istype-int set_subtype_base le_wf int_subtype_base int_seg_wf lelt_wf less_than_wf nat_wf mul_bounds_1a decidable__lt 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 full-omega-unsat decidable__le nat_properties int_formula_prop_eq_lemma intformeq_wf int_term_value_mul_lemma itermMultiply_wf mul_preserves_le isqrt-of-square int_term_value_subtract_lemma itermSubtract_wf decidable__equal_int subtype_base_sq false_wf int_seg_subtype_nat int_seg_properties subtract_wf equal_wf exists_wf multiply-is-int-iff
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis Error :inhabitedIsType,  independent_pairFormation sqequalRule Error :productIsType,  because_Cache Error :equalityIsType4,  baseApply closedConclusion baseClosed applyEquality intEquality Error :lambdaEquality_alt,  natural_numberEquality independent_isectElimination productElimination Error :universeIsType,  addEquality setElimination rename multiplyEquality Error :equalityIsType1,  equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination dependent_pairFormation unionElimination dependent_set_memberEquality voidEquality voidElimination isect_memberEquality int_eqEquality lambdaEquality approximateComputation applyLambdaEquality cumulativity instantiate lambdaFormation promote_hyp pointwiseFunctionality

Latex:
\mforall{}x:\mBbbN{}
    (\mexists{}y,z:\mBbbN{}.  (((y  *  y)  +  (z  *  z))  =  x)
    \mLeftarrow{}{}\mRightarrow{}  \mexists{}y:\mBbbN{}isqrt(x)  +  1.  ((isqrt(x  -  y  *  y)  *  isqrt(x  -  y  *  y))  =  (x  -  y  *  y)))



Date html generated: 2019_06_20-PM-02_37_21
Last ObjectModification: 2019_06_12-PM-00_26_06

Theory : num_thy_1


Home Index