Let $K$ be a field. We write $K[[X]]$ for the ring of all formal power series with coefficients from the field $K$. Then, we will try to prove the next theorem.
Theorem. If $K$ is a field then:
$K[[X]]$ is PID
The ideals of $K[[X]]$ have the form $\langle X^k \rangle$, $k=1,2,3,...$ and in particular, it is $$\langle X \rangle \supset \langle X^2 \rangle \supset \langle X^3 \rangle \supset \langle X^4 \rangle \supset \cdots \ .$$
Proof. 1. Let's take a non-zero ideal $\{0_K \} \neq I \trianglelefteq K[[X]]$ of $K[[X]]$. We define the subset $$E:=\{ n\in \Bbb{N}: n=\tau (f(X)),\ f(X)\in I \}\subseteq \Bbb{N}$$ where $\tau(f(X))$ is the order of the formal power series $f(X)$.
Then, $E\neq \emptyset$ (because $I \neq \{0_K \} $) and from the Well-Ordering Principle, there is an element $n_0\in E$ such that $n_0=\tau (g(X))$, for some $g(X)\in I$.
Claim. We will show that $I=\langle X^{n_0} \rangle $.
Trivial Case: If $n_0=0\iff \tau(g(X))=0 \iff $ the fixed term of $g(X)$ is non-zero $\iff g(X)\in U(K[[X]]).$ So, $I$ contains an invertible element $\iff I=K[[X]]=\langle 1_K \rangle $.
If $n_0>0 $, we can write
\begin{align} g(X) &:=a_{n_0}X^{n_0}+a_{n_1}X^{n_1}+... && \in I \trianglelefteq K[[X]]\\ &= X^{n_0}\cdot (a_{n_0}+a_{n_0+1}X+...) && \in I \trianglelefteq K[[X]] \tag{♠} \end{align}
where the term $a_{n_0} \neq 0_K$ and we set $h(X):=a_{n_0}+a_{n_0+1}X+... \in K[[X]] $. But then, $a_{n_0}\neq 0_K\iff h(X) \in U(K[[X]])$. So, $(♠)$ could be written in the form
\begin{align} X^{n_{0}}&=g(X)\cdot h(X)^{-1}\in I \implies \\ \langle X^{n_{0}} \rangle & \subseteq I. \tag{1} \end{align}
On the other hand, if we take an element $f(X)\in I$, then
\begin{align} f(x) & \in I && \implies \\ \tau(f(X)):&=n_1 \geq n_0 && \implies \\ f(X) & =X^{n_0}\cdot \ell (X),\ \ell (X) \in K[[X]] && \implies \\ f(X) & \in \langle X^{n_{0}} \rangle . \end{align} So, $$I\subseteq \langle X^{n_0} \rangle \tag{2}.$$
And now, from $(1),(2)$ we get $I = \langle X^{n_0} \rangle$. So, every non zero ideal $I\trianglelefteq K[[Χ]]$ is principal.
Questions.
1) Is this proof completely right?
2) Why do we get from 1. this decreasing sequence of ideals?
3) Can we conclude from 2. that our $K[[X]]$ is Noetherian?