Basic counting principles: how many three-digit even numbers have distinct digits

Goal and scope

Count the even integers from 100 to 999 whose three digits are pairwise distinct. Requirements: add only disjoint classes, and before each multiplication confirm that the number of options at every stage is the same for all earlier choices; when it is not, branch first.

Counts finite sets only (MKO assumption a1), using the addition principle for disjoint classes (a2) and the stage-by-stage multiplication principle (a3); the 'dependent' multiplication lemma used here is proved from basic facts of finite counting. It does not treat general inclusion-exclusion, permutation or combination formulas, or infinite sets, and does not change the canonical MKO or its English edition.

Givens and symbols

• finite_counting_basics
• cartesian_product_def
• injective_surjective_def
• set_operations_def
• numeric_evaluation

• G1 — A three-digit number is an integer n with 100≤n≤999; each such n has exactly one representation n=100d₁+10d₂+d₃ with d₁∈W⁺ and d₂,d₃∈W (see decimal_rep).
• G2 — The set to count is T={n∈ℤ ∣ 100≤n≤999, n is even, and the three digits of n are pairwise distinct}.
• G3 — Notation: [n]={k∈ℕ ∣ 1≤k≤n}; |S|=n means there is a bijection S→[n].

• T — the set of numbers to be counted
• d_1,d_2,d_3 — hundreds, tens and units digits
• W,\ W^{+} — W={0,1,2,3,4,5,6,7,8,9} and W⁺=W∖{0}
• E — the even digits {0,2,4,6,8}
• D,\ D_0,\ D_+ — the set of digit triples and its two classes
• [n] — the set {k∈ℕ ∣ 1≤k≤n}
• |S| — the number of elements of a finite set S

Rules and sources

• finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements.
• cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d.
• injective_surjective_def · prerequisite — Injective: f(a)=f(a′) ⇒ a=a′. Surjective: every b∈B has some a∈A with f(a)=b. Bijective: both; then there is a unique inverse f⁻¹ with f⁻¹∘f=id_A and f∘f⁻¹=id_B.
• 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.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• divides_def · prerequisite — Divisibility: for integers a, b, a∣b means there is an integer k with b=ak.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• 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.
• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• 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.
• 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.
• function_def · prerequisite — Function: f:A→B assigns to each a∈A exactly one f(a)∈B. Two functions are equal ⇔ they have the same domain and codomain and agree at every a.
• 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.
• mko_counting · cited — Counts of mutually exclusive choice classes are added. Counts of combinations across successive choice stages are multiplied when the options and conditions at every stage are explicit. · mko-counting-principle
• decimal_rep · prerequisite — Decimal representation: every integer n with 100≤n≤999 has exactly one digit triple (d₁,d₂,d₃) with n=100d₁+10d₂+d₃, d₁∈{1,2,3,4,5,6,7,8,9} and d₂,d₃∈{0,1,2,3,4,5,6,7,8,9}; conversely every such triple gives such an n.
• even_def · prerequisite — An integer n is even when 2∣n, that is, n=2k for some integer k.
• finite_subset · prerequisite — A subset of a finite set is finite.
• L_remove · lemma — If a finite set S has s elements and R⊆S has r elements, then |S∖R|=s−r.
• L_stage · lemma — Let a finite set X have m elements, and for each x∈X let the finite set Yₓ have exactly n elements (the number n is the same for every x, while the set Yₓ itself may depend on x). Then P={(x,y) ∣ x∈X, y∈Yₓ} has m·n elements.

Main derivation

T

|T|=|D|,\ D=\{(d_1,d_2,d_3)\mid d_1\in W^{+},\ d_2,d_3\in W,\ 100d_1+10d_2+d_3\ \text{even},\ d_1,d_2,d_3\ \text{pairwise distinct}\}

100d_1+10d_2+d_3\ \text{even}

d_3\in E=\{0,2,4,6,8\}

D

D=\{(d_1,d_2,d_3)\mid d_1\in W^{+},\ d_2\in W,\ d_3\in E,\ d_1\neq d_2,\ d_1\neq d_3,\ d_2\neq d_3\}

D

