### Nuprl Lemma : divides_functionality_wrt_assoced

`∀a,a',b,b':ℤ.  ((a ~ a') `` (b ~ b') `` (a | b `⇐⇒` a' | b'))`

Proof

Definitions occuring in Statement :  assoced: `a ~ b` divides: `b | a` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` int: `ℤ`
Definitions unfolded in proof :  assoced: `a ~ b` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` iff: `P `⇐⇒` Q` member: `t ∈ T` guard: `{T}` uall: `∀[x:A]. B[x]` prop: `ℙ` rev_implies: `P `` Q`
Lemmas referenced :  divides_transitivity divides_wf istype-int
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep Error :lambdaFormation_alt,  sqequalHypSubstitution productElimination thin independent_pairFormation cut hypothesis introduction extract_by_obid dependent_functionElimination hypothesisEquality independent_functionElimination Error :universeIsType,  isectElimination Error :productIsType,  Error :inhabitedIsType

Latex:
\mforall{}a,a',b,b':\mBbbZ{}.    ((a  \msim{}  a')  {}\mRightarrow{}  (b  \msim{}  b')  {}\mRightarrow{}  (a  |  b  \mLeftarrow{}{}\mRightarrow{}  a'  |  b'))

Date html generated: 2019_06_20-PM-02_20_52
Last ObjectModification: 2018_10_03-AM-00_35_50

Theory : num_thy_1

Home Index