Proof of Suprema and Finite Sums in [0,∞]

Preliminaries. By The Extended Real Line, Its Order, and [0,∞] (ii) and The Extended Real Line, Its Order, and [0,∞] (i), every element of $[0,\infty]$ is either a real number $x$ with $0\le x$ or $\infty$, and not both. By Order and Suprema in the Extended Real Line (i), Order and Suprema in the Extended Real Line (ii) and Order and Suprema in the Extended Real Line (viii), $\le$ is a total order on $[-\infty,\infty]$ which agrees with the order of $\mathbb{R}$ on $\mathbb{R}$, every $x\in[0,\infty]$ satisfies $0\le x\le\infty$, and $\infty\le x$ only for $x=\infty$; by Order and Suprema in the Extended Real Line (iii) and Order and Suprema in the Extended Real Line (ix), every nonempty subset of $[0,\infty]$ has a supremum in $[0,\infty]$. Sums over finite sets of maps into $[0,\infty]$ lie in $[0,\infty]$ (Iterated Operations and Operations over Finite Sets Take Values in the Underlying Set (ii)). We use these facts without repeating the references, together with the following, for $x,y\in[0,\infty]$.

(P0) If $x\le y$ and $y\in\mathbb{R}$, then $x\in\mathbb{R}$: otherwise $x=\infty$ and $\infty\le y$ gives $y=\infty\notin\mathbb{R}$.

(P1) If $x,y\in\mathbb{R}$, then $x+y$ is the real sum; otherwise $x+y=\infty$. So $x+y\in\mathbb{R}$ if and only if $x,y\in\mathbb{R}$. This is Addition and Multiplication on [0,∞] (i).

(P2) If $x=0$ or $y=0$, then $xy=0$; if $x\neq0$ and $y\neq0$, then $xy$ is the real product if $x,y\in\mathbb{R}$, and $xy=\infty$ otherwise. This is Addition and Multiplication on [0,∞] (ii).

Proof of (i). Let $Y=\{x+c:x\in X\}$, a nonempty subset of $[0,\infty]$, and $T=\sup Y$. For $x\in X$, $x\le\sup X$, so $x+c\le\sup X+c$ by Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (iv); hence $T\le\sup X+c$. For the reverse inequality: if $c=\infty$, then $\infty\in Y$ by (P1), so $T=\infty$ by Order and Suprema in the Extended Real Line (v), and $\sup X+c\le T$. Let $c\in\mathbb{R}$. If $T=\infty$, then $\sup X+c\le T$. Let $T\in\mathbb{R}$. As $X\neq\emptyset$, let $x_{0}\in X$; then $c=0+c\le x_{0}+c\le T$ by Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (i) and Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (iv), so $c\le T$ in $\mathbb{R}$, and $T-c$ is a real number with $0\le T-c$, that is $T-c\in[0,\infty]$, with $(T-c)+c=T$ by (P1). For $x\in X$, $x+c\le T=(T-c)+c$, so $x\le T-c$ by Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (vi), as $c\in\mathbb{R}$. Hence $T-c$ is an upper bound of $X$, so $\sup X\le T-c$, and $\sup X+c\le(T-c)+c=T$ by Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (iv). By antisymmetry, $T=\sup X+c$.

Proof of (ii). Let $Y=\{cx:x\in X\}$ and $T=\sup Y$. For $x\in X$, $cx\le c\sup X$ by Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (iv) and Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (ii), so $T\le c\sup X$. For the reverse inequality, we distinguish cases. If $c=0$, then $Y=\{0\}$ by (P2), whose supremum is its greatest element $0$, and $c\sup X=0$ by (P2). If $c=\infty$ and every element of $X$ is $0$, then $X=\{0\}$, $\sup X=0$, $Y=\{0\}$ and $T=0=c\sup X$. If $c=\infty$ and some $x\in X$ is nonzero, then $cx=\infty$ by (P2), so $T=\infty$ by Order and Suprema in the Extended Real Line (v), and $c\sup X\le T$. If $c\in\mathbb{R}$ and $c\neq0$, so $0<c$: if $T=\infty$, then $c\sup X\le T$. Let $T\in\mathbb{R}$. For $x\in X$, $cx\le T$, so $cx\in\mathbb{R}$ by (P0); then $x\in\mathbb{R}$, trivially if $x=0$ and by (P2) otherwise, and $x\le T/c$ in $\mathbb{R}$ as $0<c$. Hence $T/c\in[0,\infty]$, it is an upper bound of $X$, $\sup X\le T/c$, and $c\sup X\le c(T/c)=T$ by Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (iv), Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (ii) and (P2). By antisymmetry, $T=c\sup X$.

