# Arithmetic operations: whether the same inputs give a defined result in ℕ, ℤ and ℚ

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

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-arithmetic-operations-01 · production-20261019-adopted-96



## Goal and scope

Take a=3 and b=5. In each of the number systems ℕ (including 0), ℤ and ℚ, decide whether a+b, a·b, a−b and a÷b are defined; when they are, compute the result and decide which systems it belongs to. Then decide whether 3÷0 and 0÷0 are defined in these three systems.

Treats only the three stated systems ℕ⊂ℤ⊂ℚ and one stated pair of inputs; difference and quotient are defined by the equations b+c=a and b·q=a having exactly one solution in the system (G2). It illustrates the MKO's point that whether an operation is defined, and whether its result stays in the original system, must be stated together with the system and the division-by-zero boundary. It does not construct these systems, does not treat other operations such as truncated subtraction or division with remainder, and does not change the canonical MKO or its English edition.





## Givens and symbols


- order_basics
- add_inverse
- mul_inverse_nonzero
- mul_zero
- numeric_evaluation


- G1 — Number systems: ℕ={n∈ℤ ∣ n≥0} and ℕ⊂ℤ⊂ℚ; the three share one addition, one multiplication and one order (those of ℚ restricted to ℤ and ℕ).
- G2 — Difference and quotient: let S be one of these systems and a,b∈S. If exactly one c∈S satisfies b+c=a, then a−b is defined in S and a−b=c; if exactly one q∈S satisfies b·q=a, then a÷b is defined in S and a÷b=q. If there is no such element, or more than one, the operation is undefined in S for these inputs.
- G3 — Inputs: a=3 and b=5; in addition, the two inputs with divisor zero, (3,0) and (0,0).


- \mathbb{N} — the set of nonnegative integers 0, 1, 2 and so on
- \mathbb{Z},\ \mathbb{Q} — the integers and the rationals
- a-b — the unique c in the stated system with b+c=a
- a\div b — the unique q in the stated system with b·q=a
- \tfrac{1}{u} — the reciprocal of a nonzero rational u





## Rules and sources


- 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.
- add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
- mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
- mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
- add_zero · prerequisite — Additive identity: u+0=u.
- quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
- 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.
- 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.
- add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
- add_comm · prerequisite — Commutativity of addition: u+v=v+u.
- 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.
- 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.
- mul_one · prerequisite — Multiplicative identity: 1·u=u.
- mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
- mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
- contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- mko_arith · cited — Each arithmetic operation forms a result from two inputs. Whether the operation is defined and whether the result remains in the original number system must be stated together with boundaries such as division by zero. · mko-arithmetic-operations
- nat_closed · prerequisite — ℕ is closed under addition and multiplication: if m,n∈ℕ then m+n∈ℕ and m·n∈ℕ (sums and products of nonnegative integers are nonnegative integers).
- int_no_gap · prerequisite — No gaps in the integers: for integers k and m, k≤m or k≥m+1; in particular no integer lies strictly between m and m+1.
- L_sub · lemma — In ℤ or in ℚ, for a, b, c in that system: b+c=a ⇔ c=a+(−b).
- L_div · lemma — In ℚ, for a,q∈ℚ and b≠0: b·q=a ⇔ q=a·(1/b).





## Main derivation

S01 · definitionBefore

a,b\ \text{and an operation, system not yet stated}

After

S\in\{\mathbb{N},\mathbb{Z},\mathbb{Q}\};\ a-b=c\iff b+c=a\ (\text{unique }c\in S);\ a\div b=q\iff bq=a\ (\text{unique }q\in S)

Conditions: none

Rule: mko_arith · Uses: G1, G2

Leaf basis: mko_arith + def_intro

