Nuprl Lemma : Prime-isOdd
∀p:Prime. ((¬(p = 2 ∈ ℤ)) ⇒ (↑isOdd(p)))
Proof
Definitions occuring in Statement :
Prime: Prime,
isOdd: isOdd(n),
assert: ↑b,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
squash: ↓T,
prop: ℙ,
not: ¬A,
false: False,
less_than': less_than'(a;b),
and: P ∧ Q,
le: A ≤ B,
nat: ℕ,
subtype_rel: A ⊆r B,
sq_stable: SqStable(P),
int_upper: {i...},
member: t ∈ T,
uall: ∀[x:A]. B[x],
Prime: Prime,
implies: P ⇒ Q,
all: ∀x:A. B[x]
Lemmas referenced :
Prime_wf,
equal-wf-T-base,
not_wf,
le_wf,
false_wf,
int_upper_subtype_nat,
prime-isOdd,
isOdd_wf,
sq_stable__assert
Rules used in proof :
intEquality,
imageElimination,
baseClosed,
imageMemberEquality,
independent_pairFormation,
sqequalRule,
natural_numberEquality,
dependent_set_memberEquality,
applyEquality,
dependent_functionElimination,
independent_functionElimination,
hypothesis,
hypothesisEquality,
isectElimination,
extract_by_obid,
introduction,
cut,
rename,
thin,
setElimination,
sqequalHypSubstitution,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}p:Prime. ((\mneg{}(p = 2)) {}\mRightarrow{} (\muparrow{}isOdd(p)))
Date html generated:
2018_05_21-PM-06_58_02
Last ObjectModification:
2017_12_31-PM-06_12_35
Theory : general
Home
Index