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

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $\infty$, $[-\infty,\infty]$, $[0,\infty]$, the order $\le$ and the relation $<$ be as in The Extended Real Line, Its Order, and [0,∞] (i), The Extended Real Line, Its Order, and [0,∞] (ii) and The Extended Real Line, Its Order, and [0,∞] (iii), let $0$ be the zero of $\mathbb{R}$, an element of $[0,\infty]$ as in The Extended Real Line, Its Order, and [0,∞] (ii), and let sums of sequences in $[0,\infty]$ be as in Sum of a Sequence in [0,∞] (ii).

(i) If $a\in[0,\infty]$ and $a\le0$, then $a=0$.

(ii) For $a\in[0,\infty]$: $a<\infty$ if and only if $a\in\mathbb{R}$.

(iii) If $a,b\in[0,\infty]$, $a\le b$ and $b<\infty$, then $a<\infty$, and hence $a\in\mathbb{R}$.

(iv) If $(a_{k})$ is a sequence in $[0,\infty]$ with $a_{k}=0$ for every $k\in\mathbb{N}$, then $\sum_{k\in\mathbb{N}}a_{k}=0$.