Krull-Akizuki theorem without Axiom of Choice

Motivation
This question came from my efforts to solve this problem presented by Andre Weil in 1951.

We use the definitions in my answers to this question.
Can we prove the following theorem without Axiom of Choice?

Theorem
Let $A$ be a weakly Artinian integral domain.
Let $K$ be the field of fractions of $A$.
Let $L$ be a finite extension field of $K$.
Let $B$ be a subring of L containing $A$.
Then the following assertions hold.

(1) Every ideal of $B$ is finitely generated

(2) Every non-zero prime ideal of $B$ is maximal.

(3) $leng_A B/I$ is finite for every non-zero ideal $I$ of $B$.

EDIT
Why worry about the axiom of choice?

Solutions Collecting From Web of "Krull-Akizuki theorem without Axiom of Choice"

I borrowed the idea of the Bourbaki’s proof of Krull-Akizuki theorem.

Lemma 1
Let A be a weakly Artinian integral domain.
Let $M$ be a torsion $A$-module of finite type.
Then $leng_A M$ is finite.

Proof:
Let $x_1, …, x_n$ be generating elements of $M$.
There exists a non-zero element $f$ of $A$ such that $fx_i = 0$, $i = 1, …, n$.
Let $\psi:A^n \rightarrow M$ be the morphism defined by $\psi(e_i) = x_i$, $i = 1, …, n$,
where $e_1, …, e_n$ is the canonical basis of $A^n$.
Since $leng_A A^n/fA^n$ is finite and $\psi$ induces a surjective mophism $A^n/fA^n \rightarrow M$, $leng_A M$ is finite.
QED

Lemma 2
Let A be a weakly Artinian integral domain.
Let $K$ be the field of fractions of $A$.
Let $M$ be a torsion-free $A$-module of finite type.
Let $r = dim_K M \otimes_A K$.
Let $f$ be a non-zero element of $A$.
Then $leng_A M/fM \leq r(leng_A A/fA)$

Proof:
There exists a $A$-submodule $L$ of $M$ such that $L$ is isomorphic to $A^r$ and $Q = M/L$ is a torsion module of finite type over $A$.
Hence, by Lemma 1, $leng_A Q$ is finite.
Let $n \geq 1$ be any integer.
The kernel of $M/f^nM \rightarrow Q/f^nQ$ is $(L + f^nM)/f^nM$ which is isomorphic to $L/(f^nM \cap L)$.
Since $f^nL \subset f^nM \cap L$,
$leng_A M/f^nM \leq leng_A L/f^nL + leng_A Q/f^nQ \leq leng_A L/f^nL + leng_A Q$.
Since $M$ is torsion-free, $f$ induces isomorphism $M/fM \rightarrow fM/f^2M$.
Hence $leng_A M/f^nM = n(leng_A M/fM)$.
Similarly $leng_A L/f^nL = n(leng_A L/fL)$.
Hence $leng_A M/fM \leq leng_A L/fL + (1/n) leng_A Q$.
Since $L$ is isomorphic to $A^r$, $leng_A L/fL = r(leng_A A/fA)$. Hence, by letting $n \rightarrow \infty$, $leng_A M/fM \leq r(Leng_A A/fA)$.
QED

Lemma 3
Let A be a weakly Artinian integral domain.
Let $K$ be the field of fractions of $A$.
Let $M$ be a torsion-free $A$-module.
Suppose $r = dim_K M \otimes_A K$ is finite.
Let $f$ be a non-zero element of $A$.
Then $leng_A M/fM \leq r(Leng_A A/fA)$

Proof:
Let $(M_i)_I$ be the family of finitely generated $A$-submodules of $M$.
$M/fM = \cup_i (M_i + fM)/fM =\cup_i M_i/(M_i \cap fM)$.
Since $fM_i \subset M_i \cap fM$, $M_i/(M_i \cap fM)$ is isomorphic to a quotient of $M_i/fM_i$.
Hence, by Lemma 2, $leng_A M_i/(M_i \cap fM) \leq r(leng_A A/fA)$.
Hence, by By Lemma 4 of this, $leng_A M/fM \leq r(leng_A A/fA)$
QED

Lemma 4
Let A be a weakly Artinian integral domain.
Let $K$ be the field of fractions of $A$.
Let $L$ be a finite extension field of $K$.
Let $B$ be a subring of $L$ containing $A$.
Then $leng_A B/fB$ is finite for every non-zero element $f \in B$.

Proof:
Since $L$ is a finite extension of $K$, $a_rf^r + … + a_1f + a_0 = 0$, where $a_i \in A, a_0 \neq 0$.
Then $a_0 \in fB$.
Since $B \otimes_A K \subset L$, $dim_K B \otimes_A K \leq [L : K]$.
Hence, by Lemma 3, $leng_A B/a_0B$ is finite.
Hence $leng_A B/fB$ is finite.
QED

Proof of the title theorem
By Lemma 2 of my answer to this, $B$ is weakly Artinian.
Hence, by this, we are done.
QED