avewright/proofwiki-math huggingface dataset:
Theorem: Principle of Mathematical Induction/Well-Ordered Integral Domain

Let $\struct {D, +, \times, \le}$ be a well-ordered integral domain whose zero is $0_D$.
Let the unity of $D$ be $1_D$.
Let $S \subseteq D$ be such that:
:$1_D \in S$
:$a \in S \implies a + 1_D \in S$
Then:
:$D_{> 0_D} \subseteq S$
where $D_{> 0_D}$ denotes all the elements $d \in D$ such that $\map P d$.
That is, $D_{> 0_D}$ is the set of all (strictly) positive elements of $D$.

Proof:
Let $\overline S$ be the set of all elements of $D_{> 0_D}$ that are not in $S$:
:$\overline S = D_{> 0_D} \setminus S$
{{AimForCont}} $\overline S$ is not empty.
Then as $D$ is well-ordered, it follows that $\overline S$ has a minimal element, which we will call $m$.
Then $m - 1 \notin \overline S$.
But $1 < m$ as $1 \in S$, and from One Succeeds Zero in Well-Ordered Integral Domain, $1$ is the minimal positive element of $D$.
So $0 < m - 1$ and so $m - 1$ is strictly positive.
Because $m - 1 \notin \overline S$, it follows that $m - 1 \in S$.
By construction of $S$ it follows that $m \in S$.
So $m \in S$ and $m \in \overline S$, that is:
:$m \notin S$
From this contradiction we deduced that there can therefore be no such $m$.
Hence:
:$D_{\ge 0_D} \setminus S = \O$.
From Set Difference with Superset is Empty Set it follows that $D_{\ge 0_D} \subseteq S$.
{{qed}}
Theorem: Multiple of Divisor in Integral Domain Divides Multiple

Let $\struct {D, +, \times}$ be an integral domain.
Let $a, b, c \in D$.
Let $a \divides b$, where $\divides$ denotes divisibility.
Then $a \times c$ is a divisor of $b \times c$.

Proof:
By definition, if $a \divides b$ then $\exists d \in D: a \times d = b$.
Then $\paren {a \times d} \times c = b \times c$, that is:
:$\paren {a \times c} \times d = b \times c$
which follows because $\times$ is commutative and associative in an integral domain.
Hence the result.
{{qed}}
Theorem: Integer Divisor Results/One Divides all Integers

{{begin-eqn}}
{{eqn | l = 1
      | o = \divides
      | r = n
}}
{{eqn | l = -1
      | o = \divides
      | r = n
}}
{{end-eqn}}

Proof:
From Integers form Integral Domain, the concept '''divisibility''' is fully applicable to the integers.
Therefore this result follows directly from Unity Divides All Elements.
{{qed}}
Theorem: Integer Divisor Results/Integer Divides Itself

:$n \divides n$

Proof:
From Integer Multiplication Identity is One:
:$\forall n \in \Z: 1 \cdot n = n = n \cdot 1$
thus demonstrating that $n$ is a divisor of itself.
{{qed}}
Theorem: Integer Divisor Results/Integer Divides Itself

:$n \divides n$

Proof:
As the set of integers form an integral domain, the concept '''divides''' is fully applicable to the integers.
Therefore this result follows directly from Element of Integral Domain is Divisor of Itself.
{{qed}}
Theorem: Integer Divisor Results/Integer Divides its Negative

{{begin-eqn}}
{{eqn | l = n
      | o = \divides
      | r = -n
}}
{{eqn | l = -n
      | o = \divides
      | r = n
}}
{{end-eqn}}

Proof:
From Integers form Integral Domain, the integers are an integral domain.
Hence we can apply Product of Ring Negatives:
:$\forall n \in \Z: \exists -1 \in \Z: n = \paren {-1} \times \paren {-n}$
and Product with Ring Negative:
:$\forall n \in \Z: \exists -1 \in \Z: -n = \paren {-1} \times \paren n$
{{qed}}
Theorem: Integer Divisor Results/Integer Divides its Absolute Value

{{begin-eqn}}
{{eqn | l = n
      | o = \divides
      | r = \size n
}}
{{eqn | l = \size n
      | o = \divides
      | r = n
}}
{{end-eqn}}
where:
:$\size n$ is the absolute value of $n$
:$\divides$ denotes divisibility.

