Proof of A Closed Interval Covered by Open Intervals Is No Longer than Their Total Length

Write $\lambda(m)=b_{m}-a_{m}$ for $m\in\mathbb{N}$. A real number $u\ge0$ is an element of $[0,\infty]$ (The Extended Real Line, Its Order, and [0,∞] (ii)), the sum in $[0,\infty]$ of two such numbers is their real sum (Addition and Multiplication on [0,∞] (i)), and on real numbers the order of $[0,\infty]$ is that of $\mathbb{R}$ (Order and Suprema in the Extended Real Line (i)); these identifications are used throughout. For a set $G\subseteq\mathbb{N}$ and $u,v\in\mathbb{R}$ with $u\le v$, say that $G$ covers $[u,v]$ if every $x\in[u,v]$ lies in $(a_{m},b_{m})$ for some $m\in G$. The empty set covers no such $[u,v]$, since $u\in[u,v]$.

Proof of (i). Differences of real numbers are read in the type $\mathrm{Real}$ of The Real Numbers as a Type (i): for $x,y\in\mathbb{R}$, the difference $x-y$ lies in $\mathbb{R}$ and equals $x+(-y)$, the difference in $\mathrm{Real}$, by Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (i); so the laws of The Real Numbers as a Type (iv), The Real Numbers as a Type (v) and The Real Numbers as a Type (vi) govern the arithmetic and the inequalities between differences below. As $b_{m}-a_{m}\in[0,\infty]$ for $m\in\mathbb{N}$ by hypothesis, there is the map $\lambda:F\to[0,\infty]$ of the given lengths, $\lambda(m)=b_{m}-a_{m}$ for $m\in F$, and the claim reads $q-p\le\sum_{m\in F}\lambda(m)$. Every $G\subseteq F$ is 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), and $\sum_{m\in G}\lambda(m)\in[0,\infty]$ is the sum over $G$ of the restriction $\lambda|_{G}$, as in Sums and Products over a Finite Set and over an Interval (iii), the sum $+$ of $[0,\infty]$ having the neutral element $0$ by Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (i). We induct over the subsets $G$ of $F$ by their number of elements $\#G\in\mathbb{N}_{0}$. For $n\in\mathbb{N}$ let $\varphi(n)$ be the statement: for every $G\subseteq F$ with $\#G<n$ and all $u,v\in\mathbb{R}$ with $u\le v$ such that $G$ covers $[u,v]$, we have $v-u\le\sum_{m\in G}\lambda(m)$.

The condition $\varphi(n)$ on the set variable $n$ is expressed by a predicative formula whose parameters are $F$, $\lambda$, the sequences $a$ and $b$ (the maps $m\mapsto a_{m}$ and $m\mapsto b_{m}$ on $\mathbb{N}$), $\mathbb{R}$ with its $+$, $\cdot$, $0$, $1$ and its order $\le$ (the strict order of $\mathbb{R}$ occurs only through $\le$ and $\neq$), $[0,\infty]$ with its order $\le$ and its sum $+$, and $\mathbb{N}_{0}$, $\mathbb{N}$, the order and the addition of $\mathbb{N}_{0}$. Namely, as $\#G$ is the unique $j\in\mathbb{N}_{0}$ for which there is a bijection from $[j]$ onto $G$ (The Number of Elements of a Finite Set (i)), and $x\in(a_{m},b_{m})$ means $a_{m}<x<b_{m}$ (Intervals of the Real Line (ii)), for $n\in\mathbb{N}$, $\varphi(n)$ holds if and only if

$$\forall G\,\forall u\,\forall v\,\Bigl(\bigl(G\subseteq F\wedge\exists j\,\exists h\,(j<n\wedge\beta(h,j,G))\wedge u,v\in\mathbb{R}\wedge u\le v\wedge\kappa(G,u,v)\bigr)\Rightarrow\exists w\,\exists d\,\bigl(\mathrm{fop}(w,G,\lambda)\wedge\delta(v,u,d)\wedge d\le w\bigr)\Bigr),$$

where $\beta(h,j,G)$ is the condition that $j\in\mathbb{N}_{0}$ and $h$ is a bijection from $[j]$ onto $G$; $\kappa(G,u,v)$ is

