# Integer: deciding membership, the meaning of the minus sign, and closure under negation

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-integer/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-integer-01 · production-20261019-adopted-96



## Goal and scope

Inside the reals, take Z={0}∪N⁺∪{−n ∣ n∈N⁺} (N contains 0 by the OCME convention, N⁺=N∖{0}, and −n is the additive inverse of n). Prove −7∈Z; show that the decimal numeral '3.0' denotes the integer 3; prove −2.5∉Z; prove −(−a)=a from uniqueness of additive inverses, in particular −(−4)=4; prove −z∈Z for every z∈Z; and use 5−8=5+(−8)=−3 to tell binary subtraction from the unary minus sign.

Treats only the membership and notation boundary the MKO sets up: the three parts of Z, the minus sign as an additive inverse, and closure under negation. Z is described inside ℝ (using only the addition axioms and order), with N characterized as the smallest inductive set and taken as a premise. It does not prove closure of Z under addition or multiplication and does not treat order or divisibility (the MKO says these need their own claims); it does not treat the semantic correspondence with Lean's Int; and it does not change the canonical MKO or its English edition.





## Givens and symbols


- add_assoc
- add_comm
- add_zero
- add_inverse
- order_basics
- numeric_evaluation


- G1 — Work inside the reals ℝ (using only the addition axioms and order). N⊆ℝ is the natural numbers under the OCME convention (containing 0, MKO assumption a1), the smallest inductive subset of ℝ: 0∈N, x∈N ⇒ x+1∈N, and every T⊆ℝ that contains 0 and is closed under x↦x+1 contains N.
- G2 — N⁺=N∖{0}; Z={0}∪N⁺∪{−n ∣ n∈N⁺}.
- G3 — −a denotes the additive inverse of a (a+(−a)=0); binary subtraction a−b is defined as a+(−b).
- G4 — Objects to decide or compute: −7, the decimal numeral '3.0', −2.5, −(−4), 5−8.


- \mathbb{Z} — the set of integers
- N,\ N^{+} — natural numbers (with 0) and positive naturals N∖{0}
- -a — the additive inverse of a (unary minus)
- a-b — binary subtraction, defined as a+(−b)
- T_3 — the inductive set {0,1,2}∪{x ∣ x≥3}





## Rules and sources


- add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
- add_comm · prerequisite — Commutativity of addition: u+v=v+u.
- add_zero · prerequisite — Additive identity: u+0=u.
- add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
- order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
- set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
- exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
- power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
- eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
- case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
- contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
- subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
- de_morgan_logic · prerequisite — De Morgan's laws for logic: ¬(P∧Q) ⇔ ¬P∨¬Q and ¬(P∨Q) ⇔ ¬P∧¬Q.
- quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
- forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
- eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
- eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
- forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- mko_int_def · cited — The integer set Z contains 0, every positive natural number, and its negative. The notation n∈Z states that n is an integer. · mko-integer
- nat_least_inductive · prerequisite — N is the smallest inductive subset of ℝ: 0∈N and x∈N ⇒ x+1∈N; if T⊆ℝ contains 0 and is closed under x↦x+1, then N⊆T.
- positional_def · prerequisite — Decimal numerals with a point: the digits d_i before the point contribute Σ d_i 10^i and the j-th digit e_j after the point contributes e_j 10^{−j}, added together; for example '3.0' denotes 3·10⁰+0·10⁻¹.
- L_N_T3 · lemma — Let T₃={0,1,2}∪{x∈ℝ ∣ x≥3}; then N⊆T₃.
- L_inv_unique · lemma — For reals a, x, y: if a+x=0 and a+y=0, then x=y (additive inverses are unique).





## Main derivation

S01 · definitionBefore

z\in\mathbb{Z}

After

z=0\ \lor\ z\in N^{+}\ \lor\ \exists n\in N^{+}:\ z=-n

Conditions: none

Rule: mko_int_def · Uses: G1, G2, mko_int_def

Leaf basis: mko_int_def + def_unfold + set_operations_def

By the MKO, Z consists of three parts: 0, the positive natural numbers, and the negatives of positive natural numbers. So deciding z∈Z means deciding whether at least one of three disjuncts holds. Here −n is the additive inverse of n, not the action 'subtract n' (G3).



S02 · impliesBefore

7=0+1+1+1+1+1+1+1

After

7\in N^{+},\ -7\in\mathbb{Z}

Conditions: none

Rule: exists_intro · Uses: S01, G1

Leaf basis: exists_intro + nat_least_inductive + set_operations_def + numeric_evaluation

7 is obtained from 0 by seven successor steps (N1), so applying the closure of G1 seven times gives 7∈N; 7≠0, so 7∈N⁺. Taking n=7, −7=−n, so the third disjunct holds and by ∃-introduction −7∈Z.



