### 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