D=D_0\cup D_+,\ D_0\cap D_+=\varnothing,\ D_0=\{t\in D\mid d_3=0\},\ D_+=\{t\in D\mid d_3\in\{2,4,6,8\}\}

D=D_0\cup D_+,\ D_0\cap D_+=\varnothing

|D|=|D_0|+|D_+|

d_3=0

|W^{+}\setminus\{0\}|=9,\ \ |W\setminus\{0,d_1\}|=8\ \text{for every}\ d_1\in W^{+}

D_0

|D_0|=9\cdot 8=72

d_3\in\{2,4,6,8\}

|W^{+}\setminus\{d_3\}|=8,\ \ |W\setminus\{d_1,d_3\}|=8\ \text{for every}\ d_1\in W^{+}\setminus\{d_3\}

Q=\{(d_3,d_1)\mid d_3\in\{2,4,6,8\},\ d_1\in W^{+}\setminus\{d_3\}\}

|Q|=4\cdot 8=32

D_+

|D_+|=32\cdot 8=256

|D|=|D_0|+|D_+|

|D|=72+256=328

D=D'_{\mathrm{odd}}\cup D'_{\mathrm{even}}\ \text{(branch on}\ d_1)

|D|=5\cdot 5\cdot 8+4\cdot 4\cdot 8=200+128=328

|T|=|D|,\ |D|=328

|T|=328

Substeps and lemmas

R\subseteq S,\ |S|=s,\ |R|=r

|S\setminus R|=s-r

|X|=m,\ |Y_x|=n\ (x\in X)

\Phi:P\to X\times[n],\ \Phi(x,y)=(x,\varphi_x(y))

\Phi(x,y)=(x,\varphi_x(y))

\Phi\ \text{is a bijection}

\Phi:P\to X\times[n]\ \text{bijective}

|P|=|X\times[n]|=m\cdot n

Reverse audits

• S13 · sufficient_goal_reduction · S01, S11, eq_refl_symm_trans — Goal G: |T|=328. Sufficient condition H: a bijection between T and D, and |D|=328; H⇒G by transitivity of equality. H is proved forwards from the givens in S01 and S11, and G is never used as a premise; S12 is only an independent check.
• S12 · premise_audit · L_stage, L_remove, S05 — This is a second count with a different stage order, again branching before multiplying; its agreement with S11 adds confidence, while the conclusion is still derived by S01 to S11.
• S11 · inverse_equivalence · S07, S10, eq_replace — Replacement of equals and the exact sum (N8) hold in both directions.
• S10 · premise_audit · S08, S09, L_stage, finite_counting_basics — The 8 options at the third stage must hold for every pair (d₃,d₁); S08 proves this using d₁≠d₃. Reordering coordinates is a bijection, so the count is unchanged.
• S09 · premise_audit · S08, L_stage — The lemma's condition that every d₃ is followed by exactly 8 choices of d₁ is supplied by S08.
• S08 · premise_audit · L_remove, S04 — It needs d₃∈W⁺ (the removed digit really lies in W⁺) and d₁≠d₃ (the two removed digits differ). The first condition fails when d₃=0, which is exactly why S04 branches.
• S07.3 · premise_audit · S07.2, finite_counting_basics — If the Yₓ had different sizes there would be no common [n] and the product formula fails. Counterexample: X={a,b}, |Y_a|=1, |Y_b|=3 give |P|=4, which is neither 2·1 nor 2·3.
• S07.2 · premise_audit · S07.1, injective_surjective_def, cartesian_product_def — The two parts use the injectivity and surjectivity of φₓ respectively; nothing is claimed about maps other than Φ.
• S07.1 · premise_audit · G3, def_intro — This step only introduces notation; it relies on every Yₓ being matched with the same [n], that is, on each Yₓ having exactly n elements.
• S07 · premise_audit · S06, L_stage, finite_counting_basics — The lemma needs every Y_{d₁} to have the same size n; S06 proves n=8 for all d₁∈W⁺. Checking a single d₁ would not be enough.
• S06.1 · premise_audit · finite_counting_basics, subset_def, set_operations_def — R⊆S is needed. Counterexample: S={1,2} and R={2,3} give S∖R={1} with 1 element, but s−r=0.
• S06 · premise_audit · L_remove, S04 — The key condition is d₁≠0, which makes the removed set have 2 elements rather than 1; this is exactly the 'same number of options for every earlier choice' that a3 requires.
• S05 · premise_audit · S04, finite_counting_basics, finite_subset — The disjointness from S04 must be cited; if the classes overlapped (for example 'ends in 0' and 'starts with 2'), plain addition would count the intersection twice (see error control 1).
• S04 · premise_audit · S03, set_operations_def — Two things are needed: the classes cover all of D, and they do not overlap. The first prevents missing elements; the second prevents double counting in the addition of S05.
• S03 · inverse_equivalence · S02, set_extensionality — The conditions are equivalent item by item, so by extensionality the sets agree in both directions.
• S02 · inverse_equivalence · divides_def, even_def, distributive — Each direction exhibits its own integer k or j, so this is an equivalence; N1 checks the polynomial identity n−d₃=2(50d₁+5d₂).
• S01 · premise_audit · G1, decimal_rep, finite_counting_basics — It needs existence of the representation (the map is defined) and uniqueness (no number goes to two triples). Without uniqueness there could be more triples than numbers. The step claims only that the two sets have the same size.

