### Nuprl Lemma : gcd_reduce_wf

[p,q:ℤ].  (gcd_reduce(p;q) ∈ ℕ × ℤ × ℤ)

Proof

Definitions occuring in Statement :  gcd_reduce: gcd_reduce(p;q) nat: uall: [x:A]. B[x] member: t ∈ T product: x:A × B[x] int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T gcd_reduce: gcd_reduce(p;q) subtype_rel: A ⊆B all: x:A. B[x] so_lambda: λ2x.t[x] prop: and: P ∧ Q nat: so_apply: x[s] exists: x:A. B[x] implies:  Q spreadn: spread4
Lemmas referenced :  gcd-reduce-ext subtype_rel_self all_wf exists_wf nat_wf equal-wf-base-T int_subtype_base equal-wf-base equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut applyEquality thin instantiate extract_by_obid hypothesis sqequalRule sqequalHypSubstitution isectElimination functionEquality intEquality lambdaEquality productEquality hypothesisEquality multiplyEquality setElimination rename because_Cache baseApply closedConclusion baseClosed lambdaFormation spreadEquality productElimination dependent_pairEquality independent_pairEquality equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination axiomEquality isect_memberEquality

Latex:
\mforall{}[p,q:\mBbbZ{}].    (gcd\_reduce(p;q)  \mmember{}  \mBbbN{}  \mtimes{}  \mBbbZ{}  \mtimes{}  \mBbbZ{})

Date html generated: 2018_05_21-PM-00_59_30
Last ObjectModification: 2018_05_19-AM-06_35_44

Theory : num_thy_1

Home Index