$$\forall x\,\Bigl(\bigl(x\in\mathbb{R}\wedge u\le x\wedge x\le v\bigr)\Rightarrow\exists m\,\bigl(m\in G\wedge\exists y\,((m,y)\in a\wedge y<x)\wedge\exists z\,((m,z)\in b\wedge x<z)\bigr)\Bigr);$$

$\mathrm{fop}(w,G,\lambda)$ is the formula $\mathrm{fop}(w,C,g)$ of Iterated Operations over Finite Sets Are Given by a Predicative Formula (i) with that lemma's set variables $w$, $C$ and $g$ taken as $w$, $G$ and $\lambda$, and with $[0,\infty]$, its sum $+$, $\mathbb{N}$, and the order and the addition of $\mathbb{N}_{0}$ assigned to that lemma's class variables $X$, $F$, $Y$, $R$ and $P$, chosen distinct from every variable used here (so that lemma's $F$ is the operation $+$ of $[0,\infty]$, not our set $F$, and its map $g$ is our $\lambda$); as $+$ is associative and commutative with neutral element $0$ (Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (i)), that lemma gives that, for $G\subseteq F$, $\mathrm{fop}(w,G,\lambda)$ holds if and only if $w=\sum_{m\in G}\lambda(m)$, $G$ being finite and $\lambda$ a map from the set $F\supseteq G$ to $[0,\infty]$; and $\delta(v,u,d)$ is the condition $v\in\mathbb{R}\wedge u\in\mathbb{R}\wedge d=v-u$. For $m\in G\subseteq\mathbb{N}$, the formula $\exists y\,((m,y)\in a\wedge y<x)$ holds if and only if $a_{m}<x$, and likewise for $b$, by Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (i), as $m$ lies in the domain $\mathbb{N}$ of $a$ and of $b$. From now on, $\varphi$ is the condition on the variable $n$ given by this formula. The parts are predicative: $\beta$ by Predicative Formulas for Bijections from a Segment [n] and for Increasing Listings (i); $\mathrm{fop}$ by Iterated Operations over Finite Sets Are Given by a Predicative Formula (i); $\delta$ by Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (iv), $\mathbb{R}$ being an ordered field; the formulas $\exists y\,((m,y)\in a\wedge y<x)$ and $\exists z\,((m,z)\in b\wedge x<z)$ by Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (i); $u,v\in\mathbb{R}$, $x\in\mathbb{R}$ and $m\in G$ are atomic; $G\subseteq F$ abbreviates $\forall t\,(t\in G\Rightarrow t\in F)$; $u\le v$, $u\le x$, $x\le v$ and $d\le w$ state that an ordered pair lies in a parameter relation, the order of $\mathbb{R}$ or that of $[0,\infty]$, and are predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (vi) and Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i); and the strict relations $j<n$, $y<x$ and $x<z$ are $\le$ together with $\neq$, that is $j\le n\wedge j\neq n$, $y\le x\wedge y\neq x$ and $x\le z\wedge x\neq z$, for $\mathbb{N}_{0}$ by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor (ii) and for $\mathbb{R}$ by Partial and Total Orders on a Set and the Associated Strict Relation (iii), $<$ being the strict relation of the order of $\mathbb{R}$ (The Real Numbers as a Type (ii)), so they are predicative by the same two clauses. The whole formula quantifies over the set variables $G$, $u$, $v$, $j$, $h$, $x$, $m$, $y$, $z$, $w$, $d$ and $t$ only, so it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i). So we may prove $\varphi(n)$ for every $n\in\mathbb{N}$ by Induction for Predicative Formulas, and the Order of ℕ below 1 and below n+1 (i).

If $G\subseteq\mathbb{N}$ is finite and nonempty, then $\#G\neq0$ by Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products (ii), so $\#G\in\mathbb{N}$, as $\mathbb{N}=\mathbb{N}_{0}\setminus\{0\}$ (The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii)).

Since $p\in[p,q]$ lies in $(a_{m},b_{m})$ for some $m\in F$, $F$ is nonempty, so $\#F\in\mathbb{N}$ by the preceding paragraph; then $\#F<\#F+1$ by Arithmetic and Order of the Natural Numbers (xi), and $\#F+1\in\mathbb{N}$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication (vi). So the statement $\varphi(\#F+1)$, applied to $G=F$, $u=p$ and $v=q$, gives $q-p\le\sum_{m\in F}\lambda(m)$, the claim. It remains to prove $\varphi(n)$ for every $n\in\mathbb{N}$.

Base. Let $G\subseteq F$ with $\#G<1$. If $G$ were nonempty, then $\#G\in\mathbb{N}$ with $\#G<1$, which Induction for Predicative Formulas, and the Order of ℕ below 1 and below n+1 (ii) excludes. So $G=\emptyset$, which covers no $[u,v]$, and $\varphi(1)$ holds.

Step. Let $n\in\mathbb{N}$ with $\varphi(n)$, let $G\subseteq F$ with $\#G<n+1$, and let $u,v\in\mathbb{R}$ with $u\le v$ be such that $G$ covers $[u,v]$. Then $G\neq\emptyset$, so $\#G\in\mathbb{N}$ and hence $\#G\le n$ by Induction for Predicative Formulas, and the Order of ℕ below 1 and below n+1 (iii). Since $v\in[u,v]$, there is $k\in G$ with $a_{k}<v<b_{k}$. Let $G'=G\setminus\{k\}$; it is a subset of $F$, and $\#G'<\#G$ by Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products (iv), as $G'\subseteq G$ and $G'\neq G$. Hence $\#G'<n$ in $\mathbb{N}_{0}$, where $\#G'$ may be $0$: by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor (ii), $\#G'\le\#G$ and $\#G'\neq\#G$; as the order of $\mathbb{N}_{0}$ is a well-order (The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor (i)), hence a partial order, $\#G'\le\#G$ and $\#G\le n$ give $\#G'\le n$ by transitivity; and $\#G'=n$ would give $\#G\le\#G'$, hence $\#G=\#G'$ by antisymmetry, which is false; so $\#G'<n$ by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor (ii). As $G=G'\cup\{k\}$ with $G'\cap\{k\}=\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), applied to $\lambda|_{G}$, whose restrictions to $G'$ and to $\{k\}$ are those of $\lambda$, give

$$\sum_{m\in G}\lambda(m)=\sum_{m\in G'}\lambda(m)+\lambda(k).$$

Put $\Sigma'=\sum_{m\in G'}\lambda(m)\in[0,\infty]$. Two cases.

If $a_{k}<u$, then adding $v-u-a_{k}$ to both sides of $a_{k}<u$ and $-a_{k}$ to both sides of $v<b_{k}$ gives

$$v-u<v-a_{k}<b_{k}-a_{k}=\lambda(k)$$

by The Real Numbers as a Type (vi), the sums being simplified with the negatives and $x+(-x)=0$ of The Real Numbers as a Type (iv), and the inequalities staying strict as $x<y$ means $x\le y$ and not $y\le x$ (The Real Numbers as a Type (v)); so $v-u\le\lambda(k)$ by the transitivity in The Real Numbers as a Type (v). Further $0\le v-u$, by adding $-u$ to both sides of $u\le v$ (The Real Numbers as a Type (vi), The Real Numbers as a Type (iv)), so $v-u\in[0,\infty]$. Also $\lambda(k)\le\lambda(k)+\Sigma'=\Sigma'+\lambda(k)$ by Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (v) and Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (i). As $v-u\le\lambda(k)$ also in $[0,\infty]$, the transitivity of its total order (Order and Suprema in the Extended Real Line (i)) gives $v-u\le\sum_{m\in G}\lambda(m)$.

If $u\le a_{k}$, then $u\le a_{k}<v$. Every $y\in[u,a_{k}]$ lies in $[u,v]$, hence in $(a_{m},b_{m})$ for some $m\in G$; and $m\neq k$, as $y\le a_{k}$ means $y\notin(a_{k},b_{k})$. So $G'$ covers $[u,a_{k}]$, and $\varphi(n)$, applied to $G'$, $u$ and $a_{k}$, gives $a_{k}-u\le\Sigma'$. Also, adding $-a_{k}$ to both sides of $v<b_{k}$, $-u$ to both sides of $u\le a_{k}$ and $-a_{k}$ to both sides of $a_{k}<v$ gives $v-a_{k}\le b_{k}-a_{k}=\lambda(k)$, $0\le a_{k}-u$ and $0\le v-a_{k}$ by The Real Numbers as a Type (vi), with $x+(-x)=0$ from The Real Numbers as a Type (iv), and a strict inequality giving the weak one by The Real Numbers as a Type (v). By Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (iv), applied twice, Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (i) and the transitivity of the total order of $[0,\infty]$ (Order and Suprema in the Extended Real Line (i)),

$$v-u=(a_{k}-u)+(v-a_{k})\le\Sigma'+(v-a_{k})\le\Sigma'+\lambda(k)=\sum_{m\in G}\lambda(m),$$

the first equation holding in $\mathbb{R}$ by The Real Numbers as a Type (iv), its right side being the real sum of two nonnegative reals. This proves $\varphi(n+1)$.

Proof of (ii). For $n\in\mathbb{N}$ the segment $[n]=\{1,\dots,n\}$ is a finite subset of $\mathbb{N}$ (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 (vii)). Let

$$S=\{x\in[p,q]:\text{there is }n\in\mathbb{N}\text{ such that }[n]\text{ covers }[p,x]\}.$$

(The defining condition of $S$ is predicative: it quantifies over sets only and is built from the same pieces as the condition $\varphi(n)$ above, namely the values $a_{m}$ and $b_{m}$, membership in the intervals $(a_{m},b_{m})$ and $[p,x]$, the segments $[n]$ and the orders of $\mathbb{R}$ and $\mathbb{N}_{0}$, so it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i). So $S$ is a subclass of the set $[p,q]$, hence a set by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i).) If $[n]$ covers $[p,x]$ and $n\le n'$, then $[n']$ covers $[p,x]$, as $[n]\subseteq[n']$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (v). For $k,n\in\mathbb{N}$ with $k\le n$, $k\in[n]$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i); in particular $k\in[k]$, as $k\le k$ by Arithmetic and Order of the Natural Numbers (vi).

$S$ is nonempty and has supremum $q$. By hypothesis $p\in(a_{k},b_{k})$ for some $k\in\mathbb{N}$; as $[p,p]=\{p\}$ and $k\in[k]$, the segment $[k]$ covers $[p,p]$, so $p\in S$. Thus $S$ is a nonempty subset of $\mathbb{R}$ bounded above by $q$, and has a supremum $s\in\mathbb{R}$ by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (vii), with $p\le s\le q$. By hypothesis $s\in(a_{k},b_{k})$ for some $k\in\mathbb{N}$. As $a_{k}<s$, the number $a_{k}$ is not an upper bound of $S$ (Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv)), so there is $x\in S$ with $a_{k}<x$; fix such an $x$ and $n_{x}\in\mathbb{N}$ such that $[n_{x}]$ covers $[p,x]$. Let $n=\max\{n_{x},k\}$, which exists by The Maximum and Minimum of Two Elements of a Total Order (i), so that $n_{x}\le n$ and $k\le n$ (The Maximum and Minimum of Two Elements of a Total Order (iii), for the total order of $\mathbb{N}$).

