Nuprl Lemma : mod2-is-zero

x:ℤ((x mod 2) 0 ∈ ℤ ⇐⇒ ∃n:ℤ(x (2 n) ∈ ℤ))


Proof




Definitions occuring in Statement :  modulus: mod n all: x:A. B[x] exists: x:A. B[x] iff: ⇐⇒ Q multiply: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  squash: T exists: x:A. B[x] top: Top subtract: m rev_implies:  Q iff: ⇐⇒ Q or: P ∨ Q decidable: Dec(P) lelt: i ≤ j < k int_seg: {i..j-} subtype_rel: A ⊆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:  Q not: ¬A nequal: a ≠ b ∈  true: True uimplies: supposing a member: t ∈ T uall: [x:A]. B[x] has-value: (a)↓ modulus: 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