Nuprl Lemma : Vieta-jumping-example2

∀k:ℤ. ∀a,b:ℕ. (((((a * a) + (b * b)) + 1) = (k * a * b) ∈ ℤ) ⇒ (k = 3 ∈ ℤ))

Proof

Definitions occuring in Statement : nat: ℕ, all: ∀x:A. B[x], implies: P ⇒ Q, multiply: n * m, add: n + m, natural_number: $n, int: ℤ, equal: s = t ∈ T
Definitions unfolded in proof : all: ∀x:A. B[x], uall: ∀[x:A]. B[x], member: t ∈ T, nat: ℕ, implies: P ⇒ Q, false: False, ge: i ≥ j , uimplies: b supposing a, not: ¬A, satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], top: Top, and: P ∧ Q, prop: ℙ, guard: {T}, int_seg: {i..j^-}, lelt: i ≤ j < k, le: A ≤ B, decidable: Dec(P), or: P ∨ Q, subtype_rel: A ⊆r B, so_lambda: λ₂x.t[x], so_apply: x[s], sq_type: SQType(T), cand: A c∧ B, nat_plus: ℕ⁺
Lemmas referenced : nat_properties, full-omega-unsat, intformand_wf, intformle_wf, itermConstant_wf, itermVar_wf, intformless_wf, istype-int, int_formula_prop_and_lemma, istype-void, int_formula_prop_le_lemma, int_term_value_constant_lemma, int_term_value_var_lemma, int_formula_prop_less_lemma, int_formula_prop_wf, ge_wf, istype-less_than, int_seg_properties, int_seg_wf, subtract-1-ge-0, decidable__equal_int, subtract_wf, subtype_base_sq, set_subtype_base, int_subtype_base, 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, subtype_rel_self, itermAdd_wf, itermMultiply_wf, int_term_value_add_lemma, int_term_value_mul_lemma, le_wf, istype-nat, mul_bounds_1a, mul_cancel_in_le, mul_nat_plus, mul_preserves_le
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, Error :lambdaFormation_alt, cut, thin, introduction, extract_by_obid, sqequalHypSubstitution, isectElimination, hypothesisEquality, hypothesis, setElimination, rename, intWeakElimination, natural_numberEquality, independent_isectElimination, approximateComputation, independent_functionElimination, Error :dependent_pairFormation_alt, Error :lambdaEquality_alt, int_eqEquality, dependent_functionElimination, Error :isect_memberEquality_alt, voidElimination, sqequalRule, independent_pairFormation, Error :universeIsType, axiomEquality, Error :functionIsTypeImplies, Error :inhabitedIsType, productElimination, unionElimination, applyEquality, instantiate, because_Cache, equalityTransitivity, equalitySymmetry, applyLambdaEquality, Error :dependent_set_memberEquality_alt, Error :productIsType, hypothesis_subsumption, Error :equalityIstype, baseApply, closedConclusion, baseClosed, intEquality, sqequalBase, addEquality, cumulativity, multiplyEquality, promote_hyp

Latex:
\mforall{}k:\mBbbZ{}. \mforall{}a,b:\mBbbN{}. (((((a * a) + (b * b)) + 1) = (k * a * b)) {}\mRightarrow{} (k = 3)) Date html generated: 2019_06_20-PM-02_43_17 Last ObjectModification: 2019_03_10-PM-10_43_49 Theory : num_thy_1 Home Index