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