Nuprl Lemma : ab-divides-a^2+b^2+1

a,b:ℤ.
  ((a b) (((a a) (b b)) 1)
  ⇐⇒ ∃n:ℕ((<|a|, |b|> vexample(n;1;1) ∈ (ℤ × ℤ)) ∨ (<|b|, |a|> vexample(n;1;1) ∈ (ℤ × ℤ))))


Proof




Definitions occuring in Statement :  vexample: vexample(n;a;b) divides: a absval: |i| nat: all: x:A. B[x] exists: x:A. B[x] iff: ⇐⇒ Q or: P ∨ 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] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T uall: [x:A]. B[x] subtype_rel: A ⊆B prop: rev_implies:  Q exists: x:A. B[x] or: P ∨ Q nat: so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a squash: T guard: {T} true: True divides: a decidable: Dec(P) le: A ≤ B not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) false: False top: Top uiff: uiff(P;Q) ge: i ≥  pi2: snd(t) pi1: fst(t)
Lemmas referenced :  divides_wf absval_wf istype-nat int_subtype_base set_subtype_base le_wf istype-int absval-divides absval_mul iff_weakening_equal squash_wf true_wf add_functionality_wrt_eq absval_squared subtype_rel_self Vieta-jumping-example2-corollary decidable__le decidable__equal_int full-omega-unsat intformand_wf intformnot_wf intformeq_wf itermAdd_wf itermMultiply_wf itermVar_wf itermConstant_wf int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_add_lemma int_term_value_mul_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_wf add-is-int-iff multiply-is-int-iff intformle_wf int_formula_prop_le_lemma false_wf vexample_wf nat_properties istype-le pi2_wf pi1_wf nat_wf equal_wf istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  cut thin independent_pairFormation Error :universeIsType,  introduction extract_by_obid sqequalHypSubstitution isectElimination multiplyEquality hypothesisEquality hypothesis applyEquality because_Cache sqequalRule addEquality natural_numberEquality Error :productIsType,  Error :unionIsType,  Error :equalityIstype,  baseApply closedConclusion baseClosed intEquality Error :lambdaEquality_alt,  Error :inhabitedIsType,  independent_isectElimination sqequalBase equalitySymmetry productElimination independent_functionElimination promote_hyp dependent_functionElimination setElimination rename equalityTransitivity imageElimination imageMemberEquality instantiate universeEquality unionElimination approximateComputation Error :dependent_pairFormation_alt,  int_eqEquality Error :isect_memberEquality_alt,  voidElimination Error :inlFormation_alt,  pointwiseFunctionality Error :inrFormation_alt,  Error :dependent_set_memberEquality_alt,  applyLambdaEquality

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



Date html generated: 2019_06_20-PM-02_43_55
Last ObjectModification: 2019_03_11-PM-06_33_37

Theory : num_thy_1


Home Index