We claim that every $y\in[p,q]$ with $y<b_{k}$ lies in $S$, as $[n]$ covers $[p,y]$. Let $z\in[p,y]$. If $z\le x$, then $z\in[p,x]$ lies in $(a_{m},b_{m})$ for some $m\in[n_{x}]\subseteq[n]$. If $x<z$, then $a_{k}<x<z\le y<b_{k}$, so $z\in(a_{k},b_{k})$ with $k\in[n]$. This proves the claim.

Suppose $s<q$. Let $y=\min\{q,s+(b_{k}-s)/2\}$, which exists by The Maximum and Minimum of Two Elements of a Total Order (i), for the total order of $\mathbb{R}$. As $s<b_{k}$, Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares (vii) gives $s<s+(b_{k}-s)/2<b_{k}$; as also $s<q$, and $y$ is one of $q$ and $s+(b_{k}-s)/2$ (The Maximum and Minimum of Two Elements of a Total Order (ii)), we get $s<y$, and $y\le s+(b_{k}-s)/2<b_{k}$ and $y\le q$ by The Maximum and Minimum of Two Elements of a Total Order (iii). So $y\in[p,q]$ and $y<b_{k}$, hence $y\in S$ by the claim, contradicting $s<y$ and $s=\sup S$. Hence $s=q$.

Conclusion. Now $q=s<b_{k}$ and $q\in[p,q]$, so $q\in S$ by the claim: $[n]$ covers $[p,q]$. By (i), applied to $F=[n]$, and by Sums of Sequences in [0,∞]: Real Series, Linearity, Comparison, Rearrangement, Double Series and Monotone Convergence (iv),

$$q-p\le\sum_{m\in[n]}\lambda(m)\le\sum_{m\in\mathbb{N}}\lambda(m).$$