Skip to content
Axiomatic Wiki
Lemma·L11

Multiplication from the left

Zero times anything is zero; a successor on the left adds one copy.

for all .
In words
Multiplying zero by anything gives zero, and multiplying a successor by n gives the original product plus n, for all natural numbers m and n: the mirror images of the defining equations of multiplication.
Rests onF02F09F14A01A06
Never needed: F03 · F04 · F05 · F06 · F08 · F10 · F11 · F12 · F13 · A02 · A03 · A04 · A05 · A07 · A08 (computed from the citation graph, not asserted).

Proof

  1. 1
    Claim A: . Induction on (T05, Separation). Base: by D028. Step: , using D028, the hypothesis, and from D027.
  2. 2
    Claim B: . Fix , induct on . Base: and by D028 and D027.
  3. 3
    Step of Claim B: assume . Then by D028 and the hypothesis. Regroup with associativity: , and by D027 and commutativity. Hence , using L08 again and D028; this is the claim at .
  4. 4
    T05 closes both inductions.
∎

Remarks

Multiplication recurses on its right argument; these are the matching equations for the left argument, and the workhorses behind commutativity and the counting step of L27 and the division algorithm.
Wikipedia ↗Nat.succ_mul ↗

Used by

L12L19L20L27L46T10T23
Propose an edit1 published revision