Throughout, Rn is Euclidean space, xβ
y is the dot product, Bx is the matrix-vector product, and 0Rnβ is the origin, all components of which are 0.
Step 0: squares are nonnegative. Let tβR. By the totality of the order of the ordered field R, either 0β€t or tβ€0. If 0β€t, then claim 5 of Elementary Arithmetic in an Ordered Field, applied to the inequality 0β€t and the nonnegative factor t, gives 0tβ€tt, and 0t=0 by Zero Products and Elementary Identities in a Field. If tβ€0, then adding βt to both sides by claim 3 of Elementary Order Arithmetic in an Ordered Field gives 0β€βt, so the previous case gives 0β€(βt)(βt), and (βt)(βt)=tt by Zero Products and Elementary Identities in a Field. In both cases 0β€tt.
Step 1: the diagonal entries are nonnegative. Fix iβ[n] and let eβRn be the vector with eiβ=1 and ejβ=0 for jβ[n] with jξ =i. For jβ[n] the summands of (Be)jβ=βk=1nβBjkβekβ vanish for kξ =i, so claim 7 of Properties of Finite Sums gives (Be)jβ=Bjiβ. The same claim applied to eβ
(Be)=βj=1nβejβ(Be)jβ gives
eβ
(Be)=(Be)iβ=Biiβ.
Since B is positive semidefinite, 0β€eβ
(Be), so 0β€Biiβ. As this holds for every iβ[n], claim 5 of Properties of Finite Products gives 0β€βi=1nβBiiβ.
Step 2: the positive definite case. Suppose B is positive definite. By claim 4 of Properties of the Order on the Natural Numbers we have 1β€n, so Cholesky Factorisation of a Symmetric Positive Definite Real Matrix applies and provides a lower triangular real nΓn matrix L, in the sense of The Determinant of a Triangular Matrix is the Product of its Diagonal Entries, with 0<Liiβ for every iβ[n] and B=LLβ€, where Lβ€ is the transpose and the product is the matrix product.
The matrix Lβ€ is upper triangular with (Lβ€)iiβ=Liiβ, since (Lβ€)ilβ=Lliβ and Lliβ=0 whenever l<i. Hence The Determinant is Multiplicative, claims 1 and 2 of The Determinant of a Triangular Matrix is the Product of its Diagonal Entries, and claim 2 of Properties of Finite Products give
detB=detLΒ det(Lβ€)=(i=1βnβLiiβ)(i=1βnβLiiβ)=i=1βnβLiiβLiiβ.
On the other hand, by Product of Real Matrices and Transpose of a Real Matrix,
Biiβ=k=1βnβLikβ(Lβ€)kiβ=k=1βnβLikβLikβ(iβ[n]),
and every summand is nonnegative by Step 0, so claim 6 of Properties of Finite Sums gives LiiβLiiββ€Biiβ for every iβ[n]. Since also 0β€LiiβLiiβ by Step 0, claim 5 of Properties of Finite Products gives
0β€i=1βnβLiiβLiiββ€i=1βnβBiiβ,
which is the assertion.
Step 3: the remaining case. Suppose B is not positive definite. By Symmetric, Positive Semidefinite, and Positive Definite Real Matrices and the trichotomy of the order of R there is then an xβRn with xξ =0Rnβ and xβ
(Bx)β€0; since B is positive semidefinite we also have 0β€xβ
(Bx), so xβ
(Bx)=0. Claim 3 of Cauchy-Schwarz Inequality for a Positive Semidefinite Quadratic Form on Rn gives Bx=0Rnβ, that is,
i=1βnβBjiβxiβ=0forΒ everyΒ jβ[n].
Because B is symmetric and multiplication in R is commutative, Bjiβxiβ=xiβBijβ, so βi=1nβxiβBijβ=0 for every jβ[n]. Moreover xξ =0Rnβ means that xkβξ =0 for at least one kβ[n]. Claim 6 of Row Properties of the Determinant therefore gives detB=0, and Step 1 gives 0β€βi=1nβBiiβ, so the asserted inequalities hold.