Strictly Positive Integer Power Function Strictly Succeeds Each Element

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\struct {R, +, \circ, \le}$ be an ordered ring with unity.

Let $\struct {R, \le}$ be a directed set with no upper bound.

Let $n \in \N_{>0}$.

Let $f: R \to R$ be defined by:

$\forall x \in R: \map f x = \circ^n x$


Then the image of $f$ has elements strictly succeeding each elements of $R$.


Proof

Let $b \in R$.

By Directed Set has Strict Successors iff Unbounded Above:

$\exists c \in R: b < c$
$\exists d \in R: 1 < d$

By the definition of a directed set:

$\exists e \in R: d \le e, c \le e$

$\struct {R, +, \circ, \le}$ is an ordered ring, so $\le$ is by definition a transitive relation.

Hence by transitivity:

$b < e$

and:

$1 < e$

By Strictly Positive Power of Strictly Positive Element Greater than One Succeeds Element:

$e \le \map f e$

Thus by transitivity:

$b < \map f e$

$\blacksquare$