Nuprl Lemma : gcd_p_functionality_wrt_assoced
∀a,a',b,b',y,y':ℤ. ((a ~ a') ⇒ (b ~ b') ⇒ (y ~ y') ⇒ (GCD(a;b;y) ⇐⇒ GCD(a';b';y')))
Proof
Definitions occuring in Statement :
gcd_p: GCD(a;b;y),
assoced: a ~ b,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
int: ℤ
Definitions unfolded in proof :
prop: ℙ,
uall: ∀[x:A]. B[x],
member: t ∈ T,
gcd_p: GCD(a;b;y),
implies: P ⇒ Q,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
cand: A c∧ B,
rev_implies: P ⇐ Q,
uimplies: b supposing a
Lemmas referenced :
istype-int,
assoced_wf,
divides_wf,
divides_functionality_wrt_assoced,
assoced_weakening
Rules used in proof :
Error :inhabitedIsType,
hypothesis,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
Error :universeIsType,
Error :lambdaFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
independent_pairFormation,
productElimination,
dependent_functionElimination,
independent_functionElimination,
sqequalRule,
Error :productIsType,
Error :functionIsType,
because_Cache,
promote_hyp,
independent_isectElimination
Latex:
\mforall{}a,a',b,b',y,y':\mBbbZ{}. ((a \msim{} a') {}\mRightarrow{} (b \msim{} b') {}\mRightarrow{} (y \msim{} y') {}\mRightarrow{} (GCD(a;b;y) \mLeftarrow{}{}\mRightarrow{} GCD(a';b';y')))
Date html generated:
2019_06_20-PM-02_21_24
Last ObjectModification:
2019_01_11-PM-04_06_37
Theory : num_thy_1
Home
Index