Proof of (iii). First, $u_{m}\le u_{n}$ for all $m,n\in\mathbb{N}$ with $m\le n$, and likewise for $(v_{n})$. Let $K$ be the set of $n\in\mathbb{N}$ such that $u_{m}\le u_{n}$ for every $m\in\mathbb{N}$ with $m\le n$. If $m\le1$, then $1\le m$ by Arithmetic and Order of the Natural Numbers (x), so $m=1$ by Arithmetic and Order of the Natural Numbers (vi); thus $1\in K$. Let $n\in K$ and $m\le n+1$. If $m=n+1$, then $u_{m}\le u_{n+1}$. Otherwise $m<n+1$ by Arithmetic and Order of the Natural Numbers (vi), and $m\le n$: else $n<m$ by Arithmetic and Order of the Natural Numbers (vii), with $m<n+1$, contradicting Arithmetic and Order of the Natural Numbers (xi). So $u_{m}\le u_{n}\le u_{n+1}$. Hence $n+1\in K$, and $K=\mathbb{N}$ by Arithmetic and Order of the Natural Numbers (xiii).

Let $U=\sup_{n}u_{n}$, $V=\sup_{n}v_{n}$ and $S=\sup_{n}(u_{n}+v_{n})$. For $n\in\mathbb{N}$, $u_{n}+v_{n}\le U+v_{n}\le U+V$ by Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (iv) and Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (i); hence $S\le U+V$. Conversely let $m,n\in\mathbb{N}$. By Arithmetic and Order of the Natural Numbers (vii) and Arithmetic and Order of the Natural Numbers (vi), $m\le n$ or $n\le m$. If $m\le n$, then $u_{m}+v_{n}\le u_{n}+v_{n}\le S$; if $n\le m$, then $u_{m}+v_{n}\le u_{m}+v_{m}\le S$; both by the first paragraph and Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (iv). Fix $n$. Then $S$ is an upper bound of $\{u_{m}+v_{n}:m\in\mathbb{N}\}$, whose supremum is $U+v_{n}$ by (i); so $U+v_{n}\le S$, that is $v_{n}+U\le S$ by Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (i). As $n$ is arbitrary, (i) gives $V+U\le S$. Hence $S=U+V$ by antisymmetry and Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (i).

Proof of (iv). Let $f(y)\le g(y)$ for every $y\in A$. For $y\in A$ with $g(y)\neq\infty$, $g(y)\in\mathbb{R}$, so $f(y)\in\mathbb{R}$ by (P0), and $g(y)-f(y)$ is real with $0\le g(y)-f(y)$. By Maps Defined by Cases (i), with the condition $g(y)=\infty$ on $y\in A$ (predicative, with parameters $g$ and $\infty$, as a condition on a value of a map, by Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices (iv)), the value $\infty\in[0,\infty]$ where it holds, and the value $g(y)-f(y)$, a difference of real numbers lying in $[0,\infty]$ by the previous sentence, where it fails, there is a map $d:A\to[0,\infty]$ with $d(y)=\infty$ if $g(y)=\infty$, and $d(y)=g(y)-f(y)$ otherwise. Then $f(y)+d(y)=g(y)$ for every $y\in A$: if $g(y)=\infty$, by (P1); otherwise by real arithmetic and (P1). By Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (v) and Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (v),

$$\sum_{y\in A}g(y)=\sum_{y\in A}\big(f(y)+d(y)\big)=\sum_{y\in A}f(y)+\sum_{y\in A}d(y)\ge\sum_{y\in A}f(y).$$

