# The Top 100 Theorems in Isabelle

The following are the theorems from this list proved so far in the Isabelle proof assistant.

If you have proved additional ones or know of any, please send me email so I can add them here.

If the theorem is not part of the Isabelle distribution, the entry will usually contain a link to the repository that does. The list does not automatically track the most recent version of each theorem. If you find one that that is out of date and would like me to update it, let me know.

## 1. Square Root of 2 is Irrational

```theorem sqrt_prime_irrational: "prime p ⟹ sqrt (real p) ∉ ℚ"

corollary sqrt_2_not_rat: "sqrt 2 ∉ ℚ"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Sqrt.html

## 2. Fundamental Theorem of Algebra

```lemma fundamental_theorem_of_algebra:
assumes nc: "¬ constant (poly p)"
shows "∃z::complex. poly p z = 0"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-Computational_Algebra/Fundamental_Theorem_Algebra.html

## 3. Denumerability of the Rational Numbers

```theorem rat_denum: "∃f :: nat ⇒ rat. surj f"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Countable.html

## 4. Pythagorean Theorem

```lemma pythagoras:
fixes a b c :: "'a :: real_inner"
assumes "orthogonal (b - a) (c - a)"
shows   "dist b c ^ 2 = dist a b ^ 2 + dist a c ^ 2"
```

## 5. Prime Number Theorem

Avigad et al. formalised the elementary Erdős–Selberg proof:

```definition pi :: "nat ⇒ real"
where "pi x = real (card {y::nat. y ≤ x ∧ prime y})"

lemma PrimeNumberTheorem: "(λx. pi x * ln (real x) / real x) ⇢ 1"
```

A formalisation by Eberl and Paulson of the shorter analytic proof is available in the AFP:

```definition primes_pi :: "real ⇒ real" where
"primes_pi x = real (card {p::nat. prime p ∧ p ≤ x})"

corollary prime_number_theorem: "primes_pi ∼[at_top] (λx. x / ln x)"
```

https://www.isa-afp.org/entries/Prime_Number_Theorem.html

## 6. Gödel’s Incompleteness Theorem

```theorem Goedel_I:
assumes "¬ {} ⊢ Fls"
obtains δ where
"{} ⊢ δ IFF Neg (PfP ⌈δ⌉)"
"¬ {} ⊢ δ"
"¬ {} ⊢ Neg δ"
"eval_fm e δ"
"ground_fm δ"

theorem Goedel_II:
assumes "¬ {} ⊢ Fls"
shows "¬ {} ⊢ Neg (PfP ⌈Fls⌉)"
```

https://isa-afp.org/entries/Incompleteness.shtml

## 7. Law of Quadratic Reciprocity

```theorem Quadratic_Reciprocity:
assumes "prime p" "2 < p" "prime q" "2 < q" "p ≠ q"
shows "Legendre p q * Legendre q p = (-1) ^ ((p - 1) div 2 * ((q - 1) div 2))"
```

## 8. The Impossibility of Trisecting the Angle and Doubling the Cube

```theorem impossibility_of_doubling_the_cube:
"x^3 = 2 ⟹ (Point x 0) ∉ constructible"

theorem impossibility_of_trisecting_angle_pi_over_3:
"Point (cos (pi / 9)) 0 ∉ constructible"
```

https://isa-afp.org/entries/Impossible_Geometry.shtml

## 9. The Area of a Circle

```theorem content_ball:
fixes c :: "'a :: euclidean_space"
assumes "r ≥ 0"
shows   "content (ball c r) = pi powr (DIM('a) / 2) / Gamma (DIM('a) / 2 + 1) * r ^ DIM('a)"

corollary content_circle:
"r ≥ 0 ⟹ content (ball c r :: (real ^ 2) set) = r ^ 2 * pi"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Ball_Volume.html

## 10. Euler’s Generalisation of Fermat’s Little Theorem

```lemma euler_theorem:
fixes a m :: nat
assumes "coprime a m"
shows "[a ^ totient m = 1] (mod m)"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-Number_Theory/Residues.html

## 11. The Infinitude of Primes

```lemma primes_infinite: "¬finite {p::nat. prime p}"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-Computational_Algebra/Primes.html

## 12. The Independence of the Parallel Postulate

https://isa-afp.org/entries/Tarskis_Geometry.shtml

## 14. Euler’s Summation of 1 + (1/2)^2 + (1/3)^2 + ….