Proof:
Let $n > 0$.
Then $\size n = n$ and Integer Divides Itself applies.
Let $n = 0$.
Then Integer Divides Itself holds again.
Let $n < 0$.
Then $\size n = -n$ and Integer Divides its Negative applies.
{{qed}}
Category:Divisors
Category:Absolute Value Function
qwokq3o9x7dlgf3p8phr3bj8v8ig1wr
Theorem: Integer Divisor Results/Integer Divides Zero

:$n \divides 0$

Proof:
From Integers form Integral Domain, the concept '''divides''' is fully applicable to the integers.
Therefore this result follows directly from Element of Integral Domain Divides Zero.
{{qed}}
Theorem: Integer Divisor Results/Divisors of Negative Values

:$m \divides n \iff -m \divides n \iff m \divides -n \iff -m \divides -n$

Proof:
Let $m \divides n$.
From Integer Divides its Negative, we have $-m \divides m$.
From Divisor Relation on Positive Integers is Partial Ordering it follows that $-m \divides n$.
From Integer Divides its Negative, we have $n \divides -n$.
From Divisor Relation on Positive Integers is Partial Ordering it follows that $m \divides -n$.
From above, we have $-m \divides n$.
From Integer Divides its Negative, we have $n \divides -n$.
From Divisor Relation on Positive Integers is Partial Ordering it follows that $-m \divides -n$.
The reverse implications follow similarly.
{{qed}}
Theorem: Divisors of One

The only divisors of $1$ are $1$ and $-1$.
That is:
:$a \divides 1 \iff a = \pm 1$

Proof:
=== Necessary Condition ===
Let $a = \pm 1$.
From Integer Divides Itself we have that $1 \divides 1$.
From Integer Divides its Negative we have that $-1 \divides 1$.
{{qed|lemma}}
Theorem: Divisor Relation is Antisymmetric

''Divides'' is a antisymmetric relation on $\Z_{>0}$, the set of positive integers.
That is:
:$\forall a, b \in \Z_{>0}: a \divides b \land b \divides a \implies a = b$

Proof:
Let $a, b \in \Z_{> 0}$ such that $a \divides b$ and $b \divides a$.
Then:
{{begin-eqn}}
{{eqn | l = a \divides b
      | o = \implies
      | r = \size a \le \size b
      | c = Absolute Value of Integer is not less than Divisors
}}
{{eqn | l = b \divides a
      | o = \implies
      | r = \size b \le \size a
      | c = Absolute Value of Integer is not less than Divisors
}}
{{eqn | o = \leadsto
      | r = \size a = \size b
}}
{{end-eqn}}
If we restrict ourselves to the domain of positive integers, we can see:
:$\forall a, b \in \Z_{>0}: a \divides b \land b \divides a \implies a = b$
{{qed}}
Theorem: Divisor Relation is Antisymmetric

''Divides'' is a antisymmetric relation on $\Z_{>0}$, the set of positive integers.
That is:
:$\forall a, b \in \Z_{>0}: a \divides b \land b \divides a \implies a = b$

Proof:
Let $a \divides b$ and $b \divides a$.
Then from Divisor Relation is Antisymmetric:
:$\size a = \size b$
The result follows from Integer Divides its Negative and Integer Divides its Absolute Value.
{{qed}}
Theorem: Divisor Relation is Antisymmetric

''Divides'' is a antisymmetric relation on $\Z_{>0}$, the set of positive integers.
That is:
:$\forall a, b \in \Z_{>0}: a \divides b \land b \divides a \implies a = b$

Proof:
Let $a \divides b$ and $b \divides a$.
Then by definition of divisor:
:$\exists c, d \in \Z: a c = b, b d = a$
Thus:
{{begin-eqn}}
{{eqn | l = a c d
      | r = a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = c d
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = d
      | r = \pm 1
      | c = Divisors of One
}}
{{eqn | ll= \leadsto
      | l = a
      | r = \pm b
      | c = as $a = b d$
}}
{{end-eqn}}
{{qed}}
Theorem: Real Function is Continuous at Point iff Oscillation is Zero

