Proof of Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros

Elements of $[0,\infty]$ lie in $[-\infty,\infty]$ and $0\in\mathbb{R}\subseteq[-\infty,\infty]$, by The Extended Real Line, Its Order, and [0,∞] (ii); as $0\le0$ in $\mathbb{R}$, also $0\in[0,\infty]$ by The Extended Real Line, Its Order, and [0,∞] (ii).

Proof of (i). Let $a\in[0,\infty]$ with $a\le0$. By Order and Suprema in the Extended Real Line (viii), $0\le a$. By Order and Suprema in the Extended Real Line (i), $\le$ is a total order, in particular a partial order, on $[-\infty,\infty]$, so it is antisymmetric by Partial and Total Orders on a Set and the Associated Strict Relation (i); hence $a\le0$ and $0\le a$ give $a=0$.

Proof of (ii). Let $a\in[0,\infty]$. If $a\in\mathbb{R}$, then $a\le\infty$ by The Extended Real Line, Its Order, and [0,∞] (iii), the case $y=\infty$ there, and $a\neq\infty$ because $\infty\notin\mathbb{R}$ by The Extended Real Line, Its Order, and [0,∞] (i); so $a<\infty$ by The Extended Real Line, Its Order, and [0,∞] (iii). Conversely, let $a<\infty$; then $a\neq\infty$ by The Extended Real Line, Its Order, and [0,∞] (iii). By The Extended Real Line, Its Order, and [0,∞] (ii), either $a\in\mathbb{R}$ and $0\le a$, or $a=\infty$; the second is excluded, so $a\in\mathbb{R}$.

Proof of (iii). Let $a,b\in[0,\infty]$ with $a\le b$ and $b<\infty$, so $b\neq\infty$ by The Extended Real Line, Its Order, and [0,∞] (iii). If $a=\infty$, then $\infty\le b$, so $b=\infty$ by Order and Suprema in the Extended Real Line (ii), which is impossible. So $a\neq\infty$, and $a\in\mathbb{R}$ by The Extended Real Line, Its Order, and [0,∞] (ii); then $a<\infty$ by (ii).

Proof of (iv). Let $(a_{k})$ be a sequence in $[0,\infty]$ with $a_{k}=0$ for every $k\in\mathbb{N}$, and let $s_{1}=\sum_{k=1}^{1}a_{k}$ be its first partial sum. In particular $a_{k}=0$ for every $k\in\mathbb{N}$ with $1<k$, so Sums of Sequences in [0,∞]: Real Series, Linearity, Comparison, Rearrangement, Double Series and Monotone Convergence (vii), with $n=1$, gives $\sum_{k\in\mathbb{N}}a_{k}=s_{1}$. By Iterated Operations: Finite Sums and Finite Products (ii), $s_{1}$ is the iterated operation of the sum $+$, a binary operation on $[0,\infty]$ by Addition and Multiplication on [0,∞] (i), applied to the restriction $a|_{[1]}$ of $a$ to $[1]=\{1\}$, a subset of $\mathbb{N}$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i); since $[1]\subseteq\mathbb{N}$, this restriction is a map $[1]\to[0,\infty]$ by Domains and Restrictions of Maps (ii), whose value at $1$ is $a_{1}$ by Domains and Restrictions of Maps (iii). By Iterated Operations: Finite Sums and Finite Products (i), with $n=1$, this iterated operation is $t(1)$, where $t:[1]\to[0,\infty]$ is the map of Iterating a Binary Operation along a Finite List (i) for $+$ and $a|_{[1]}$; that map satisfies $t(1)=(a|_{[1]})(1)$. Hence $s_{1}=t(1)=a_{1}=0$. Hence $\sum_{k\in\mathbb{N}}a_{k}=0$.