```theorem inverse_squares_sums: "(λn. 1 / (n + 1)\<^sup>2) sums (pi\<^sup>2 / 6)"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Gamma_Function.html

## 15. Fundamental Theorem of Integral Calculus

```theorem fundamental_theorem_of_calculus:
fixes f :: "real ⇒ 'a::banach"
assumes "a ≤ b"
and   "⋀x. x ∈ {a..b} ⟹ (f has_vector_derivative f' x) (at x within {a..b})"
shows   "(f' has_integral (f b - f a)) {a..b}"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Henstock_Kurzweil_Integration.html

## 17. DeMoivre’s Theorem

```lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"

lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL/Complex.html

## 18. Liouville’s Theorem and the Construction of Transcendental Numbers

```corollary transcendental_liouville_constant:
"¬algebraic (standard_liouville (λ_. 1) 10)"
```

https://isa-afp.org/entries/Liouville_Numbers.shtml

## 19. Lagrange’s Four-Square Theorem

```theorem four_squares: "∃a b c d::nat. n = a\<^sup>2 + b\<^sup>2 + c\<^sup>2 + d\<^sup>2"
```

https://www.isa-afp.org/entries/SumSquares.html

## 20. All Primes (1 mod 4) Equal the Sum of Two Squares

```theorem two_squares:
assumes "prime (p :: nat)"
shows   "(∃a b. p = a\<^sup>2 + b\<^sup>2) = [p ≠ 3] (mod 4)
```

https://www.isa-afp.org/entries/SumSquares.html

## 21. Green’s theorem

```lemma GreenThm_typeI_typeII_divisible_region:
assumes valid_typeI_div: "valid_typeI_division s twoChain_typeI" and
valid_typeII_div: "valid_typeII_division s twoChain_typeII" and
f_analytically_valid: "∀twoC ∈ twoChain_typeI. analytically_valid (cubeImage twoC) (%x. (F x) ∙ i) j"
"∀twoC ∈ twoChain_typeII. analytically_valid (cubeImage twoC) (%x. (F x) ∙ j) i" and
only_vertical_division:
"only_vertical_division one_chain_typeI twoChain_typeI"
"boundary_chain one_chain_typeI" and
only_horizontal_division:
"only_horizontal_division one_chain_typeII twoChain_typeII"
"boundary_chain one_chain_typeII" and
typeI_and_typII_one_chains_have_common_subdiv:
"common_boundary_sudivision_exists one_chain_typeI one_chain_typeII"
shows "integral s (%x. partial_vector_derivative (%x. (F x) ∙ j) i x - partial_vector_derivative (%x. (F x) ∙ i) j x) = one_chain_line_integral F {i, j} one_chain_typeI"
"integral s (%x. partial_vector_derivative (%x. (F x) ∙ j) i x - partial_vector_derivative (%x. (F x) ∙ i) j x) = one_chain_line_integral F {i, j} one_chain_typeII"
```

https://www.isa-afp.org/entries/Green.html

## 22. The Non-Denumerability of the Continuum

```theorem real_non_denum: "∄f :: nat ⇒ real. surj f"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Continuum_Not_Denumerable.html

## 23. Formula for Pythagorean Triples

```theorem nat_euclid_pyth_triples:
fixes a b c :: nat
assumes "coprime a b" "odd a" "a⇧2 + b⇧2 = c⇧2"
shows   "∃p q. a = p⇧2 - q⇧2 ∧ b = 2 * p * q ∧ c = p⇧2 + q⇧2 ∧ coprime p q"
```

https://www.isa-afp.org/entries/Fermat3_4.html

## 25. Schroeder-Bernstein Theorem

```theorem Schroeder_Bernstein:
fixes f :: "'a ⇒ 'b" and g :: "'b ⇒ 'a"
and A :: "'a set" and B :: "'b set"
assumes "inj_on f A" and "f ` A ⊆ B"
and   "inj_on g B" and "g ` B ⊆ A"
shows   "∃h. bij_betw h A B"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL/Inductive.html

## 26. Leibnitz’s Series for Pi

```theorem pi_series:
"pi / 4 = (∑ k. (-1)^k * 1 / real (k*2+1))"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL/Transcendental.html

## 27. Sum of the Angles of a Triangle

```lemma angle_sum_triangle:
assumes "a ≠ b ∨ b ≠ c ∨ a ≠ c"
shows   "angle c a b + angle a b c + angle b c a = pi"
```

https://isa-afp.org/entries/Triangle.shtml

## 30. The Ballot Problem

```lemma
"valid_countings a b = (if a ≤ b then (if b = 0 then 1 else 0) else (a - b) / (a + b) * all_countings a b)"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Ballot.html

