Sums are the finite sums of the field of real numbers, whose order β€ is that of an ordered field.
Claim 1. Let c:[n]βR be the map with ckβ=bkββakβ. For each kβ[n] the hypothesis akββ€bkβ and claim 3 of Elementary Arithmetic in an Ordered Field give 0β€ckβ, so claim 5 of Properties of Finite Sums gives
0β€k=1βnβckβ.
By commutativity and associativity of addition in the field R together with claims 3 and 4 of Additive Cancellation and Elementary Additive Identities in a Field, akβ+ckβ=bkβ+(akββakβ)=bkβ+0=bkβ for every kβ[n], so claim 2 of Properties of Finite Sums gives
k=1βnβbkβ=k=1βnβakβ+k=1βnβckβ.
Hence βk=1nβbkβββk=1nβakβ=βk=1nβckβ, and this is nonnegative, so claim 3 of Elementary Arithmetic in an Ordered Field yields claim 1.
Claim 2. First, 0t=0 for every tβR: indeed 0t=(0+0)t=0t+0t by distributivity, and claim 2 of Additive Cancellation and Elementary Additive Identities in a Field applies. Consequently t+(β1)t=(1+(β1))t=0t=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 akββ€β£akββ£ and ββ£akββ£β€akβ for every kβ[n]. Applying claim 1 above to the families a and kβ¦β£akββ£ gives
k=1βnβakββ€k=1βnββ£akββ£.
Applying claim 1 above to the families kβ¦ββ£akββ£ and a, and evaluating the left-hand sum by claim 3 of Properties of Finite Sums with Ξ»=β1 together with the identity (β1)t=βt just established, gives
βk=1βnββ£akββ£=k=1βnβ(ββ£akββ£)β€k=1βnβakβ.
The two displayed bounds and claim 6 of Properties of the Absolute Value in an Ordered Field give claim 2.