Proof of Properties of Finite Products

Throughout, $\pi$ denotes the map supplied by Existence and Uniqueness of Iterates of a Binary Operation for the multiplication of $K$ and the family $a$, so that $\prod_{k=1}^{j}a_{k}=\pi(j)$ by Finite Product Notation in a Field. Elementary order facts about $\mathbb{N}$, such as transitivity and totality of $\le$, that $[j]\subseteq[n]$ when $j\in[n]$, and that $S(j)\in[n]$ implies $j\in[n]$, are those recorded in Properties of the Order on the Natural Numbers.

Claims 2 to 5 are proved by induction, using the induction principle for the natural numbers: in each case we let $\mathcal{P}$ be the set of natural numbers $j$ such that the assertion in question holds for $j$ whenever $j\in[n]$, verify $1\in\mathcal{P}$ and that $j\in\mathcal{P}$ implies $S(j)\in\mathcal{P}$, and then specialise to $j=n$.

Claim 1. The two recursion identities are the defining properties of $\pi$ recorded in Finite Product Notation in a Field. For the restriction statement, let $\pi'$ be the map supplied by Existence and Uniqueness of Iterates of a Binary Operation for the family $a'$ on $[j]$. Since $[j]\subseteq[n]$ and $a$ agrees with $a'$ on $[j]$, the restriction of $\pi$ to $[j]$ satisfies $\pi(1)=a_{1}=a'_{1}$ and $\pi(S(m))=\pi(m)\,a_{S(m)}=\pi(m)\,a'_{S(m)}$ whenever $S(m)\in[j]$. By the uniqueness assertion of Existence and Uniqueness of Iterates of a Binary Operation, this restriction equals $\pi'$, which is the stated identity.

Claim 2. For $j=1$ both sides equal $a_{1}b_{1}$ by claim 1. Suppose the identity holds for $j$ and let $S(j)\in[n]$. By claim 1 and the induction hypothesis,

and by commutativity and associativity of the multiplication of $K$ the right-hand side equals

Claim 3. We prove by induction on $j$ that, for $j\in[n]$, the product $\prod_{k=1}^{j}a_{k}$ equals $a_{i}$ if $i\le j$ and equals $1$ if $j<i$; exactly one of these two cases occurs, since $\le$ is total on $\mathbb{N}$.

For $j=1$: if $i=1$ the product is $a_{1}=a_{i}$ by claim 1; if $1<i$ then $a_{1}=1$ by hypothesis and the product is $1$. Suppose the assertion holds for $j$ and let $S(j)\in[n]$. If $S(j)<i$ then $j<i$, so $\prod_{k=1}^{j}a_{k}=1$, and $a_{S(j)}=1$, whence $\prod_{k=1}^{S(j)}a_{k}=1$. If $S(j)=i$ then $j<i$, so $\prod_{k=1}^{j}a_{k}=1$ and $\prod_{k=1}^{S(j)}a_{k}=a_{S(j)}=a_{i}$. If $i<S(j)$ then $i\le j$, so $\prod_{k=1}^{j}a_{k}=a_{i}$, and $a_{S(j)}=1$, whence $\prod_{k=1}^{S(j)}a_{k}=a_{i}$. Taking $j=n$ and using $i\le n$ gives claim 3.

Claim 4. Suppose first that $a_{i}=0$ for some $i\in[n]$. We show by induction on $j$ that $\prod_{k=1}^{j}a_{k}=0$ whenever $j\in[n]$ and $i\le j$. If $j=1$ then $i=1$ and the product is $a_{1}=0$. Suppose the assertion holds for $j$, let $S(j)\in[n]$ and let $i\le S(j)$. If $i\le j$ then $\prod_{k=1}^{j}a_{k}=0$ and $\prod_{k=1}^{S(j)}a_{k}=0\,a_{S(j)}=0$ by Zero Products and Elementary Identities in a Field; otherwise $i=S(j)$ and $\prod_{k=1}^{S(j)}a_{k}=\bigl(\prod_{k=1}^{j}a_{k}\bigr)0=0$ by the same lemma. Taking $j=n$ gives $\prod_{k=1}^{n}a_{k}=0$.

Conversely suppose $a_{k}\ne0$ for every $k\in[n]$. We show by induction on $j$ that $\prod_{k=1}^{j}a_{k}\ne0$ for $j\in[n]$. For $j=1$ the product is $a_{1}\ne0$. If $\prod_{k=1}^{j}a_{k}\ne0$ and $S(j)\in[n]$, then $\prod_{k=1}^{S(j)}a_{k}=\bigl(\prod_{k=1}^{j}a_{k}\bigr)a_{S(j)}$ is a product of two nonzero elements of a field, hence nonzero by Zero Products and Elementary Identities in a Field. Taking $j=n$ proves the contrapositive of the remaining implication.

Claim 5. For the first assertion, induct on $j$. For $j=1$ the product is $a_{1}$ and $0\le a_{1}$ by hypothesis. Suppose $0\le\prod_{k=1}^{j}a_{k}$ and let $S(j)\in[n]$. Applying claim 5 of Elementary Arithmetic in an Ordered Field to the inequality $0\le a_{S(j)}$ with the nonnegative factor $\prod_{k=1}^{j}a_{k}$, and using $t\,0=0$ from Zero Products and Elementary Identities in a Field together with commutativity of multiplication, gives $0\le\bigl(\prod_{k=1}^{j}a_{k}\bigr)a_{S(j)}=\prod_{k=1}^{S(j)}a_{k}$.

For the second assertion, note first that $0\le b_{k}$ for every $k\in[n]$ by transitivity of $\le$, so the first assertion applies to $b$ as well. Induct on $j$. For $j=1$ the assertion is the hypothesis $a_{1}\le b_{1}$. Suppose $\prod_{k=1}^{j}a_{k}\le\prod_{k=1}^{j}b_{k}$ and let $S(j)\in[n]$. By claim 5 of Elementary Arithmetic in an Ordered Field, applied first with the nonnegative factor $a_{S(j)}$ and then with the nonnegative factor $\prod_{k=1}^{j}b_{k}$, and using commutativity of multiplication,

By transitivity of $\le$ and claim 1 this is $\prod_{k=1}^{S(j)}a_{k}\le\prod_{k=1}^{S(j)}b_{k}$.