Nuprl Lemma : mod2-is-one

`∀x:ℤ. ((x mod 2) = 1 ∈ ℤ `⇐⇒` ∃n:ℤ. (x = ((2 * n) + 1) ∈ ℤ))`

Proof

Definitions occuring in Statement :  modulus: `a mod n` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` multiply: `n * m` add: `n + m` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  so_apply: `x[s]` so_lambda: `λ2x.t[x]` decidable: `Dec(P)` exists: `∃x:A. B[x]` bfalse: `ff` btrue: `tt` ifthenelse: `if b then t else f fi ` or: `P ∨ Q` less_than': `less_than'(a;b)` le: `A ≤ B` uiff: `uiff(P;Q)` top: `Top` subtract: `n - m` rev_implies: `P `` Q` and: `P ∧ Q` iff: `P `⇐⇒` Q` subtype_rel: `A ⊆r B` prop: `ℙ` false: `False` guard: `{T}` sq_type: `SQType(T)` uimplies: `b supposing a` implies: `P `` Q` not: `¬A` nequal: `a ≠ b ∈ T ` true: `True` int_nzero: `ℤ-o` uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]`
Lemmas referenced :  iff_wf mod2-is-zero exists_wf minus-minus mul-associates minus-add not-equal-2 false_wf decidable__int_equal assert_of_bnot iff_weakening_uiff iff_transitivity eqff_to_assert assert_of_eq_int eqtt_to_assert bool_subtype_base bool_wf bool_cases le-add-cancel add-zero add_functionality_wrt_le minus-one-mul-top minus-one-mul condition-implies-le le_antisymmetry_iff not_wf bnot_wf assert_wf zero-add add-commutes add-swap add-associates nequal_wf true_wf equal-wf-base int_subtype_base subtype_base_sq modulus_wf eq_int_wf subtract_wf mod2-add1
Rules used in proof :  promote_hyp multiplyEquality dependent_pairFormation impliesFunctionality unionElimination productElimination addEquality minusEquality voidEquality isect_memberEquality lambdaEquality closedConclusion baseApply independent_pairFormation sqequalRule because_Cache applyEquality baseClosed voidElimination independent_functionElimination equalitySymmetry equalityTransitivity independent_isectElimination cumulativity instantiate addLevel dependent_set_memberEquality hypothesis natural_numberEquality hypothesisEquality isectElimination thin dependent_functionElimination sqequalHypSubstitution extract_by_obid introduction intEquality cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}x:\mBbbZ{}.  ((x  mod  2)  =  1  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbZ{}.  (x  =  ((2  *  n)  +  1)))

Date html generated: 2018_07_25-PM-01_27_57
Last ObjectModification: 2018_06_27-PM-05_54_42

Theory : arithmetic

Home Index