Proof of (v). The sets $B$ and $A\setminus B$ are finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (iv), disjoint, with union $A$. By Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (ii) and Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (v), $\sum_{y\in A}f(y)=\sum_{y\in B}f(y)+\sum_{y\in A\setminus B}f(y)\ge\sum_{y\in B}f(y)$.

Proof of (vi). Let $\varphi:[0,\infty]\to[0,\infty]$, $x\mapsto cx$. Then $\varphi(0)=0$ by (P2), and $\varphi(x+y)=c(x+y)=cx+cy=\varphi(x)+\varphi(y)$ for $x,y\in[0,\infty]$ by Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (iii). By Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (vi), with both operations equal to $+$ on $[0,\infty]$ and both neutral elements $0$ (Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (i)), $c\sum_{y\in A}f(y)=\sum_{y\in A}cf(y)$.

Proof of (vii). Applying (vi) with $c=0$ to the map $f:A\to[0,\infty]$ with all values $0$, and using $0\cdot0=0$, gives $\sum_{y\in A}0=0\cdot\sum_{y\in A}0=0$ by (P2).

Proof of (viii). For $n\in\mathbb{N}$ there is a map $h_{n}:A\to[0,\infty]$ with $h_{n}(y)=w(n,y)$ for every $y\in A$ (Maps and Relations Given by Formulas (i)); for $C\subseteq A$, $\sum_{y\in C}w(n,y)$ is the sum $\sum_{y\in C}h_{n}(y)$ of $h_{n}|_{C}$ (Sums and Products over a Finite Set and over an Interval (iii)). For a finite set $C$, let $\varphi(C)$ be the statement: if $C\subseteq A$, then $\sum_{y\in C}\sup_{n}w(n,y)=\sup_{n}\sum_{y\in C}w(n,y)$; it is predicative, with the parameters $w$ and $A$ (Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices (iv)). For $C=\emptyset$, both sides are $0$: the left by Sums and Products over a Finite Set and over an Interval (ii), and the right as the supremum of $\{0\}$, which is its greatest element $0$. Let $C$ be finite with $\varphi(C)$, let $z\notin C$, and let $C\cup\{z\}\subseteq A$. Then $C\subseteq A$. For $n\in\mathbb{N}$ let $U_{n}=\sum_{y\in C}h_{n}(y)$ and $V_{n}=w(n,z)$. By Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set (v), applied to $+$ on $[0,\infty]$ (associative and commutative with neutral element $0$ by Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (i)), the finite set $C$ and the restriction of $w$ to $\mathbb{N}\times C$, whose map $y\mapsto w(n,y)$ on $C$ is $h_{n}|_{C}$, there is a map $\mathbb{N}\to[0,\infty]$, $n\mapsto U_{n}$; by Maps and Relations Given by Formulas (i) there is a map $\mathbb{N}\to[0,\infty]$, $n\mapsto V_{n}$. So $(U_{n})$ and $(V_{n})$ are sequences in $[0,\infty]$. Then $U_{n}\le U_{n+1}$ by (iv), applied with $C$ in place of $A$ to $h_{n}|_{C}$ and $h_{n+1}|_{C}$, and $V_{n}\le V_{n+1}$ by hypothesis. As $C\cap\{z\}=\emptyset$, Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (ii) and Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (i) give $\sum_{y\in C\cup\{z\}}w(n,y)=U_{n}+V_{n}$ and $\sum_{y\in C\cup\{z\}}\sup_{m}w(m,y)=\sum_{y\in C}\sup_{m}w(m,y)+\sup_{m}w(m,z)$. By $\varphi(C)$ and (iii), the latter equals $\sup_{n}U_{n}+\sup_{n}V_{n}=\sup_{n}(U_{n}+V_{n})=\sup_{n}\sum_{y\in C\cup\{z\}}w(n,y)$. So $\varphi(C\cup\{z\})$ holds. By Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (iii), $\varphi(C)$ holds for every finite set $C$, in particular for $C=A$.