Error controls and negative controls

Add directly only when the classes are disjoint

The first common mistake named by the MKO is adding cases that overlap. In T, 72 numbers end in 0 and 4·8=32 start with 2, but the two classes share the 8 numbers 210, 230, 240, 250, 260, 270, 280 and 290. Adding directly gives 104 and counts the overlap twice; the union really has 72+32−8=96 elements (MKO assumption a2: an overlap must be corrected separately). The classes of S04 are split by whether d₃ is 0, so they cannot overlap and S05 may add them directly.

Do not multiply blindly when the number of options depends on an earlier choice

The second mistake named by the MKO: 'units digit 5 ways, then hundreds 8 ways and tens 8 ways' gives 5·8·8=320. The claim 'hundreds 8 ways' holds only when the units digit is nonzero; when it is 0 the hundreds digit has 9 options. In the class d₃=0 alone the wrong count gives 1·8·8=64 instead of 72, exactly 8 too few, and 320+8=328. The correct method is the branching of S04, or the other branching of S12.

The order of stages may change, but each order must be rechecked

Choosing hundreds, then tens, then units and writing 9·8·5=360 assumes that 5 even digits always remain for the units place. If the hundreds or tens digit uses an even digit, fewer remain; for example d₁=2 and d₂=4 leave only 0, 6 and 8. Changing the order is not the error; the error is not checking that each stage has a fixed number of options. S12 branches on the parity of d₁ before multiplying.

• Units 5 ways, hundreds 8 ways, tens 8 ways, so |T|=5·8·8=320 → reject — When the units digit is 0 the hundreds digit has 9 options; the correct count is 328.
• Hundreds 9 ways, tens 8 ways, units 5 ways, so |T|=360 → reject — The number of even digits left for the units place depends on the first two digits; with d₁=2 and d₂=4 only 3 remain.
• The numbers in T that end in 0 or start with 2 number 72+32=104 → reject — The classes share 8 numbers (210, 230 and so on); the correct count is 96.
• The sizes of D₀ and D₊ were obtained by multiplying, so |D|=72·256 → reject — Disjoint classes are combined by addition; multiplication is for successive stages of one process.

Result and limitations

There are 328 even numbers from 100 to 999 with pairwise distinct digits: splitting by the units digit into two disjoint classes, 9·8=72 end in 0 and 4·8·8=256 end in 2, 4, 6 or 8. Branching instead on the parity of the hundreds digit also gives 200+128=328.

• N2 checks, at each integer from 100 to 999, that n has the same parity as its units digit; it is a finite check that covers exactly the 900 numbers used here, and the argument of S02 does not depend on it.
• Existence and uniqueness of the decimal representation (decimal_rep) is a premise of this guide; it is not derived here from the division algorithm.

Verification and source binding

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 7f8dccaca5069630be4159d5fe0095ba10e312d6050c11349077668b0fd09b5a
• original source SHA-256: 7f8dccaca5069630be4159d5fe0095ba10e312d6050c11349077668b0fd09b5a
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)