Nuprl Lemma : is_prime_wf

[n:ℕ]. (is_prime(n) ∈ 𝔹)


Proof




Definitions occuring in Statement :  is_prime: is_prime(n) nat: bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T is_prime: is_prime(n) subtype_rel: A ⊆B all: x:A. B[x] nat: prop: implies:  Q decidable: Dec(P) or: P ∨ Q isl: isl(x)
Lemmas referenced :  decidable__prime subtype_rel_self nat_wf decidable_wf prime_wf btrue_wf bfalse_wf equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule applyEquality thin instantiate extract_by_obid hypothesis sqequalHypSubstitution isectElimination functionEquality setElimination rename hypothesisEquality because_Cache lambdaFormation unionElimination equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination axiomEquality

Latex:
\mforall{}[n:\mBbbN{}].  (is\_prime(n)  \mmember{}  \mBbbB{})



Date html generated: 2018_05_21-PM-06_59_03
Last ObjectModification: 2018_05_19-PM-04_41_40

Theory : general


Home Index