The MKO requires operations to be specified together with the number system and the division-by-zero boundary, so these are fixed first: the three systems ℕ⊂ℤ⊂ℚ share one addition and one multiplication (G1); subtraction and division are defined by solving equations: a−b is the unique c with b+c=a, and a÷b is the unique q with b·q=a, where the solution must lie in the system S under discussion (G2). From here on 'defined' always has this meaning.



S02 · impliesBefore

3,5\in\mathbb{N}

After

3+5=8\in\mathbb{N},\quad 3\cdot 5=15\in\mathbb{N}

Conditions: 3\ge 0; 5\ge 0

Rule: nat_closed · Uses: G1, G3, nat_closed

Leaf basis: nat_closed + numeric_evaluation

3 and 5 are nonnegative integers, so they lie in ℕ. By nat_closed their sum and product stay in ℕ; computing gives 3+5=8 and 3·5=15, both ≥0. Addition and multiplication are defined in ℕ for these inputs and the results stay in ℕ. Since the three systems share one set of operations (G1), the sum and product in ℤ and ℚ are also 8 and 15.



S03 · impliesBefore

c\in\mathbb{N}

After

5+c\ge 5

Conditions: c\ge 0

Rule: order_basics · Uses: G1

Leaf basis: order_basics + add_zero

To decide whether 3−5 is defined in ℕ, first see which values 5+c can take for c in ℕ. Take any c∈ℕ, so c≥0. If c>0, order_basics (u<v gives u+w<v+w, with u=0, v=c, w=5) gives 5+0<5+c; if c=0 then 5+c=5. In both cases 5+c≥5+0=5.



S04 · impliesBefore

\forall c\in\mathbb{N}:\ 5+c\ge 5>3

After

\neg\exists c\in\mathbb{N}:\ 5+c=3

Conditions: none

Rule: quantifier_negation · Uses: S03

Leaf basis: quantifier_negation + order_basics

By S03 every c∈ℕ has 5+c≥5, and 5>3, so by transitivity of order 5+c>3; by trichotomy 5+c>3 rules out 5+c=3. So 5+c≠3 for every c∈ℕ, which by negation of quantifiers is the same as 'there is no c∈ℕ with 5+c=3'.



S05 · impliesBefore

\neg\exists c\in\mathbb{N}:\ 5+c=3

After

3-5\ \text{is undefined in}\ \mathbb{N}

Conditions: none

Rule: def_unfold · Uses: S04, G2

Leaf basis: def_unfold

By G2, 3−5 is defined in ℕ only if exactly one c∈ℕ satisfies 5+c=3; S04 says there is none at all, so 3−5 is undefined in ℕ. This shows that ℕ is not closed under subtraction.



S06 · equivalentBefore

5+c=3,\ c\in\mathbb{Z}

After

c=3+(-5)=-2

Conditions: none

Rule: L_sub · Uses: G1, G3

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

In ℤ, by Lemma L_sub (a=3, b=5): 5+c=3 ⇔ c=3+(−5), and 3+(−5)=−2. So in ℤ the equation 5+c=3 has exactly one solution, c=−2. The same argument works in ℚ, where the only solution is also −2.



S07 · impliesBefore

c=-2\ \text{is the only solution in}\ \mathbb{Z}

After

3-5=-2\ \text{in}\ \mathbb{Z},\quad -2\notin\mathbb{N}

Conditions: -2<0

Rule: def_unfold · Uses: S06, G1, G2

Leaf basis: def_unfold + order_basics

S06 gives exactly one solution in ℤ, so by G2, 3−5 is defined in ℤ (and in ℚ) and equals −2. Also −2<0, so by ℕ={n∈ℤ ∣ n≥0} in G1, −2∉ℕ. This agrees with S05: the only solution in ℤ is not in ℕ, so ℕ has none. The same inputs get a different verdict in a different system.



S08 · case_splitBefore

q\in\mathbb{Z}\ \text{with}\ 5q=3\ ?

After

q\le 0\ \lor\ q\ge 1

Conditions: q\in\mathbb{Z}

