Nuprl Lemma : gcd_p_neg_arg
∀a,b,y:ℤ. (GCD(a;b;y) ⇒ GCD(a;-b;y))
Proof
Definitions occuring in Statement :
gcd_p: GCD(a;b;y),
all: ∀x:A. B[x],
implies: P ⇒ Q,
minus: -n,
int: ℤ
Definitions unfolded in proof :
prop: ℙ,
uall: ∀[x:A]. B[x],
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
member: t ∈ T,
cand: A c∧ B,
and: P ∧ Q,
implies: P ⇒ Q,
all: ∀x:A. B[x],
gcd_p: GCD(a;b;y)
Lemmas referenced :
istype-int,
divides_wf,
minus-minus,
divides_invar_2
Rules used in proof :
Error :functionIsType,
Error :inhabitedIsType,
Error :universeIsType,
Error :productIsType,
because_Cache,
isectElimination,
independent_functionElimination,
minusEquality,
hypothesisEquality,
dependent_functionElimination,
extract_by_obid,
introduction,
independent_pairFormation,
hypothesis,
cut,
thin,
productElimination,
sqequalHypSubstitution,
Error :lambdaFormation_alt,
computationStep,
sqequalTransitivity,
sqequalReflexivity,
sqequalRule,
sqequalSubstitution
Latex:
\mforall{}a,b,y:\mBbbZ{}. (GCD(a;b;y) {}\mRightarrow{} GCD(a;-b;y))
Date html generated:
2019_06_20-PM-02_21_39
Last ObjectModification:
2019_06_18-PM-10_47_51
Theory : num_thy_1
Home
Index