### Nuprl Lemma : mod2-is-zero

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

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` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  squash: `↓T` exists: `∃x:A. B[x]` top: `Top` subtract: `n - m` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` or: `P ∨ Q` decidable: `Dec(P)` lelt: `i ≤ j < k` int_seg: `{i..j-}` subtype_rel: `A ⊆r B` absval: `|i|` less_than': `less_than'(a;b)` le: `A ≤ B` so_apply: `x[s]` so_lambda: `λ2x.t[x]` nat: `ℕ` and: `P ∧ Q` uiff: `uiff(P;Q)` int_nzero: `ℤ-o` prop: `ℙ` false: `False` guard: `{T}` sq_type: `SQType(T)` implies: `P `` Q` not: `¬A` nequal: `a ≠ b ∈ T ` true: `True` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]` has-value: `(a)↓` modulus: `a mod n` all: `∀x:A. B[x]`
Lemmas referenced :  rem-exact mul-swap mul-distributes zero-mul mul-distributes-right mul-associates subtract_wf iff_weakening_equal subtype_rel_self squash_wf iff_wf equal_wf less_than_irreflexivity less_than_transitivity1 le-add-cancel mul-commutes int_seg_cases le-add-cancel2 add-zero subtype_rel_sets exists_wf decidable__int_equal int_seg_wf less_than_wf and_wf le-add-cancel-alt zero-add add-swap add_functionality_wrt_le add-commutes minus-one-mul-top add-associates minus-one-mul minus-add condition-implies-le less-iff-le not-le-2 decidable__le absval_pos false_wf le_wf set_subtype_base nat_wf absval_wf absval_strict_ubound rem_bounds_absval nequal_wf div_rem_sum true_wf equal-wf-base int_subtype_base subtype_base_sq int-value-type value-type-has-value
Rules used in proof :  imageMemberEquality universeEquality imageElimination divideEquality dependent_pairFormation setEquality hypothesis_subsumption promote_hyp levelHypothesis voidEquality isect_memberEquality addEquality unionElimination minusEquality multiplyEquality closedConclusion baseApply rename setElimination applyEquality independent_pairFormation lambdaEquality productElimination because_Cache dependent_set_memberEquality baseClosed voidElimination independent_functionElimination equalitySymmetry equalityTransitivity dependent_functionElimination cumulativity instantiate addLevel natural_numberEquality hypothesisEquality remainderEquality hypothesis independent_isectElimination intEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut callbyvalueReduce sqequalRule lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

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

Date html generated: 2018_07_25-PM-01_27_54
Last ObjectModification: 2018_06_27-PM-04_13_38

Theory : arithmetic

Home Index