Nuprl Lemma : divides_wf

[a,b:ℤ].  (a b ∈ ℙ)


Proof




Definitions occuring in Statement :  divides: a uall: [x:A]. B[x] prop: member: t ∈ T int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T divides: a so_lambda: λ2x.t[x] subtype_rel: A ⊆B so_apply: x[s]
Lemmas referenced :  exists_wf equal-wf-base int_subtype_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin intEquality lambdaEquality hypothesisEquality applyEquality hypothesis baseApply closedConclusion baseClosed because_Cache axiomEquality equalityTransitivity equalitySymmetry Error :inhabitedIsType,  isect_memberEquality Error :universeIsType

Latex:
\mforall{}[a,b:\mBbbZ{}].    (a  |  b  \mmember{}  \mBbbP{})



Date html generated: 2019_06_20-PM-02_19_51
Last ObjectModification: 2018_09_26-PM-05_45_20

Theory : num_thy_1


Home Index