Rule: int_no_gap · Uses: G1, G2

Leaf basis: int_no_gap + case_analysis

To decide whether 3÷5 is defined in ℤ, ask whether some integer q has 5q=3. By int_no_gap (m=0), every integer q satisfies q≤0 or q≥1; the two cases cover all integers and are handled in S08.1 and S08.2.



S09 · impliesBefore

q\le 0\Rightarrow 5q\neq 3,\quad q\ge 1\Rightarrow 5q\neq 3

After

\neg\exists q\in\mathbb{Z}:\ 5q=3;\ 3\div 5\ \text{undefined in}\ \mathbb{Z}\ \text{and in}\ \mathbb{N}

Conditions: none

Rule: case_analysis · Uses: S08, S08.1, S08.2, G1, G2

Leaf basis: case_analysis + quantifier_negation + def_unfold

Both cases give 5q≠3, so by proof by cases every integer q has 5q≠3: there is no solution in ℤ, and by G2, 3÷5 is undefined in ℤ. Since ℕ⊂ℤ with the same operations, a solution in ℕ would also be a solution in ℤ, so 3÷5 is undefined in ℕ as well. ℤ is not closed under division.



S10 · equivalentBefore

5q=3,\ q\in\mathbb{Q}

After

q=3\cdot\tfrac{1}{5}=\tfrac{3}{5}

Conditions: 5\neq 0

Rule: L_div · Uses: G1, G3

Leaf basis: eq_congruence + mul_inverse_nonzero + mul_assoc + mul_comm + mul_one + numeric_evaluation

In ℚ, by Lemma L_div (a=3, b=5, with 5≠0): 5q=3 ⇔ q=3·(1/5)=3/5. So in ℚ the equation 5q=3 has exactly one solution.



S11 · impliesBefore

q=\tfrac{3}{5}\ \text{is the only solution in}\ \mathbb{Q}

After

3\div 5=\tfrac{3}{5}\ \text{in}\ \mathbb{Q},\quad 0<\tfrac{3}{5}<1,\ \tfrac{3}{5}\notin\mathbb{Z}

Conditions: none

Rule: def_unfold · Uses: S10, G2, int_no_gap

Leaf basis: def_unfold + int_no_gap + order_basics + numeric_evaluation

By G2 and S10, 3÷5 is defined in ℚ and equals 3/5. Also 1/5>0 (because 5>0), and multiplying 0<3<5 by 1/5 gives 0<3/5<1; by int_no_gap no integer lies strictly between 0 and 1, so 3/5∉ℤ. This agrees with S09: the only solution in ℚ is not an integer.



S12 · impliesBefore

q\in\mathbb{Q}

After

0\cdot q=0

Conditions: none

Rule: mul_zero · Uses: G1

Leaf basis: mul_zero + mul_comm

Turn to division with a divisor equal to zero. By mul_zero, q·0=0, and by commutativity 0·q=q·0=0. This holds for every q∈ℚ, hence also for q in ℤ or ℕ.



S13 · impliesBefore

\forall q\in\mathbb{Q}:\ 0\cdot q=0\neq 3

After

\neg\exists q\in\mathbb{Q}:\ 0\cdot q=3;\ 3\div 0\ \text{undefined in}\ \mathbb{Q},\mathbb{Z},\mathbb{N}

Conditions: none

Rule: contradiction · Uses: S12, G1, G2

Leaf basis: contradiction + mul_zero + numeric_evaluation

If some q∈ℚ had 0·q=3, then S12 would give 3=0·q=0, contradicting 3≠0. So no q∈ℚ satisfies 0·q=3, and by G2, 3÷0 is undefined in ℚ; a solution in ℤ or ℕ would also be one in ℚ, so 3÷0 is undefined in all three systems. This is division by zero of the 'no candidate' kind.



S14 · impliesBefore

\forall q:\ 0\cdot q=0

After

