Proof of Comparison and Absolute Value Bounds for Finite Sums of Real Numbers

Sums are the finite sums of the field of real numbers, whose order $\le$ is that of an ordered field.

Claim 1. Let $c:[n]\to\mathbb{R}$ be the map with $c_k=b_k-a_k$. For each $k\in[n]$ the hypothesis $a_k\le b_k$ and claim 3 of Elementary Arithmetic in an Ordered Field give $0\le c_k$, so claim 5 of Properties of Finite Sums gives

By commutativity and associativity of addition in the field $\mathbb{R}$ together with claims 3 and 4 of Additive Cancellation and Elementary Additive Identities in a Field, $a_k+c_k=b_k+(a_k-a_k)=b_k+0=b_k$ for every $k\in[n]$, so claim 2 of Properties of Finite Sums gives

Hence $\sum_{k=1}^{n}b_k-\sum_{k=1}^{n}a_k=\sum_{k=1}^{n}c_k$, and this is nonnegative, so claim 3 of Elementary Arithmetic in an Ordered Field yields claim 1.

Claim 2. First, $0\,t=0$ for every $t\in\mathbb{R}$: indeed $0\,t=(0+0)\,t=0\,t+0\,t$ by distributivity, and claim 2 of Additive Cancellation and Elementary Additive Identities in a Field applies. Consequently $t+(-1)\,t=(1+(-1))\,t=0\,t=0$, so $(-1)\,t=-t$ by claim 1 of Additive Cancellation and Elementary Additive Identities in a Field.

By claim 3 of Properties of the Absolute Value in an Ordered Field we have $a_k\le|a_k|$ and $-|a_k|\le a_k$ for every $k\in[n]$. Applying claim 1 above to the families $a$ and $k\mapsto|a_k|$ gives

Applying claim 1 above to the families $k\mapsto-|a_k|$ and $a$, and evaluating the left-hand sum by claim 3 of Properties of Finite Sums with $\lambda=-1$ together with the identity $(-1)\,t=-t$ just established, gives

The two displayed bounds and claim 6 of Properties of the Absolute Value in an Ordered Field give claim 2.