## 31. Ramsey’s Theorem

```lemma ramsey: "
∀(s::nat) (r::nat) (YY::'a set) (f::'a set => nat).
infinite YY
∧ (∀X. X <= YY ∧ finite X ∧ card X = r ⟶ f X < s)
⟶ (∃Y' t'.
Y' <= YY
∧ infinite Y'
∧ t' < s
∧ (∃X. X <= Y' ∧ finite X ∧ card X = r ⟶ f X = t'))"
```

https://isa-afp.org/entries/Ramsey-Infinite.shtml

## 34. Divergence of the Harmonic Series

```theorem not_summable_harmonic:
shows "¬summable (λn. 1 / real (n + 1))"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Summation_Tests.html

## 35. Taylor’s Theorem

```theorem taylor:
fixes a :: real and n :: nat and f :: "real ⇒ real"
assumes "n > 0" and "diff 0 = f"
and   "∀m t. m < n ∧ t ∈ {a..b} ⟶ (diff m has_real_derivative diff (m + 1) t) (at t)"
and   "c ∈ {a..b}" and "x ∈ {a..b} - {c}"
shows "∃t. t ∈ open_segment x c ∧
f x = (∑m<n. (diff m c / fact m) * (x - c) ^ m) + (diff n t / fact n) * (x - c) ^ n"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL/MacLaurin.html

## 36. Brouwer Fixed Point Theorem

```lemma brouwer:
fixes f :: "'a::euclidean_space ⇒ 'a"
assumes "compact S" and "convex S" and "S ≠ {}"
and "continuous_on S f"
and "f ` S ⊆ S"
obtains x where "x ∈ S" and "f x = x"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Brouwer_Fixpoint.html

## 37. The Solution of a Cubic

```lemma cubic:
assumes a0: "a ≠ 0"
shows "
let p = (3 * a * c - b^2) / (9 * a^2) ;
q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3);
s = csqrt(q^2 + p^3);
s1 = (if p = 0 then ccbrt(2 * q) else ccbrt(q + s));
s2 = -s1 * (1 + ii * csqrt 3) / 2;
s3 = -s1 * (1 - ii * csqrt 3) / 2
in if p = 0 then
a * x^3 + b * x^2 + c * x + d = 0 ⟷
x = s1 - b / (3 * a) ∨
x = s2 - b / (3 * a) ∨
x = s3 - b / (3 * a)
else
s1 ≠ 0 ∧
(a * x^3 + b * x^2 + c * x + d = 0 ⟷
x = s1 - p / s1 - b / (3 * a) ∨
x = s2 - p / s2 - b / (3 * a) ∨
x = s3 - p / s3 - b / (3 * a))"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Cubic_Quartic.html

## 38. Arithmetic Mean / Geometric Mean

```theorem CauchysMeanTheorem_Eq:
fixes z::"real list"
assumes "pos z"
shows "gmean z = mean z ⟷ het z = 0"
```

https://isa-afp.org/entries/Cauchy.shtml

## 39. Solutions to Pell’s Equation

```theorem pell_solutions:
fixes D :: nat
assumes "∄k. D = k\<^sup>2"
obtains "x\<^sub>0" "y\<^sub>0" :: nat
where   "∀(x::int) (y::int).
x\<^sup>2 - D * y\<^sup>2 = 1 ⟷
(∃n::nat. nat ¦x¦ + sqrt D * nat ¦y¦ = (x\<^sub>0 + sqrt D * y\<^sub>0) ^ n)"

corollary pell_solutions_infinite:
fixes D :: nat
assumes "∄k. D = k\<^sup>2"
shows   "infinite {(x :: int, y :: int). x\<^sup>2 - D * y\<^sup>2 = 1}"
```

https://www.isa-afp.org/entries/Pell.html

## 40. Minkowski’s Fundamental Theorem

```theorem minkowski:
fixes B :: "(real ^ 'n) set"
assumes "convex B" and symmetric: "uminus ` B ⊆ B"
assumes meas_B [measurable]: "B ∈ sets lebesgue"
assumes measure_B: "emeasure lebesgue B > 2 ^ CARD('n)"
obtains x where "x ∈ B" and "x ≠ 0" and "⋀i. x \$ i ∈ ℤ"
```

https://www.isa-afp.org/entries/Minkowskis_Theorem.shtml

## 41. Puiseux’s Theorem

The formal Puiseux series `'a fpxs` for some coefficient type `'a` is defined as the type of functions `rat ⇒ 'a` for which the support is bounded from below and the denominators of the support have a common denominator:

```definition is_fpxs :: "(rat ⇒ 'a :: zero) ⇒ bool" where
"is_fpxs f ⟷ bdd_below (supp f) ∧ (LCM r∈supp f. snd (quotient_of r)) ≠ 0"

typedef (overloaded) 'a fpxs = "{f::rat ⇒ 'a :: zero. is_fpxs f}"
morphisms fpxs_nth Abs_fpxs
```

It is then shown that if `'a` is an algebraically closed field of characteristic `0`, then `'a fpxs` is also an algebraically closed field:

```instance fpxs :: ("{alg_closed_field, field_char_0, field_gcd}") alg_closed_field
```

https://www.isa-afp.org/entries/Formal_Puiseux_Series.html

## 42. Sum of the Reciprocals of the Triangular Numbers

```definition triangle_num :: "nat ⇒ nat" where
"triangle_num n = (n * (n + 1)) div 2"

theorem inverse_triangle_num_sums:
"(λn. 1 / triangle_num (Suc n)) sums 2"
```

https://isabelle.in.tum.de/library/HOL/HOL-ex/Triangular_Numbers.html

## 44. The Binomial Theorem

```theorem binomial_ring:
fixes a b :: "'a :: comm_ring_1"
shows "(a + b) ^ n = (∑k=0..n. of_nat (n choose k) * a ^ k * b ^ (n - k))"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL/Binomial.html

## 45. The Partition Theorem

```theorem Euler_partition_theorem:
"card {p. p partitions n ∧ (∀i. p i ≤ 1)} = card {p. p partitions n ∧ (∀i. p i ≠ 0 ⟶ odd i)}"
```

https://isa-afp.org/entries/Euler_Partition.shtml

## 46. The Solution of the General Quartic Equation

```lemma quartic:
"(y::real)^3 - b * y^2 + (a * c - 4 * d) * y - a^2 * d + 4 * b * d - c^2 = 0 ∧
R^2 = a^2 / 4 - b + y ∧
s^2 = y^2 - 4 * d ∧
(D^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b + 2 * s
else 3 * a^2 / 4 - R^2 - 2 * b + (4 * a * b - 8 * c - a^3) / (4 * R))) ∧
(E^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b - 2 * s
else 3 * a^2 / 4 - R^2 - 2 * b - (4 * a * b - 8 * c - a^3) / (4 * R)))
⟹ x^4 + a * x^3 + b * x^2 + c * x + d = 0 ⟷
x = -a / 4 + R / 2 + D / 2 ∨
x = -a / 4 + R / 2 - D / 2 ∨
x = -a / 4 - R / 2 + E / 2 ∨
x = -a / 4 - R / 2 - E / 2"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Cubic_Quartic.html

## 47. The Central Limit Theorem

```theorem (in prob_space) central_limit_theorem:
fixes
X :: "nat ⇒ 'a ⇒ real" and
μ :: "real measure" and
σ :: real and
S :: "nat ⇒ 'a ⇒ real"
assumes
X_indep: "indep_vars (λi. borel) X UNIV" and
X_integrable: "⋀n. integrable M (X n)" and
X_mean_0: "⋀n. expectation (X n) = 0" and
σ_pos: "σ > 0" and
X_square_integrable: "⋀n. integrable M (λx. (X n x)\<^sup>2)" and
X_variance: "⋀n. variance (X n) = σ\<^sup>2" and
X_distrib: "⋀n. distr M borel (X n) = μ"
defines
"S n ≡ λx. ∑i<n. X i x"
shows
"weak_conv_m (λn. distr M borel (λx. S n x / sqrt (n * σ\<^sup>2)))
(density lborel std_normal_density)"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-Probability/Central_Limit_Theorem.html

## 48. Dirichlet’s Theorem

```theorem Dirichlet:
assumes "n > 1" and "coprime h n"
shows   "infinite {p. prime p ∧ [p = h] (mod n)}"
```

https://isa-afp.org/entries/Dirichlet_L.html

## 49. Cayley-Hamilton Theorem

```theorem Cayley_Hamilton:
fixes A :: "'a∷comm_ring_1^'n∷finite^'n"
shows "evalmat (charpoly A) A = 0"
```

https://isa-afp.org/entries/Cayley_Hamilton.shtml

## 51. Wilson’s Theorem

```lemma wilson_theorem:
assumes "prime p"
shows   "[fact (p - 1) = -1] (mod p)"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-Number_Theory/Residues.html