S03 · impliesBefore

\text{decimal numeral }3.0

After

3\cdot10^0+0\cdot10^{-1}=3\in N^{+}\subseteq\mathbb{Z}

Conditions: none

Rule: positional_def · Uses: S01, G4, positional_def

Leaf basis: positional_def + power_laws + numeric_evaluation + set_operations_def

The decimal numeral '3.0' denotes 3·10⁰+0·10⁻¹=3. 3 is obtained from 0 by three successor steps, so 3∈N and 3≠0, hence 3∈N⁺; the second disjunct holds and 3∈Z. The decimal point in the numeral does not change the value; integrality is decided by the number, not by how the numeral looks.



S04 · equivalentBefore

-2.5\in\mathbb{Z}

After

-2.5=0\ \lor\ -2.5\in N^{+}\ \lor\ \exists n\in N^{+}:\ -2.5=-n

Conditions: none

Rule: def_unfold · Uses: S01, G4

Leaf basis: def_unfold + mko_int_def

Unfold the membership condition of S01 for −2.5 (that is −5/2, N3). To prove −2.5∉Z, all three disjuncts must be excluded.



S05 · equivalentBefore

-2.5=-n

After

n=2.5

Conditions: none

Rule: eq_congruence · Uses: G3, eq_congruence

Leaf basis: eq_congruence + add_inverse + add_comm + add_assoc + add_zero

Add n+2.5 to both sides: the left side −2.5+(n+2.5)=n and the right side −n+(n+2.5)=2.5 (commutativity, associativity and inverses for addition), so n=2.5. Backward: if n=2.5, taking additive inverses of both sides gives −n=−2.5. So '−2.5 equals some −n' is exactly 'n=2.5'.



S06 · impliesBefore

T_3=\{0,1,2\}\cup\{x\in\mathbb{R}\mid x\ge 3\}

After

N\subseteq T_3

Conditions: none

Rule: L_N_T3 · Uses: G1, L_N_T3

Leaf basis: L_N_T3

By Lemma L_N_T3, every natural number is 0, 1 or 2, or else ≥3. So there is no natural number strictly between 2 and 3, and every natural number is ≥0. The lemma is proved in S06.1 and S06.2.



S07 · impliesBefore

N\subseteq T_3

After

2.5\notin N,\ -2.5\notin N

Conditions: none

Rule: contrapositive · Uses: S06, G4

Leaf basis: contrapositive + subset_def + order_basics + numeric_evaluation

2.5 differs from 0, 1 and 2, and 2.5<3, so 2.5∉T₃; −2.5<0 while every element of T₃ is ≥0, so −2.5∉T₃. Since N⊆T₃, the contrapositive gives 2.5∉N and −2.5∉N.



S08 · impliesBefore

\text{the three disjuncts of S04}

After

-2.5\notin\mathbb{Z}

Conditions: none

Rule: de_morgan_logic · Uses: S04, S05, S07

Leaf basis: de_morgan_logic + set_operations_def + quantifier_negation

First disjunct: −2.5≠0. Second: −2.5∉N, so it is not in N⁺⊆N either. Third: by S05 it amounts to '2.5∈N⁺', but 2.5∉N (S07). All three fail, so by De Morgan's law the disjunction is false, and by the equivalence S04, −2.5∉Z.



S09 · impliesBefore

(-a)+a=0,\ (-a)+(-(-a))=0

After

-(-a)=a\quad(a\in\mathbb{R})

Conditions: none

Rule: L_inv_unique · Uses: G3, L_inv_unique

Leaf basis: L_inv_unique + add_comm + add_inverse + forall_intro

