Previously asked on Math Stackexchange without answers.
Background: As sort of a hobby, Ernst Witt gave extremely short proofs for famous theorems. This question is about his six-line proof of the Gelfand-Mazur Theorem ("The only $\Bbb C$-Banach algebra $K$ which is a skew field is $\Bbb C$ itself") resp. its historic predecessor and now corollary, Ostrowski's Theorem ("The only complete Archimedean fields are $\Bbb R$ and $\Bbb C$"; not to be confused with the more famous Ostrowski's theorem which classifies valuations on $\Bbb Q$). Witt's article is "Über einen Satz von Ostrowski", Arch. Math. 3 (1952), p. 334, reprinted on p. 404 of his Collected Papers. The best free online source I could find is this (H.-D. Ebbinghaus, Numbers, p. 245) English translation of its decisive three sentences.
I understand the first sentence, which says that w.l.o.g. we can assume $\dim_{\Bbb R}K>2$ and hence $K^\times$ simply connected. I also understand the third sentence which says that there cannot be an isomorphism between the additive group of $K$ and the multiplicative group $K^\times$ (obviously, as we are in characteristic $0$; there is a typo in the translation, since of course it's the element $-1$ which is of order 2 in $K^\times$, and that's what Witt writes in the original). But the second sentence
The differential equation $x^{-1}dx = dy$ then [i.e. assuming $K\setminus \lbrace 0\rbrace$ simply connected] engenders a global isomorphism between the multiplicative group $(x\neq 0$) and the additive group $(y)$.
(Original: "Die Differentialgleichung $x^{-1}dx=dy$ vermittelt daher eine globale Isomorphie zwischen der multiplikativen Gruppe $(x\neq 0)$ und der additiven Gruppe $(y)$.")
seems to hide some details. My guess would be the idea is that by simply connectedness, path-integrating $f(x) = x^{-1}$ from the startpoint $1$ to any $x\neq 0$ gives a well defined "logarithm" function $F(x)$ which has the property $F(ab) = F(a) + F(b)$ and is bijective. (Which then, as said, I understand gives a contradiction and shows no such $K$ with $\Bbb R$-dimension $>2$ exists.)
Question 1: How to understand the highlighted sentence? In particular, is my interpretation correct and if yes, how exactly to show such an $F$ is a group isomorphism $K^\times \simeq (K,+)$?
Question 2: Does this prove Gelfand-Mazur, as Ebbinghaus seems to imply, or merely Ostrowski's theorem, as Witt's own title claims? If it only proves Ostrowski's theorem, is there a way to upgrade this to a full proof of Gelfand-Mazur?
Note 1: (Edit) As checked by J. Wengenroth (thanks), Witt indeed writes $x^{-1}dx = \color{red}{d}y$, whereas Ebbinghaus has $x^{-1}dx=y$.
Note 2: I am aware of the standard calculus proof that $F(x) = \int_1^x \frac{dt}{t}$ satisfies $F(ab) = F(a) +F(b)$ (actually, teaching that in my calculus class last week reminded me of this question), but it seems Witt is assuming a generalisation of this, and maybe more differential calculus, to a possibly infinite dimensional $\Bbb R$ resp. $\Bbb C$-vector space, which is a bit outside of my comfort zone.
Note 3: In the comment sections here and here Keith Conrad explains how Witt's argument proves the Fundamental Theorem of Algebra, referring to Ebbinghaus as a source. I understand that explanation, but to my (probably poor) understanding it uses Lie-theoretic background and the assumption that $\dim_{\Bbb R} K < \infty$ which both are absent from Witt's reasoning. I interpret Witt as claiming that his argument works in the much more interesting case $\dim_{\Bbb R} K =\infty$. -- Ebbinghaus himself claims that Witt's proof is "of course, the proof mentioned [on p. 242] based on the exponential function". I doubt this "of course". If Witt wanted to prove the theorem with an explicit exponential series, why would he not write that but a differential equation? Also, at the point (p. 242) where Ebbinghaus discusses that proof of Gelfand-Mazur via the exponential, he admits that a proof of the exp-log correspondence "is incidentally somewhat troublesome, because we have to consider a power series whose terms are power series", which reenforces my belief that Witt might have had a slightly different argument in mind.
Note 4: Witt's paper has four references, two of which are Ostrowski's and Mazur's papers with the respective theorems. He also refers to
E. R. Lorch, The theory of analytic functions in normal abelian vector rings. Trans. Amer. Math. Soc. 54, pp. 414–425 (1943) (thanks Daniele Tampieri for the link)
but only by saying that it presents a different proof via imitating complex function theory over $K(i)$ (as the function $f(z) = (z-a)^{-1}$ for $a \in K \setminus \Bbb C$ would be a bounded entire function and thus contradict Liouville's theorem). Incidentally, Lorch's paper quotes Mazur (Thms 3/4 p. 417) but also does define the logarithm as a path integral starting from the unit element (p. 422).
The last remaining reference is
E. Hille, Functional Analysis and Semi-Groups (Amer. Math. Soc. Coll. Publ. XXXI). New York 1948, pp. 474–475
which Dan Petersen scanned (thanks!), see comments. Unfortunately, I do not see any clue in there, it just seems to refer back to Lorch and Mazur and the "Liouville-style" proof.
