Nuprl Lemma : Vieta-jumping-example2-corollary

k:ℤ. ∀a,b:ℕ.  (((((a a) (b b)) 1) (k b) ∈ ℤ (a ≤ b)  (∃n:ℕ(<a, b> vexample(n;1;1) ∈ (ℤ × ℤ)))\000C)


Proof




Definitions occuring in Statement :  vexample: vexample(n;a;b) nat: le: A ≤ B all: x:A. B[x] exists: x:A. B[x] implies:  Q pair: <a, b> product: x:A × B[x] multiply: m add: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T implies:  Q uall: [x:A]. B[x] uimplies: supposing a sq_type: SQType(T) guard: {T} int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q le: A ≤ B not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top prop: decidable: Dec(P) or: P ∨ Q subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] nat: ge: i ≥  subtract: m vexample: vexample(n;a;b) nat_plus: + squash: T true: True iff: ⇐⇒ Q cand: c∧ B bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) less_than: a < b less_than': less_than'(a;b) bfalse: ff bnot: ¬bb ifthenelse: if then else fi  assert: b rev_implies:  Q nequal: a ≠ b ∈  has-value: (a)↓ fun_exp: f^n primrec: primrec(n;b;c) primtailrec: primtailrec(n;i;b;f) compose: g
Lemmas referenced :  Vieta-jumping-example2 subtype_base_sq int_subtype_base int_seg_properties full-omega-unsat intformand_wf intformless_wf itermVar_wf itermConstant_wf intformle_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf int_seg_wf decidable__equal_int subtract_wf set_subtype_base lelt_wf intformnot_wf intformeq_wf itermSubtract_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_subtract_lemma decidable__le decidable__lt istype-le istype-less_than subtype_rel_self le_wf nat_wf equal-wf-base primrec-wf2 nat_properties itermAdd_wf int_term_value_add_lemma istype-nat itermMultiply_wf int_term_value_mul_lemma int_entire exp_preserves_lt less_than_wf squash_wf true_wf exp2 iff_weakening_equal mul_bounds_1a absval_unfold lt_int_wf eqtt_to_assert assert_of_lt_int istype-top eqff_to_assert bool_cases_sqequal bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf itermMinus_wf int_term_value_minus_lemma exp_preserves_le absval_wf absval_squared le_functionality multiply_functionality_wrt_le le_weakening eq_int_wf assert_of_eq_int neg_assert_of_eq_int add-subtract-cancel value-type-has-value set-value-type int-value-type product_subtype_base ge_wf subtract-1-ge-0 fun_exp_add_apply base_wf subtract-add-cancel fun_exp_com
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination instantiate isectElimination cumulativity intEquality independent_isectElimination equalityTransitivity equalitySymmetry setElimination rename productElimination natural_numberEquality approximateComputation Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  int_eqEquality Error :isect_memberEquality_alt,  voidElimination sqequalRule independent_pairFormation Error :universeIsType,  unionElimination applyEquality Error :inhabitedIsType,  applyLambdaEquality Error :dependent_set_memberEquality_alt,  because_Cache Error :productIsType,  hypothesis_subsumption Error :equalityIstype,  baseApply closedConclusion baseClosed sqequalBase Error :functionIsType,  functionEquality productEquality Error :setIsType,  addEquality independent_pairEquality multiplyEquality imageElimination imageMemberEquality universeEquality minusEquality equalityElimination lessCases Error :isect_memberFormation_alt,  axiomSqEquality Error :isectIsTypeImplies,  promote_hyp int_eqReduceTrueSq int_eqReduceFalseSq callbyvalueReduce sqleReflexivity intWeakElimination Error :functionIsTypeImplies,  sqequalIntensionalEquality functionExtensionality spreadEquality

Latex:
\mforall{}k:\mBbbZ{}.  \mforall{}a,b:\mBbbN{}.
    (((((a  *  a)  +  (b  *  b))  +  1)  =  (k  *  a  *  b))  {}\mRightarrow{}  (a  \mleq{}  b)  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  (<a,  b>  =  vexample(n;1;1))))



Date html generated: 2019_06_20-PM-02_43_47
Last ObjectModification: 2019_03_11-PM-06_29_12

Theory : num_thy_1


Home Index