0\cdot 0=0,\ 0\cdot 1=0,\ 0\neq 1;\ 0\div 0\ \text{undefined in}\ \mathbb{N},\mathbb{Z},\mathbb{Q}

Conditions: none

Rule: def_unfold · Uses: S12, G2

Leaf basis: def_unfold + mul_zero

By S12 every q satisfies 0·q=0, for example q=0 and q=1; both lie in ℕ (hence in ℤ and ℚ), and 0≠1. So in each system the equation 0·q=0 has more than one solution; G2 requires exactly one, so 0÷0 is undefined in all three systems. This is division by zero of the 'too many candidates' kind.



S15 · impliesBefore

\text{verdicts of S02, S05, S07, S09, S11, S13, S14}

After

3+5=8,\ 3\cdot 5=15\ (\mathbb{N});\ 3-5=-2\ (\mathbb{Z});\ 3\div 5=\tfrac{3}{5}\ (\mathbb{Q});\ 3\div 0,\ 0\div 0\ \text{undefined}

Conditions: none

Rule: and_intro_elim · Uses: S02, S05, S07, S09, S11, S13, S14

Leaf basis: and_intro_elim

Put the conclusions together: in ℕ, 3+5=8 and 3·5=15 are defined while 3−5 and 3÷5 are not; in ℤ, 3−5=−2 is defined while 3÷5 still is not; in ℚ, 3÷5=3/5 is defined; 3÷0 and 0÷0 are undefined in all three systems.







## Substeps and lemmas

S06.1 · equivalentBefore

b+c=a

After

(-b)+(b+c)=(-b)+a

Conditions: none

Rule: eq_congruence · Uses: eq_congruence, add_inverse

Leaf basis: eq_congruence + add_inverse

In ℤ (or ℚ) every b has a −b; add −b on the left of both sides. The backward move is to add b to both sides and simplify as in S06.2.



S06.2 · equivalentBefore

(-b)+(b+c)=(-b)+a

After

c=a+(-b)

Conditions: none

Rule: eq_replace · Uses: S06.1

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

Simplify the left side: (−b)+(b+c)=((−b)+b)+c=0+c=c (associativity, inverses, commutativity and identity for addition); on the right, commutativity gives (−b)+a=a+(−b). S06.1 and S06.2 together prove Lemma L_sub.



S08.1 · impliesBefore

q\le 0

After

5q\le 0<3,\ \text{so}\ 5q\neq 3

Conditions: 5>0

Rule: order_basics · Uses: S08

Leaf basis: order_basics + mul_zero

If q<0, multiplying by the positive number 5 preserves order, so 5q<5·0=0; if q=0 then 5q=0. So 5q≤0<3, and therefore 5q≠3.



S08.2 · impliesBefore

q\ge 1

After

5q\ge 5>3,\ \text{so}\ 5q\neq 3

Conditions: 5>0

Rule: order_basics · Uses: S08

Leaf basis: order_basics + mul_one

If q>1, multiplying by 5>0 gives 5q>5·1=5; if q=1 then 5q=5. So 5q≥5>3, and therefore 5q≠3.



S10.1 · equivalentBefore

bq=a

After

\tfrac{1}{b}(bq)=\tfrac{1}{b}a

Conditions: b\neq 0

Rule: mul_inverse_nonzero · Uses: eq_congruence, mul_inverse_nonzero

Leaf basis: eq_congruence + mul_inverse_nonzero

Since b≠0 the reciprocal 1/b exists; multiply both sides by 1/b. The backward move is to multiply both sides by b and simplify as in S10.2. If b=0 there is no 1/b and the step cannot be taken.



S10.2 · equivalentBefore

\tfrac{1}{b}(bq)=\tfrac{1}{b}a

After

q=a\cdot\tfrac{1}{b}

Conditions: b\neq 0

Rule: eq_replace · Uses: S10.1