For any real a: by commutativity (−a)+a=a+(−a)=0, so a is an additive inverse of −a; by definition −(−a) is also an additive inverse of −a. By Lemma L_inv_unique (with the lemma's a taken to be −a), −(−a)=a. a was arbitrary, so this holds for every real. The lemma is proved in S09.1 and S09.2.



S10 · impliesBefore

-(-4)

After

4\in N^{+}\subseteq\mathbb{Z}

Conditions: none

Rule: forall_elim · Uses: S09, S01

Leaf basis: forall_elim + numeric_evaluation + set_operations_def

Take a=4 in S09: −(−4)=4. Check: (−4)+4=0 (N8). 4 is obtained from 0 by four successor steps and 4≠0, so 4∈N⁺⊆Z; −4 itself is also an integer (third part, n=4).



S11 · impliesBefore

z\in\mathbb{Z}

After

-z\in\mathbb{Z}

Conditions: none

Rule: case_analysis · Uses: S01, S09

Leaf basis: case_analysis + L_inv_unique + forall_intro + exists_intro

Split into the three cases of S01. (i) z=0: 0+0=0, so 0 is an inverse of 0 and by uniqueness −0=0∈Z. (ii) z∈N⁺: with n=z, −z lies in the third part. (iii) z=−n with n∈N⁺: by S09, −z=−(−n)=n∈N⁺⊆Z. The three cases cover every element of Z, so −z∈Z for every integer z. This is a proof for an arbitrary z, not a generalization from a few examples.



S12 · impliesBefore

5-8=5+(-8)

After

5+(-8)=-3

Conditions: none

Rule: L_inv_unique · Uses: G3, L_inv_unique

Leaf basis: L_inv_unique + add_comm + add_assoc + add_inverse + numeric_evaluation

By G3, binary subtraction 5−8 is defined as 5+(−8). Compute 3+(5+(−8))=(3+5)+(−8)=8+(−8)=0 (associativity and inverses), and also 3+(−3)=0; by Lemma L_inv_unique (a=3), 5+(−8)=−3. Two kinds of '−' appear: in 5−8 it is a binary operation (subtraction), in −3 a unary sign (the inverse of 3); the result of the operation is the number −3, and −3∈Z (3∈N⁺).



S13 · impliesBefore

\text{S02, S03, S08, S10, S11, S12}

After

-7,\ 3,\ 4,\ -3\in\mathbb{Z};\ -2.5\notin\mathbb{Z};\ \forall z\in\mathbb{Z}:\ -z\in\mathbb{Z}

Conditions: none

Rule: and_intro_elim · Uses: S02, S03, S08, S10, S11, S12

Leaf basis: and_intro_elim

−7, 3 (written 3.0), −(−4)=4 and 5−8=−3 are integers; −2.5 is not; and Z is closed under negation.







## Substeps and lemmas

S06.1 · impliesBefore

0\in T_3;\ x\in\{0,1,2\}

After

x+1\in\{1,2,3\}\subseteq T_3

Conditions: none

Rule: case_analysis · Uses: G1, nat_least_inductive

Leaf basis: case_analysis + numeric_evaluation + order_basics

0∈T₃. For x=0, 1, 2, x+1 is 1, 2, 3 respectively; 1 and 2 are in {0,1,2} and 3≥3, so all lie in T₃.



S06.2 · impliesBefore

x\ge 3

After

x+1\ge 4\ge 3;\ T_3\ \text{inductive},\ N\subseteq T_3

Conditions: none

Rule: nat_least_inductive · Uses: S06.1, nat_least_inductive

Leaf basis: nat_least_inductive + case_analysis + order_basics

If x≥3 then x+1≥4≥3, so x+1∈T₃. Every element of T₃ is in {0,1,2} or is ≥3, and the two cases (S06.1 and here) cover them all, so T₃ is closed under x↦x+1; with 0∈T₃, T₃ is inductive. By the minimality in G1, N⊆T₃. S06.1 and S06.2 together prove Lemma L_N_T3.



S09.1 · impliesBefore

a+x=0,\ a+y=0

After

x=x+0=x+(a+y)=(x+a)+y

Conditions: none

Rule: add_assoc · Uses: add_zero, add_assoc

Leaf basis: add_zero + eq_replace + add_assoc

x=x+0 (additive identity) =x+(a+y) (replace 0 using the hypothesis a+y=0) =(x+a)+y (associativity).



S09.2 · impliesBefore

(x+a)+y

After

y,\ \text{hence}\ x=y

Conditions: none

Rule: add_comm · Uses: S09.1, add_comm

Leaf basis: add_comm + eq_replace + add_zero + eq_refl_symm_trans

(x+a)+y=(a+x)+y (commutativity) =0+y (replace using the hypothesis a+x=0) =y. Chaining with S09.1 gives x=y. S09.1 and S09.2 together prove Lemma L_inv_unique.







## Reverse audits


- S13 · sufficient_goal_reduction · S02, S03, S08, S09, S10, S11, S12 — The goal is the list in the goal field. Sufficient condition H: S02, S03, S08, S10, S11 and S12 each hold; H gives the goal by conjunction only. The universal statements (S09, S11) come from arguments about an arbitrary element; the goal is never used as a premise.
- S12 · premise_audit · L_inv_unique, add_assoc, add_inverse, numeric_evaluation — Applying uniqueness needs the two equations 3+x=0 and 3+y=0 with x=5+(−8) and y=−3; both are verified (N9, N11).
- S11 · premise_audit · S01, S09, case_analysis, L_inv_unique, forall_intro — The three cases must match the three disjuncts of S01; none may be left out.
- S10 · premise_audit · S09, forall_elim — This is an instance of the general result; conversely, the instance could not prove the general result.
- S09.2 · premise_audit · add_comm, eq_replace, add_zero, eq_refl_symm_trans — Each hypothesis, a+x=0 and a+y=0, is used once; transitivity of equality joins the two parts.
- S09.1 · premise_audit · add_zero, eq_replace, add_assoc — The hypothesis a+y=0 is used once, as a replacement.
- S09 · premise_audit · L_inv_unique, add_comm, forall_intro — The conclusion rests on uniqueness of inverses; it is not a memorized 'two minuses make a plus' but a consequence of uniqueness.
- S08 · premise_audit · S04, S05, S07, de_morgan_logic — All three must be excluded; saying '−2.5 is negative' is not enough, since −7 is negative too and is an integer.
- S07 · premise_audit · S06, contrapositive, subset_def, order_basics — The contrapositive is equivalent to the inclusion; it is not claimed that every element of T₃ is natural.
- S06.2 · premise_audit · S06.1, nat_least_inductive, case_analysis, order_basics — Minimality only needs T₃ to contain 0 and be closed under successor; T₃⊆N is not needed (indeed 3.5∈T₃ is not natural).
- S06.1 · premise_audit · case_analysis, numeric_evaluation — The three cases are checked one by one.
- S06 · premise_audit · L_N_T3 — This step only invokes the lemma; the proof is in the sub-steps.
- S05 · inverse_equivalence · eq_congruence, add_inverse, add_comm, add_assoc — Both directions apply the same defined operation to both sides of an equation.
- S04 · inverse_equivalence · S01, def_unfold — Unfolding a definition holds both ways.
- S03 · premise_audit · positional_def, S01, numeric_evaluation — What is needed is the number the numeral denotes; its appearance (whether it has a decimal point) cannot decide.
- S02 · premise_audit · S01, exists_intro, nat_least_inductive — Only one n∈N⁺ needs to be found; uniqueness is neither needed nor claimed.
- S01 · premise_audit · mko_int_def, G2, G3, def_unfold — This step only unfolds the definition; the three parts cover every member the MKO lists.





## Error controls and negative controls

The minus sign is not subtraction itselfOne misconception the MKO names is treating the minus sign as the subtraction operation itself. −3 is a number: the additive inverse of 3, with 3+(−3)=0; 5−8 is an operation, defined as 5+(−8), whose value is −3 (S12). −(−4)=4 is not a memorized rule either but a consequence of the uniqueness of inverses (S09).

A decimal point does not decide integralityAnother misconception the MKO names concerns numerals with a decimal point. '3.0' has a decimal point yet denotes the integer 3 (S03); '−2.5' denotes a number that is not an integer (S08). What decides is the number a numeral denotes and whether it falls in one of the three parts of Z, not how it is written.

Examples do not prove general lawsThe MKO warns against deriving all integer algebra laws from a few examples. Checking −(−4)=4 and −(−7)=7 (N12) does not prove −(−z)=z for all z; S09 proves it for an arbitrary real a, and S11 proves closure under negation by cases. Closure of Z under addition and multiplication is not proved here and needs its own claims.


- −2.5 is an integer, because it is negative and the integers include negatives → reject — The negative elements of Z are precisely the negatives of positive naturals; 2.5 is not natural (S07), so −2.5∉Z (S08).
- 3.0 is not an integer, because it is written with a decimal point → reject — '3.0' denotes 3, and 3∈N⁺⊆Z (S03).
- −3 denotes the operation 'subtract 3 from something' → reject — −3 is the number with 3+(−3)=0; it is 5−8 that is an operation, 5+(−8), whose value is −3 (S12).
- Since −(−4)=4 and −(−7)=7, −(−z)=z is proved for all integers → reject — Finitely many examples cannot prove a universal statement; the general proof is S09 (uniqueness of inverses).





## Result and limitations

With Z={0}∪N⁺∪{−n ∣ n∈N⁺}: −7∈Z; '3.0' denotes 3∈Z; since N⊆{0,1,2}∪{x ∣ x≥3}, neither 2.5 nor −2.5 is natural, so −2.5∉Z. Additive inverses are unique, so −(−a)=a, in particular −(−4)=4; −z∈Z for every z∈Z. 5−8 is the operation 5+(−8), whose value is the number −3∈Z.


- Closure of Z under addition and multiplication, and properties of order and divisibility, need their own claims and are not proved here (as the MKO says).
- nat_least_inductive is a premise (the formal reading of the natural-number MKO); in OCME's construction chain ℝ is built from ℚ, ℤ and N, and this guide uses ℝ only as the setting for membership questions.
- The semantic correspondence with Lean's Int construction, the embedding of naturals and negatives (MKO formal next) is not treated here.





## Verification and source binding

13 declared checks for this guide; only the listed expressions are covered.


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 02e167b67a0275433f107a2e6696fec332105d67efeeb4872a2ed6e36226c082
- original source SHA-256: 02e167b67a0275433f107a2e6696fec332105d67efeeb4872a2ed6e36226c082
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-integer-01.json)