Let $f: D \to \R$ be a real function where $D \subseteq \R$.
Let $x$ be a point in $D$.
Let $N_x$ be the set of open subset neighborhoods of $x$.
Let $\map {\omega_f} x$ be the oscillation of $f$ at $x$:
:$\map {\omega_f} x = \ds \inf \set {\map {\omega_f} {I \cap D}: I \in N_x}$
where $\map {\omega_f} {I \cap D}$ denotes the oscillation of $f$ on $I \cap D$:
:$\map {\omega_f} {I \cap D} = \ds \sup \set {\size {\map f y - \map f z}: y, z \in I \cap D}$
Then $\map {\omega_f} x = 0$ {{iff}} $f$ is continuous at $x$.

Proof:
=== Necessary Condition ===
Let $\map {\omega_f} x = 0$.
Let $\epsilon > 0$.
Suppose that $\forall I: I \in N_x: \map {\omega_f} {I \cap D} \ge \epsilon$.
Then by definition of oscillation at point, $\map {\omega_f} x \ge \epsilon$. 
This contradicts $\map {\omega_f} x = 0$.
From this contradiction we deduce that:
:$\exists J: J \in N_x: \map {\omega_f} {J \cap D} < \epsilon$
For this particular $J$, there is an open set $O \subset J$ that contains $x$ by the definition of open subset neighborhood.
Therefore, a $\delta \in \R_{>0}$ exists such that $\openint {x - \delta} {x + \delta}$ is a subset of $O$.
So, if $y$ satisfies:
:$\size {x - y} < \delta$
Then:
:$y \in J$
and, if $y \in D$:
:$\size {\map f x - \map f y} \le \map {\omega_f} {J \cap D}$
Since $\map {\omega_f} {J \cap D} < \epsilon$ it follows by the definition of continuity that $f$ is continuous at $x$.
{{qed|lemma}}
Theorem: Quadratic Integers over 2 are Not a Field

Let $\Z \sqbrk {\sqrt 2}$ denote the set of quadratic integers over $2$:
:$\Z \sqbrk {\sqrt 2} := \set {a + b \sqrt 2: a, b \in \Z}$
that is, all (real) numbers of the form $a + b \sqrt 2$ where $a$ and $b$ are integers.
Then the algebraic structure:
:$\struct {\Z \sqbrk {\sqrt 2}, +, \times}$
where $+$ and $\times$ are addition and multiplication on real numbers, is '''not''' a field.