Leaf basis: mul_assoc + mul_comm + mul_one + mul_inverse_nonzero + eq_replace

Simplify the left side: (1/b)(bq)=((1/b)b)q=1·q=q (associativity, reciprocal, identity); on the right, commutativity gives (1/b)a=a·(1/b). S10.1 and S10.2 together prove Lemma L_div.







## Reverse audits


- S15 · sufficient_goal_reduction · S02, S05, S07, S09, S11, S13, S14, and_intro_elim — Goal G: a verdict for each system and each operation. Sufficient condition H: the conclusions of S02, S05, S07, S09, S11, S13 and S14; H⇒G just lists them together. H is proved forwards from G1 to G3; G is never used as a premise.
- S14 · premise_audit · S12, G2, def_unfold — Two distinct solutions are enough to defeat uniqueness; no particular value of 0÷0 is claimed.
- S13 · premise_audit · S12, contradiction, G2 — The contradiction depends only on S12 holding for all q and on 3≠0; the conclusion is non-existence, not 'the result is 0' and not 'the result is infinity'.
- S12 · premise_audit · mul_zero, mul_comm — mul_zero holds for every q (its reason is in the glossary); this step uses no extra assumption about q.
- S11 · premise_audit · S10, G2, int_no_gap, order_basics — It needs existence and uniqueness from S10 and 0<3/5<1; it says only that this quotient is defined in ℚ, not that every division in ℚ is defined (see S13 and S14).
- S10.2 · inverse_equivalence · mul_assoc, mul_comm, mul_one, mul_inverse_nonzero — Expressions are only replaced by equal ones, so the step is two-way; (1/b)b=1 needs b≠0.
- S10.1 · inverse_equivalence · eq_congruence, mul_inverse_nonzero — Multiplying by 1/b and multiplying by b undo each other, given exactly b≠0.
- S10 · inverse_equivalence · L_div, numeric_evaluation — Backward: substitute, 5·(3/5)=3. The lemma's hypothesis 5≠0 holds and both directions are proved, so the solution exists and is unique.
- S09 · premise_audit · S08, S08.1, S08.2, case_analysis, G2 — It needs the two cases to cover all integers (S08); checking a few values of q would not show that there is no solution.
- S08.2 · premise_audit · order_basics, mul_one — As in S08.1, 5>0 is used; no converse is claimed.
- S08.1 · premise_audit · order_basics, mul_zero — 5>0 is what keeps the direction of the inequality; only 5q≠3 is concluded and no converse is claimed.
- S08 · premise_audit · G1, int_no_gap — The case split needs the two branches to cover every integer; this depends on q being an integer and fails for a rational q such as 3/5.
- S07 · premise_audit · S06, G1, G2, order_basics — It needs existence and uniqueness from S06 and the definition of ℕ; it does not claim that ℤ is closed under every operation (division in S09 is not).
- S06.2 · inverse_equivalence · add_assoc, add_comm, add_inverse, add_zero — Expressions are only replaced by equal ones, which does not change whether the equation holds, so the step is two-way.
- S06.1 · inverse_equivalence · eq_congruence, add_inverse — Adding −b and adding b undo each other, with no side condition in ℤ or ℚ. In ℕ, −b is in general not in ℕ, so the step cannot be carried out inside ℕ, which is exactly the situation of S05.
- S06 · inverse_equivalence · L_sub, numeric_evaluation — Backward: substitute, 5+(−2)=3. Both directions of the lemma are proved in the sub-steps, so 'is a solution' and 'equals −2' are equivalent, which gives both existence and uniqueness.
- S05 · premise_audit · S04, G2, def_unfold — The definition requires a solution that exists and is unique; non-existence already settles that it is undefined. The conclusion is for ℕ only; ℤ is treated separately in S06 and S07.
- S04 · premise_audit · S03, order_basics, quantifier_negation — What is needed is an inequality for every c in ℕ, not a few trial values; S03 was proved for an arbitrary c, so the conclusion covers all c∈ℕ.
- S03 · premise_audit · G1, order_basics, add_zero — Only c≥0 and the fact that adding preserves order are used; c is arbitrary with no other assumption. The converse (recovering c∈ℕ from 5+c≥5) is neither needed nor claimed.
- S02 · premise_audit · G1, G3, nat_closed, numeric_evaluation — It needs 3,5∈ℕ and the closure of ℕ under addition and multiplication; closure is claimed for these two operations only, not for subtraction or division (see S05 and S09).
- S01 · premise_audit · G1, G2, mko_arith — This step only fixes the systems and the definitions and derives no new fact; every later conclusion is relative to a stated S.





