Real positive number/Root/Unique existence/Fact/Proof


We define recursively nested intervals . We set

and we take for an arbitrary real number with . Suppose that the interval bounds are defined up to index , the intervals fulfil the containment condition and that

holds. We set


Hence one bound remains and one bound is replaced by the arithmetic mean of the bounds of the previous interval. In particular, the stated properties hold for all intervals and we have a sequence of nested intervals. Let denote the real number defined by this nested intervals according to fact. Because of exercise, we have

Due to fact, we get

Because of the construction of the interval bounds and due to fact, this is but also , hence .