## 52. The Number of Subsets of a Set

```lemma card_Pow:
"finite A ⟹ card (Pow A) = 2 ^ card A"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL/Power.html

## 53. Pi is Transcendental

```theorem transcendental_pi: "¬algebraic pi"
```

https://www.isa-afp.org/entries/Pi_Transcendental.html

## 54. The Koenigsberg Bridges Problem

```lemma eulerian_split:
assumes "nodes G1 ∩ nodes G2 = {}" "edges G1 ∩ edges G2={}"
"valid_unMultigraph G1" "valid_unMultigraph G2"
"valid_unMultigraph.is_Eulerian_trail  G1 v1 ps1 v1'"
"valid_unMultigraph.is_Eulerian_trail  G2 v2 ps2 v2'"
shows "valid_unMultigraph.is_Eulerian_trail ⦇nodes=nodes G1 ∪ nodes G2,
edges=edges G1 ∪ edges G2 ∪ {(v1',w,v2),(v2,w,v1')}⦈ v1 (ps1@(v1',w,v2)#ps2) v2'"
```

https://isa-afp.org/entries/Koenigsberg_Friendship.shtml

## 55. Product of Segments of Chords

```theorem product_of_chord_segments:
fixes S1 T1 S2 T2 X C :: "'a :: euclidean_space"
assumes "between (S1, T1) X" "between (S2, T2) X"
assumes "dist C S1 = r" "dist C T1 = r"
assumes "dist C S2 = r" "dist C T2 = r"
shows "dist S1 X * dist X T1 = dist S2 X * dist X T2"
```

https://www.isa-afp.org/entries/Chord_Segments.shtml

## 56. The Hermite-Lindemann Transcendence Theorem

```theorem Hermite_Lindemann:
fixes α β :: "'a ⇒ complex"
assumes "finite I"
assumes "⋀x. x ∈ I ⟹ algebraic (α x)"
assumes "⋀x. x ∈ I ⟹ algebraic (β x)"
assumes "inj_on α I"
assumes "(∑x∈I. β x * exp (α x)) = 0"
shows   "∀x∈I. β x = 0"

corollary Hermite_Lindemann_original:
fixes n :: nat and α :: "nat ⇒ complex"
assumes "inj_on α {..<n}"
assumes "⋀i. i < n ⟹ algebraic (α i)"
assumes "linearly_independent_over_int (α ` {..<n})"
shows   "algebraically_independent_over_rat n (λi. exp (α i))"
```

https://www.isa-afp.org/entries/Hermite_Lindemann.html

## 57. Heron’s formula

```theorem heron:
fixes A B C :: "real ^ 2"
defines "a ≡ dist B C" and "b ≡ dist A C" and "c ≡ dist A B"
defines "s ≡ (a + b + c) / 2"
shows   "content (convex hull {A, B, C}) = sqrt (s * (s - a) * (s - b) * (s - c))"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Simplex_Content.html

## 58. Formula for the Number of Combinations

```theorem n_subsets:
"finite A ⟹ card {B. B ⊆ A ∧ card B = k} = (card A choose k)"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL/Binomial.html

## 59. The Laws of Large Numbers

``` theorem (in prob_space) strong_law_of_large_numbers_iid:
fixes X :: "nat ⇒ 'a ⇒ real"
assumes indep: "indep_vars (λ_. borel) X UNIV"
assumes distr: "⋀i. distr M borel (X i) = distr M borel (X 0)"
assumes L1:    "integrable M (X 0)"
shows "AE x in M. (λn. (∑i<n. X i x) / n) ⇢ expectation (X 0)"
```

https://www.isa-afp.org/entries/Laws_of_Large_Numbers.html

## 60. Bezout’s Theorem

```lemma bezout_gcd_nat:
fixes a b :: nat
shows "∃x y. a * x - b * y = gcd a b ∨ b * x - a * y = gcd a b"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-Computational_Algebra/Primes.html

## 63. Cantor’s Theorem

```lemma Cantors_paradox: ∄f. f ` A = Pow A
```

https://isabelle.in.tum.de/dist/library/HOL/HOL/Fun.html

## 64. L’Hôpital’s Rule

```lemma lhopital:
fixes f g f' g' :: "real ⇒ real"
assumes "f ─x→ 0" and "g ─x→ 0"
assumes "∀⇩F u in at x. g u ≠ 0"
assumes "∀⇩F u in at x. g' u ≠ 0"
assumes "∀⇩F u in at x. (f has_real_derivative f' u) (at u)"
assumes "∀⇩F u in at x. (g has_real_derivative g' u) (at u)"
assumes "filterlim (λx. f' x / g' x) F (at x)"
shows   "filterlim (λx. f x / g x) F (at x)"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL/Deriv.html

## 65. Isosceles Triangle Theorem

```lemma isosceles_triangle:
assumes "dist a c = dist b c"
shows   "angle b a c = angle a b c"
```

https://isa-afp.org/entries/Triangle.shtml

## 66. Sum of a Geometric Series

```lemma geometric_sums:
"norm c < 1 ⟹ (λn. c^n) sums (1 / (1 - c))"

lemma suminf_geometric:
"norm c < 1 ⟹ (∑n. c ^ n) = 1 / (1 - c)"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL/Series.html

## 67. e is Transcendental

```corollary e_transcendental_real: "¬ algebraic (exp 1 :: real)"
```

https://www.isa-afp.org/entries/E_Transcendental.shtml

## 68. Sum of an Arithmetic Series

```lemma double_arith_series:
fixes a d :: "'a :: comm_semiring_1"
shows "2 * (∑i=0..n. a + of_nat i * d) = (of_nat n + 1) * (2 * a + of_nat n * d)"
```

## 69. Greatest Common Divisor Algorithm

The greatest common divisor is defined in the `semiring_gcd` typeclass. Instances are provided for all the basic types, such as naturals, integers, and polynomials. The most important properties are:

```lemma gcd_dvd1:     "gcd a b dvd a"
and gcd_dvd2:     "gcd a b dvd b"
and gcd_greatest: "c dvd a ⟹ c dvd b ⟹ c dvd gcd a b"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL/GCD.html

## 70. Perfect Number Theorem

```theorem perfect_number_theorem:
assumes even: "even m" and perfect: "perfect m"
shows "∃ n . m = 2^n*(2^(n+1) - 1) ∧ prime ((2::nat)^(n+1) - 1)"
```

https://isa-afp.org/entries/Perfect-Number-Thm.shtml

## 71. Order of a Subgroup

```proposition (in group) lagrange_finite:
assumes "finite (carrier G)" and "subgroup H G"
shows "card (rcosets H) * card H = order G"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/Coset.html

## 72. Sylow’s Theorem

```theorem sylow_thm:
assumes "prime p" and "group G" and "order G = p ^ a * m" and "finite (carrier G)"
obtains H where "subgroup H G" and "card H = p ^ a"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/Sylow.html

## 73. Ascending or Descending Sequences

```lemma Erdoes_Szekeres:
fixes f :: "_ ⇒ 'a::linorder"
shows "(∃S. S ⊆ {0..m * n} ∧ card S = m + 1 ∧ mono_on f (op ≤) S) ∨
(∃S. S ⊆ {0..m * n} ∧ card S = n + 1 ∧ mono_on f (op ≥) S)"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Erdoes_Szekeres.html

## 74. The Principle of Mathematical Induction

```theorem nat_induct:
assumes "P 0" and "⋀n. P n ⟹ P (Suc n)"
shows   "P n"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL/Nat.html

## 75. The Mean Value Theorem

```theorem MVT:
fixes a b :: real and f :: "real ⇒ real"
assumes "a < b"
and "∀x∈{a..b}. isCont f x"
and "∀x∈{a<..<b}. f differentiable (at x)"
shows "∃l z::real. z ∈ {a<..<b} ∧ (f has_real_derivative l) (at z) ∧
f b - f a = (b - a) * l"

lemma MVT2:
fixes a b :: real and f f' :: "real ⇒ real"
assumes "a < b"
and "∀x∈{a..b}. (f has_real_derivative f' x) (at x)"
shows "∃z::real. z ∈ {a<..<b} ∧ f b - f a = (b - a) * f' z"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL/Deriv.html

## 76. Fourier Series

```corollary Fourier_Fejer_Cesaro_summable_simple:
assumes f: "continuous_on UNIV f"
and periodic: "⋀x. f(x + 2*pi) = f x"
shows "(λn. (∑m<n. ∑k≤2*m. Fourier_coefficient f k * trigonometric_set k x) / n) \<longlonglongrightarrow> f x"
```

https://www.isa-afp.org/entries/Fourier.html

## 77. Sum of kth powers

```lemma sum_of_powers:
fixes m n :: nat
shows "(∑k=0..n. k ^ m) = (bernpoly (m + 1) (n + 1) - bernpoly (m + 1) 0) / (m + 1)"
```

https://www.isa-afp.org/entries/Bernoulli.html

## 78. The Cauchy-Schwarz Inequality

```theorem CauchySchwarzReal:
fixes x::vector
assumes "vlen x = vlen y"
shows "¦x⋅y¦ ≤ ∥x∥*∥y∥"
```

https://isa-afp.org/entries/Cauchy.shtml

An alternative version is available in the standard library:

```lemma Cauchy_Schwarz_ineq2:
"¦inner x y¦ ≤ norm x * norm y"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Inner_Product.html

## 79. The Intermediate Value Theorem

```lemma IVT':
fixes f :: "real ⇒ real"
assumes "a ≤ b" and "y ∈ {f a..f b}" and  "continuous_on {a..b} f"
obtains x where "x ∈ {a..b}" and "f x = y"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL/Topological_Spaces.html

## 80. Fundamental Theorem of Arithmetic

The function `prime_factorization` is defined for any factorial semiring. It returns the factorization as a multiset that fulfils the following properties:

```lemma in_prime_factors_iff:
"p ∈ set_mset (prime_factors x) ⟷ x ≠ 0 ∧ p dvd x ∧ prime p"

lemma prod_mset_prime_factorization:
assumes "x ≠ 0"
shows   "prod_mset (prime_factorization x) = normalize x"

lemma prime_factorization_unique:
assumes "x ≠ 0" "y ≠ 0"
shows   "prime_factorization x = prime_factorization y ⟷ normalize x = normalize y"
```

The `normalize` function is required because associated elements (like -3 and 3) have the same factorization; for natural numbers, it is the identity.

https://isabelle.in.tum.de/dist/library/HOL/HOL-Computational_Algebra/Factorial_Ring.html

## 81. Divergence of the Prime Reciprocal Series

```corollary prime_harmonic_series_diverges:
"¬convergent (λn. ∑p←primes_upto n. 1 / p)"
```

https://isa-afp.org/entries/Prime_Harmonic_Series.shtml

The more precise asymptotic estimate given by Mertens’ Second Theorem is also available:

```theorem mertens_second_theorem:
"(λx. (∑p | real p ≤ x ∧ prime p. 1 / p) - ln (ln x) - meissel_mertens) ∈ O(λx. 1 / ln x)"
```

https://www.isa-afp.org/entries/Prime_Number_Theorem.html

## 83. The Friendship Theorem

```theorem (in valid_unSimpGraph) friendship_thm:
assumes "⋀v u. v∈V ⟹ u∈V ⟹ v≠u ⟹ ∃! n. adjacent v n ∧ adjacent u n" and "finite V"
shows "∃v. ∀n∈V. n≠v ⟶ adjacent v n"
```

https://isa-afp.org/entries/Koenigsberg_Friendship.shtml

## 85. Divisibility by Three Rule

```theorem three_divides_nat: "3 dvd n ⟷ 3 dvd sumdig n"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/ThreeDivides.html

## 86. Lebesgue Measure and Integration

https://isa-afp.org/entries/Integration.shtml

A more recent and more extensive library of the Lebesgue Measure and Lebesgue integration is now also in the standard distribution:

https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Lebesgue_Measure.html

https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Nonnegative_Lebesgue_Integration.html

## 87. Desargues’s Theorem

```theorem desargues_3D:
assumes "desargues_config_3D A B C A' B' C' P α β γ"
shows "rk {α, β, γ} ≤ 2"
```

https://www.isa-afp.org/entries/Projective_Geometry.html

## 88. Derangements Formula

```theorem derangements_formula:
assumes "n ≠ 0" and "finite S" and "card S = n"
shows "card (derangements S) = round (fact n / exp 1)"
```

https://isa-afp.org/entries/Derangements.shtml

## 89. The Factor and Remainder Theorems

```lemma long_div_theorem:
assumes "g ∈ carrier P" and "f ∈ carrier P" and "g ≠ 𝟬\<^bsub>P\<^esub>"
shows "∃q r (k::nat). (q ∈ carrier P) ∧ (r ∈ carrier P) ∧
(lcoeff g)(^)\<^bsub>R\<^esub>k ⊙\<^bsub>P\<^esub> f = g ⊗\<^bsub>P\<^esub> q ⊕\<^bsub>P\<^esub> r ∧
(r = 𝟬\<^bsub>P\<^esub> | deg R r < deg R g)"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/UnivPoly.html

Independently, `HOL-Computational_Algebra` provides notions of division and remainder in Euclidean rings (such as naturals, integers, polynomials):

https://isabelle.in.tum.de/dist/library/HOL/HOL-Computational_Algebra/Euclidean_Algorithm.html

## 90. Stirling’s Formula

```theorem Gamma_asymp_equiv:
"Gamma ∼ (λx. sqrt (2*pi/x) * (x / exp 1) powr x :: real)"

theorem fact_asymp_equiv:
"fact ∼ (λn. sqrt (2*pi*n) * (n / exp 1) ^ n :: real)"
```

https://www.isa-afp.org/entries/Stirling_Formula.shtml

## 91. The Triangle Inequality

```class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
assumes abs_ge_zero: "¦a¦ ≥ 0"
and abs_ge_self: "a ≤ ¦a¦"
and abs_leI: "a ≤ b ⟹ - a ≤ b ⟹ ¦a¦ ≤ b"
and abs_minus_cancel: "¦-a¦ = ¦a¦"
and abs_triangle_ineq: "¦a + b¦ ≤ ¦a¦ + ¦b¦"
```

The triangle inequality is a type class property in Isabelle. Real numbers, integers, etc are instances of this type class:

```lemma abs_triangle_ineq_real: "¦(a::real) + b¦ ≤ ¦a¦ + ¦b¦"
lemma abs_triangle_ineq_int: "¦(a::int) + b¦ ≤ ¦a¦ + ¦b¦"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL/Groups.html

## 93. The Birthday Problem

```lemma birthday_paradox:
assumes "card S = 23" "card T = 365"
shows "2 * card {f ∈ S→\<^sub>E S T. ¬ inj_on f S} ≥ card (S →\<^sub>E T)"
```

## 94. The Law of Cosines

```lemma cosine_law_triangle:
"dist b c ^ 2 = dist a b ^ 2 + dist a c ^ 2 - 2 * dist a b * dist a c * cos (angle b a c)"
```

https://isa-afp.org/entries/Triangle.shtml

## 95. Ptolemy’s Theorem

```theorem ptolemy:
fixes A B C D center :: "real ^ 2"
assumes "dist center A = radius" and "dist center B = radius"
assumes "dist center C = radius" and "dist center D = radius"
assumes ordering_of_points:
shows "dist A C * dist B D = dist A B * dist C D + dist A D * dist B C"
```

https://www.isa-afp.org/entries/Ptolemys_Theorem.shtml

## 96. Principle of Inclusion/Exclusion

```lemma card_UNION:
assumes "finite A" and "∀k ∈ A. finite k"
shows "card (⋃A) = nat (∑I | I ⊆ A ∧ I ≠ {}. (- 1) ^ (card I + 1) * int (card (⋂I)))"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL/Binomial.html

## 97. Cramer’s Rule

```lemma cramer:
fixes A ::"real^'n^'n"
assumes d0: "det A ≠ 0"
shows "A *v x = b ⟷ x = (χ k. det(χ i j. if j=k then b\$i else A\$i\$j) / det A)"
```

https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Determinants.html

## 98. Bertrand’s Postulate

```theorem bertrand: "n > 1 ⟹ ∃p∈{n<..<2*n}. prime p"
```

https://www.isa-afp.org/entries/Bertrands_Postulate.shtml

## 99. Buffon Needle Problem

```theorem buffon_short:
assumes "l ≤ d"
shows   "emeasure (buffon l d) {True} = 2 * l / (d * pi)"

theorem buffon_long:
assumes "l ≥ d"
shows   "emeasure (buffon l d) {True} = 2 / pi * ((l / d) - sqrt ((l / d)⇧2 - 1) + arccos (d / l))"
```

https://www.isa-afp.org/entries/Buffons_Needle.shtml

## 100. Descartes Rule of Signs

```theorem descartes_sign_rule:
fixes p :: "real poly"
assumes "p ≠ 0"
shows "∃d. even d ∧ coeff_sign_changes p = count_pos_roots p + d"
```

https://isa-afp.org/entries/Descartes_Sign_Rule.shtml