Nuprl Lemma : prime-isOdd
∀p:ℕ. (prime(p) ⇒ (¬(p = 2 ∈ ℤ)) ⇒ (↑isOdd(p)))
Proof
Definitions occuring in Statement :
isOdd: isOdd(n),
prime: prime(a),
nat: ℕ,
assert: ↑b,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
nat: ℕ,
prop: ℙ,
exists: ∃x:A. B[x],
not: ¬A,
uimplies: b supposing a,
and: P ∧ Q,
uiff: uiff(P;Q),
member: t ∈ T,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
all: ∀x:A. B[x],
subtype_rel: A ⊆r B,
divides: b | a,
true: True,
guard: {T},
sq_type: SQType(T),
top: Top,
false: False,
satisfiable_int_formula: satisfiable_int_formula(fmla),
ge: i ≥ j ,
or: P ∨ Q,
iff: P ⇐⇒ Q
Lemmas referenced :
nat_wf,
prime_wf,
equal-wf-T-base,
not_wf,
isEven_wf,
assert_wf,
even-implies-two-times,
odd-iff-not-even,
divides-prime,
int_subtype_base,
subtype_base_sq,
int_formula_prop_le_lemma,
int_term_value_mul_lemma,
int_term_value_minus_lemma,
intformle_wf,
itermMultiply_wf,
itermMinus_wf,
int_formula_prop_wf,
int_formula_prop_not_lemma,
int_term_value_var_lemma,
int_term_value_constant_lemma,
int_formula_prop_eq_lemma,
int_formula_prop_and_lemma,
intformnot_wf,
itermVar_wf,
itermConstant_wf,
intformeq_wf,
intformand_wf,
full-omega-unsat,
nat_properties,
assoced_wf,
equal-wf-base-T,
equal-wf-base,
or_wf,
assoced_elim
Rules used in proof :
baseClosed,
intEquality,
rename,
setElimination,
hypothesis,
independent_functionElimination,
hypothesisEquality,
dependent_functionElimination,
independent_isectElimination,
productElimination,
because_Cache,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
equalitySymmetry,
equalityTransitivity,
natural_numberEquality,
applyEquality,
closedConclusion,
baseApply,
sqequalRule,
dependent_pairFormation,
cumulativity,
instantiate,
independent_pairFormation,
voidEquality,
voidElimination,
isect_memberEquality,
int_eqEquality,
lambdaEquality,
approximateComputation,
unionElimination,
promote_hyp,
minusEquality,
orFunctionality,
addLevel
Latex:
\mforall{}p:\mBbbN{}. (prime(p) {}\mRightarrow{} (\mneg{}(p = 2)) {}\mRightarrow{} (\muparrow{}isOdd(p)))
Date html generated:
2018_05_21-PM-00_57_42
Last ObjectModification:
2017_12_31-PM-06_10_15
Theory : num_thy_1
Home
Index