## Error controls and negative controls

Closure depends on the number systemThe MKO names the common mistake of believing the four operations are closed in every number system without conditions. Here ℕ is closed under addition and multiplication (S02), but 3−5 is undefined in ℕ (S05); ℤ supplies subtraction (S07), but 3÷5 is still undefined in ℤ (S09); in ℚ, 3÷5=3/5 (S11), but division by zero is still excluded (S13, S14). Saying that an operation is defined always requires naming the system.

Division by zero is not an ordinary divisionAnother mistake identified in the MKO is treating division by zero as an ordinary quotient. By G2, a÷b is the unique solution of b·q=a. When b=0, 0·q is always 0: if a≠0 (as in 3÷0) there is no candidate (S13); if a=0 (0÷0) every number is a candidate (S14). Neither case gives a result. '3÷0=0' fails on substitution, 0·0=0≠3; '0÷0=1' does satisfy 0·1=0, but so does q=0, so uniqueness fails.

Division with remainder is not exact divisionThe MKO notes that 3÷2 is not an exact division in the natural numbers. Likewise, division with remainder gives 3=5·0+3 (quotient 0, remainder 3), but that is a different operation: 3÷5 in the sense of G2 requires 5q=3 exactly, and 5·0=0≠3. Taking the quotient 0 from division with remainder as the value of 3÷5 in ℕ silently changes the operation.


- In ℕ, 3−5=0 → reject — Substituting back gives 5+0=5≠3; truncated subtraction, which replaces a negative difference by 0, is a different operation, not the subtraction of G2.
- 3÷0=0 → reject — Substituting back gives 0·0=0≠3; by S13 every q has 0·q=0≠3, so there is no candidate.
- 0÷0=1, because any number divided by itself is 1 → reject — u÷u=1 needs u≠0; 0·q=0 holds for every q, so q=0 and q=1 are both solutions and the solution is not unique (S14).
- 6÷3=2 is an integer, so ℤ is closed under division → reject — One example cannot prove closure; 3÷5 is undefined in ℤ (S09), and one counterexample is enough to refute closure.





## Result and limitations

In ℕ, 3+5=8 and 3·5=15 are defined (with the same values in ℤ and ℚ); 3−5 and 3÷5 are undefined in ℕ. In ℤ (and in ℚ), 3−5=−2, but −2∉ℕ; 3÷5 is undefined in ℤ and equals 3/5 in ℚ, while 3/5∉ℤ. 3÷0 has no candidate value and 0÷0 has no unique one, so both are undefined in ℕ, ℤ and ℚ.


- This guide takes the operations and order properties of ℕ, ℤ and ℚ (nat_closed, int_no_gap, order_basics and the like) as premises and does not construct these systems.
- G2 is one common convention that defines difference and quotient by unique solutions; truncated subtraction, division with remainder, or a programming language's special convention for a÷0 are different operations and need their own definitions.





## Verification and source binding

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: ef166229ecdb3b0f44715ad7924ab80f5ce26775fb834d7df17af4dbc883ea69
- original source SHA-256: ef166229ecdb3b0f44715ad7924ab80f5ce26775fb834d7df17af4dbc883ea69
- 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-arithmetic-operations-01.json)