Proof:
We start from the result Quadratic Integers over 2 form Subdomain of Reals.
We have from that result that $1 + 0 \sqrt 2$ is the unity.
Now consider a representative element $a + b \sqrt 2 \in \Z \sqbrk {\sqrt 2}$.
From Difference of Two Squares we have:
:$\paren {a + b \sqrt 2} \paren {a - b \sqrt 2} = a^2 - 2 b^2$
which leads to:
:$\paren {a + b \sqrt 2} \paren {\dfrac {a - b \sqrt 2} {a^2 - 2 b^2} } = 1$
so demonstrating that the product inverse of $\paren {a + b \sqrt 2}$ is $\dfrac a {a^2 - 2b^2} + \dfrac {b \sqrt 2} {a^2 - 2 b^2}$.
But for any two given integers $a$ and $b$, the values $\dfrac a {a^2 - 2 b^2}$ and $\dfrac b {a^2 - 2 b^2}$ are not in general integers.
For instance, when $a = 3$ and $b = 4$ we get:
:$\dfrac a {a^2 - 2 b^2} = \dfrac 3 {23}$ and $\dfrac b {a^2 - 2 b^2} = \dfrac 4 {23}$
(unless I've got my sums wrong).
So not every element of $\struct {\Z \sqbrk {\sqrt 2}, +, \times}$ has a product inverse, demonstrating that $\struct {\Z \sqbrk {\sqrt 2}, +, \times}$ is not a field.
{{qed}}
Theorem: Real Numbers of Type Rational a plus b root 2 form Field

Let $\Q \sqbrk {\sqrt 2}$ denote the set:
:$\Q \sqbrk {\sqrt 2} := \set {x \in \R: x = a + b \sqrt 2: a, b \in \Q}$
that is, all numbers of the form $a + b \sqrt 2$ where $a$ and $b$ are rational numbers.
Then the algebraic structure:
:$\struct {\Q \sqbrk {\sqrt 2}, +, \times}$
where $+$ and $\times$ are conventional addition and multiplication on real numbers, is a field.

Proof:
{{improve|Use subfield test}}
By definition, $\Q \sqbrk {\sqrt 2} \subseteq \R$ where $\R$ is the set of real numbers.
Thus $+$ and $\times$ on $\struct {\Q \sqbrk {\sqrt 2}, +, \times}$ are well-defined.
Theorem: Characteristic of Ring of Integers Modulo Prime

Let $\struct {\Z_p, +, \times}$ be the ring of integers modulo $p$, where $p$ is a prime number.
The characteristic of $\struct {\Z_p, +, \times}$ is $p$.

Proof:
From Ring of Integers Modulo Prime is Field we have that $\struct {\Z_p, +, \times}$ is a field.
So Characteristic of Finite Ring with No Zero Divisors applies, and so the characteristic of $\struct {\Z_p, +, \times}$ is prime.
The result follows.
{{qed}}
Theorem: Gamma Function Extends Factorial

:$\forall n \in \N: \map \Gamma {n + 1} = n!$

Proof:
For $n = 0$:
{{begin-eqn}}
{{eqn | l = \map \Gamma 1
      | r = \int_0^\infty e^{-t} \rd t
      | c = {{Defof|Integral Form of Gamma Function|Gamma Function}}
}}
{{eqn | r = \bigintlimits {-e^{-t} } 0 \infty
      | c =
}}
{{eqn | r = 0 - \paren {-1}
}}
{{eqn | r = 1
}}
{{end-eqn}}
Then by Gamma Difference Equation:
:$\forall z \in \Z_{> 0}: \map \Gamma {z + 1} = z \, \map \Gamma z$
Hence the result.
{{qed}}
Theorem: Uniform Limit of Analytic Functions is Analytic

Let $U$ be an open subset of $\C$.
Let $\sequence {f_n}_{n \mathop \in \N}$ be a sequence of analytic functions $f_n : U \to \C$.
Let $\sequence {f_n}$ converge locally uniformly to $f$ on $U$.
Then $f$ is analytic.

Proof:
Let $z \in U$.
By definition of locally uniform convergence, there is an $\epsilon > 0$ so that:
:$\map {B_\epsilon} z \subset U$
and $f_n$ converges uniformly on $\map {B_\epsilon} z$.
Let $\gamma$ be any simple closed curve in $\map {B_\epsilon} z$.
Then $f_n \to f$ uniformly on $\gamma$, because $\gamma \subset \map {B_\epsilon} z$.
Thus by Definite Integral of Limit of Uniformly Convergent Sequence of Integrable Functions, we have:
:$\ds \lim_{n \mathop \to \infty} \oint_\gamma \map {f_n} z \rd z = \oint_\gamma \map f z \rd z$
Since each $f_n$ is analytic, we have by Cauchy-Goursat Theorem that:
:$\ds \forall n \in \N: \oint_\gamma \map {f_n} z \rd z = 0$
So we conclude also that:
:$\ds \oint_\gamma \map f z \rd z = 0$
Since $\gamma$ was arbitrary, we have by Morera's Theorem that $f$ is analytic in $\map {B_\epsilon} z$.
Since $z$ was arbitrary, $f$ is analytic on all of $U$.
{{qed}}
Theorem: Triangle Inequality for Integrals/Complex

Let $\closedint a b$ be a closed real interval.
Let $f: \closedint a b \to \C$ be a continuous complex function.
Then:
:$\ds \size {\int_a^b \map f t \rd t} \le \int_a^b \size {\map f t} \rd t$
where the first integral is a complex Riemann integral, and the second integral is a definite real integral.

Proof:
Define:
:$z \in \C$ as the value of the complex Riemann integral:
::$z = \ds \int_a^b \map f t \rd t$
:$r \in \hointr 0 \to$ as the modulus of $z$
:$\theta \in \hointr 0 {2 \pi}$ as the argument of $z$.
From Modulus and Argument of Complex Exponential:
:$z = re^{i \theta}$
Then:
{{begin-eqn}}
{{eqn | l = r
      | r = z e^{-i \theta}
      | c = Reciprocal of Complex Exponential
}}
{{eqn | r = \int_a^b e^{-i \theta} \map f t \rd t
      | c = Linear Combination of Complex Integrals
}}
{{eqn | r = \int_a^b \map \Re {e^{-i \theta} \map f t} \rd t + i \int_a^b \map \Im {e^{-i \theta} \map f t} \rd t
      | c = {{Defof|Complex Riemann Integral}}
}}
{{end-eqn}}
As $r$ is wholly real, we have:
:$\ds 0 = \map \Im r = \int_a^b \map \Im {e^{-i \theta} \map f t} \rd t$
Then:
{{begin-eqn}}
{{eqn | l = r
      | r = \int_a^b \map \Re {e^{-i \theta} \map f t} \rd t
}}
{{eqn | o = \le
      | r = \int_a^b \size {\map \Re {e^{-i \theta} \map f t} } \rd t
      | c = Absolute Value of Definite Integral
}}
{{eqn | o = \le
      | r = \int_a^b \size {e^{-i \theta} \map f t} \rd t
      | c = Modulus Larger than Real Part
}}
{{eqn | r = \int_a^b \size {e^{-i \theta} } \size {\map f t} \rd t
}}
{{eqn | r = \int_a^b \size {\map f t} \rd t
      | c = Modulus of Exponential of Imaginary Number is One
}}
{{end-eqn}}
As $\ds r = \size {\int_a^b \map f t \rd t}$ by its definition, the result follows.
{{qed}}
Theorem: Estimation Lemma for Contour Integrals

Let $C$ be a contour.
Let $f: \Img C \to \C$ be a continuous complex function, where $\Img C$ denotes the image of $C$.
Then:
:$\ds \size {\int_C \map f z \rd z} \le \max_{z \mathop \in \Img C} \size {\map f z} \map L C$
where $\map L C$ denotes the length of $C$.

Proof:
By definition of contour, $C$ is a concatenation of a finite sequence $C_1, \ldots, C_n$ of directed smooth curves.
Let $C_k$ be parameterized by the smooth path $\gamma_k: \closedint {a_k} {b_k} \to \C$ for all $k \in \set {1, \ldots, n}$.
Then:
{{begin-eqn}}
{{eqn | l = \size {\int_C \map f z \rd z}
      | r = \size {\sum_{k \mathop = 1}^n \int_{a_k}^{b_k} \map f {\map {\gamma_k} t} \map {\gamma_k'} t \rd t}
      | c = {{Defof|Complex Contour Integral}}
}}
{{eqn | o = \le
      | r = \sum_{k \mathop = 1}^n \size {\int_{a_k}^{b_k} \map f {\map {\gamma_k} t} \map {\gamma_k'} t \rd t}
      | c = Triangle Inequality for Complex Numbers
}}
{{eqn | o = \le
      | r = \sum_{k \mathop = 1}^n \int_{a_k}^{b_k} \size {\map f {\map {\gamma_k} t} } \size {\map {\gamma_k'} t} \rd t
      | c = Modulus of Complex Integral
}}
{{eqn | o = \le
      | r = \sum_{k \mathop = 1}^n \max_{t \mathop \in \closedint {a_k} {b_k} } \size {\map f {\map {\gamma_k} t} } \int_{a_k}^{b_k} \size {\map {\gamma_k'} t} \rd t
      | c = Linear Combination of Definite Integrals
}}
{{eqn | o = \le
      | r = \sum_{k \mathop = 1}^n \max_{z \mathop \in \Img C} \size {\map f z} \int_{a_k}^{b_k} \size {\map {\gamma_k'} t} \rd t
      | c = as $\map {\gamma_k} t \in \Img C$
}}
{{eqn | r = \max_{z \mathop \in \Img C} \size {\map f z} \map L C
      | c = {{Defof|Length of Contour (Complex Plane)}}
}}
{{end-eqn}}
{{qed}}
Theorem: Jensen's Formula

Let $S$ be an open subset of the complex plane containing the closed disk:
:$D_r = \set {z \in \C : \cmod z \le r}$
of radius $r$ about $0$.
Let $f: S \to \C$ be holomorphic on $S$. 
Let $f$ have no zeroes on the circle $\cmod z = r$.
Let $\map f 0 \ne 0$.
Let $\rho_1, \ldots, \rho_n$ be the zeroes of $f$ in $D_r$, counted with multiplicity.
Then:
:$(1): \quad \ds \frac 1 {2 \pi} \int_0^{2 \pi} \ln \cmod {\map f {r e^{i \theta} } } \rd \theta = \ln \cmod {\map f 0} + \sum_{k \mathop = 1}^n \paren {\ln r - \ln \size {\rho_k} }$

Proof:
Write:
:$\map f z = \paren {z - \rho_1} \dotsm \paren {z - \rho_n} \map g z$
so $\map g z \ne 0$ for $z \in D_r$.
It is sufficient to check the equality for each factor of $f$ in this expansion.
First let:
:$\map h z = z - \rho_k$
for some $k \in \set {1, \ldots, n}$.
Making use of the substitution $u = r e^{i \theta} - \rho_k$ we find that:
:$\ds \frac 1 {2 \pi} \int_0^{2 \pi} \ln \size {\map h {r e^{i \theta} } } \rd \theta = \frac 1 {2 \pi i} \int_\gamma \frac {\ln \size u} {u + \rho_k} \rd u$
where $\gamma$ is a circle of radius $r$ centred at $-\rho_k$, traversed anticlockwise.
{{mistake|I think this last statement is False! The circle is not centered at 0 so $\size u$ is not constant.}}
On this circle, $\ln \size u = \ln r$ is constant, and we have that:
:$\ds \int_\gamma \frac 1 {u + \rho_k} \rd u = \int_{\size z \mathop = r} \frac {\d u} u = 2 \pi i$
Therefore the {{LHS}} of $(1)$ is $\ln r$ as required.
To show equality for $\map g z$, first observe that by Cauchy's Residue Theorem:
:$\ds \int_{\size z = r} \frac {\ln \map g z} z \rd z = 2 \pi i \ln \map g 0$
{{explain|Is $\ln \map g z$ well-defined?}}
Therefore substituting $z = r e^{i \theta}$ we have
:$\ds 2 \pi i \ln \map g 0 = i \int_0^{2 \pi} \ln \map g {r e^{i \theta} } \rd \theta$
Comparing the imaginary parts of this equality we see that:
:$\ds \frac 1 {2 \pi} \int_0^{2 \pi} \ln \size {\map g {r e^{i \theta} } } \rd \theta = \ln \size {\map g 0}$
as required.
{{qed}}
Theorem: Jensen's Formula

Let $S$ be an open subset of the complex plane containing the closed disk:
:$D_r = \set {z \in \C : \cmod z \le r}$
of radius $r$ about $0$.
Let $f: S \to \C$ be holomorphic on $S$. 
Let $f$ have no zeroes on the circle $\cmod z = r$.
Let $\map f 0 \ne 0$.
Let $\rho_1, \ldots, \rho_n$ be the zeroes of $f$ in $D_r$, counted with multiplicity.
Then:
:$(1): \quad \ds \frac 1 {2 \pi} \int_0^{2 \pi} \ln \cmod {\map f {r e^{i \theta} } } \rd \theta = \ln \cmod {\map f 0} + \sum_{k \mathop = 1}^n \paren {\ln r - \ln \size {\rho_k} }$

Proof:
Write
:$\map f z = \dfrac {r^2 - z \overline {\rho_1} } {r \paren {z - \rho_1} } \cdots \dfrac {r^2 - z \overline {\rho_n} } {r \paren {z - \rho_n} } \map g z$
so $\map g z \ne 0$ for $z \in D_r$.
{{explain|Why can you write like this? Looks wrong, because the zeros do not correspond. For example, insert $z{{=}}\rho_1$ in both sides.}}
It is sufficient to check equality for each factor of $f$ in this expansion.
When $\cmod z = r$, we have:
:$\dfrac 1 z = \dfrac {\overline z} {r^2}$
and:
:$\cmod {\dfrac z r} = 1$
where $\overline z$ denotes the complex conjugate of $z$.
So:
{{begin-eqn}}
{{eqn | l = \cmod {\frac {r^2 - z \overline {\rho_k} } {r \paren {z - \rho_k} } }
      | r = \frac {\cmod {r^2 - \overline z \rho_k} } {\cmod {r \paren {z - \rho_k} } }
      | c = 
}}
{{eqn | r = \frac {\cmod {1 - \overline z \rho_k / r^2} } {\cmod {z / r - \rho_k / r} }
      | c = 
}}
{{eqn | r = \frac {\cmod {1 - \overline z \rho_k / r^2} } {\cmod {1 - \rho_k / z} }
      | c = 
}}
{{eqn | r = \frac {\cmod {1 - \overline z \rho_k / r^2} } {\cmod {1 - \overline z \rho_k / r^2} }
      | c = 
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
so the {{LHS}} is $0$.
{{explain|What are you doing? The calculation above looks wrong and the conclusion that {{LHS}} is zero because {{RHS}} is one does not make sense. Please explain more.}}
Moreover:
:$\\ln \cmod {\dfrac {r^2 - 0 \overline {\rho_k} } {r \paren {0 - \rho_k} } } = \ln \cmod {\rho_k} - \ln r$
so the {{RHS}} is $0$.
Therefore, the formula holds for $\dfrac {r^2 - z \overline {\rho_k} } {r \paren {z - \rho_k} }$.
Since:
:$r^2 - z \overline {\rho_i} = 0 \implies \cmod z = r^2 / \cmod {\overline {\rho_i} } > r$
it follows that $\map g z$ is holomorphic without zeroes on $D_r$.
So the {{RHS}} is $\ln \size {\map g 0}$.
On the other hand, by the mean value property:
:$\ds \dfrac 1 {2 \pi} \int_0^{2 \pi} \ln \size {\map g {r e^{i \theta} } } \rd \theta = \ln \map g 0$
as required.
{{qed}}
Theorem: Jensen's Formula

Let $S$ be an open subset of the complex plane containing the closed disk:
:$D_r = \set {z \in \C : \cmod z \le r}$
of radius $r$ about $0$.
Let $f: S \to \C$ be holomorphic on $S$. 
Let $f$ have no zeroes on the circle $\cmod z = r$.
Let $\map f 0 \ne 0$.
Let $\rho_1, \ldots, \rho_n$ be the zeroes of $f$ in $D_r$, counted with multiplicity.
Then:
:$(1): \quad \ds \frac 1 {2 \pi} \int_0^{2 \pi} \ln \cmod {\map f {r e^{i \theta} } } \rd \theta = \ln \cmod {\map f 0} + \sum_{k \mathop = 1}^n \paren {\ln r - \ln \size {\rho_k} }$

Proof:
{{WLOG}}, assume that $r = 0$. 
{{explain|I don't see why $r {{=}} 0$ is WLOG?}}
Write:
:$\map f z = \map {B_{\rho_1} } z \dotsm \map {B_{\rho_n} } z \map g z$
where $\map {B_\rho} z := \dfrac {z - \rho} {1 - z \overline \rho}$ is the Blaschke factor at $\rho$.
So:
:$\map g z$ is holomorphic and nonzero in $D_r$
and:
:each $\map {B_{\rho_i} } z$ is holomorphic and has a simple zero $\rho_i$ inside $D_r$.
It is sufficient to check the equality for each factor of $f$ in this expansion.
First let:
:$\map h z = \map {B_{\rho_k} } z = \dfrac {z - \rho_k} {1 - z \overline {\rho_k} }$
for some $k \in \set {1, \ldots, n}$.
Note that:
:$\size {\map h z} \equiv 1$ for $\size z = 1$
so the integral is $0$.
Also:
:$\map {B_{\rho_k} } 0 = \rho_k$
so the equality holds in this case.
{{explain|Why do the above statements hold? All statements in the above line look wrong.}}
To show equality for $\map g z$, first observe that by the Cauchy's Residue Theorem:
:$\ds \int_{\size z \mathop = r} \frac {\ln \map g z} z \rd z = 2 \pi i \ln \map g 0$
{{explain|Is $\ln \map g z$ well-defined?}}
Therefore substituting $z = r e^{i \theta}$ we have:
:$\ds 2 \pi i \ln \map g 0 = i \int_0^{2 \pi} \ln \map g {r e^{i \theta} } \rd \theta$
Comparing the imaginary parts of this equality we see that:
:$\ds \frac 1 {2 \pi} \int_0^{2 \pi} \ln \size {\map g {r e^{i \theta} } } \rd \theta = \ln \size {\map g 0}$
as required.
{{qed}}