### Nuprl Lemma : rem_nrel_wf

[a:ℕ]. ∀[n:ℕ+]. ∀[r:ℕ].  (Rem(a;n;r) ∈ ℙ)

Proof

Definitions occuring in Statement :  rem_nrel: Rem(a;n;r) nat_plus: + nat: uall: [x:A]. B[x] prop: member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T rem_nrel: Rem(a;n;r) so_lambda: λ2x.t[x] prop: and: P ∧ Q nat: nat_plus: + so_apply: x[s]
Lemmas referenced :  exists_wf nat_wf div_nrel_wf equal_wf nat_plus_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis lambdaEquality productEquality hypothesisEquality intEquality addEquality multiplyEquality setElimination rename axiomEquality equalityTransitivity equalitySymmetry Error :inhabitedIsType,  isect_memberEquality Error :universeIsType,  because_Cache

Latex:
\mforall{}[a:\mBbbN{}].  \mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[r:\mBbbN{}].    (Rem(a;n;r)  \mmember{}  \mBbbP{})

Date html generated: 2019_06_20-PM-01_14_38
Last ObjectModification: 2018_09_26-PM-02_32_22

Theory : int_2

Home Index