Nuprl Lemma : coprime_iff_ndivides
∀a,p:ℤ. (prime(p) ⇒ (CoPrime(p,a) ⇐⇒ ¬(p | a)))
Proof
Definitions occuring in Statement :
prime: prime(a),
coprime: CoPrime(a,b),
divides: b | a,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
implies: P ⇒ Q,
int: ℤ
Definitions unfolded in proof :
rev_implies: P ⇐ Q,
prop: ℙ,
uall: ∀[x:A]. B[x],
member: t ∈ T,
false: False,
not: ¬A,
and: P ∧ Q,
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
all: ∀x:A. B[x],
prime: prime(a),
assoced: a ~ b,
or: P ∨ Q,
guard: {T}
Lemmas referenced :
istype-int,
prime_wf,
not_wf,
coprime_wf,
divides_wf,
coprime_elim,
divides_reflexivity,
coprime_intro,
prime_elim,
divides_transitivity
Rules used in proof :
Error :inhabitedIsType,
hypothesisEquality,
isectElimination,
extract_by_obid,
introduction,
Error :universeIsType,
voidElimination,
independent_functionElimination,
sqequalHypSubstitution,
hypothesis,
thin,
cut,
independent_pairFormation,
Error :lambdaFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
productElimination,
dependent_functionElimination,
unionElimination
Latex:
\mforall{}a,p:\mBbbZ{}. (prime(p) {}\mRightarrow{} (CoPrime(p,a) \mLeftarrow{}{}\mRightarrow{} \mneg{}(p | a)))
Date html generated:
2019_06_20-PM-02_23_31
Last ObjectModification:
2019_01_15-PM-03_02_34
Theory : num_thy_1
Home
Index