The Top 100 Theorems in Isabelle

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

corollary sqrt_2_not_rat: "sqrt 2 ∉ ℚ"

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

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

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"

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"

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)"

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⌉)"

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))"

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"

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"

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

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

corollary Euler_relation:
  fixes p :: "'n::euclidean_space set"
  assumes "polytope p" "aff_dim p = 3" "DIM('n) = 3"
  shows "(card {v. v face_of p ∧ aff_dim v = 0} + card {f. f face_of p ∧ aff_dim f = 2}) -
         card {e. e face_of p ∧ aff_dim e = 1} = 2"

theorem inverse_squares_sums: "(λn. 1 / (n + 1)⇧2) sums (pi⇧2 / 6)"

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}"

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

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

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

theorem four_squares: "∃a b c d::nat. n = a⇧2 + b⇧2 + c⇧2 + d⇧2"

theorem two_squares:
  assumes "prime (p :: nat)"
  shows   "(∃a b. p = a⇧2 + b⇧2) = [p ≠ 3] (mod 4)

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"

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

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"

corollary ctm_ZFC_imp_ctm_not_CH:
  assumes
    "M ≈ ω" "Transset(M)" "M ⊨ ZFC"
  shows
    "∃N.
      M ⊆ N ∧ N ≈ ω ∧ Transset(N) ∧ N ⊨ ZFC ∪ {⋅¬⋅CH⋅⋅} ∧
      (∀α. Ord(α) ⟶ (α ∈ M ⟷ α ∈ N))"

corollary ctm_ZFC_imp_ctm_CH:
assumes
  "M ≈ ω" "Transset(M)" "M ⊨ ZFC"
shows
  "∃N.
    M ⊆ N ∧ N ≈ ω ∧ Transset(N) ∧ N ⊨ ZFC ∪ {⋅CH⋅} ∧
    (∀α. Ord(α) ⟶ (α ∈ M ⟷ α ∈ N))"

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"

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

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"

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)"

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'))"

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

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"

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"

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))"

  theorem CauchysMeanTheorem:
  fixes z::"real list"
  assumes "pos z"
  shows "gmean z ≤ mean z"

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

corollary pell_solutions_infinite:
  fixes D :: nat
  assumes "∄k. D = k⇧2"
  shows   "infinite {(x :: int, y :: int). x⇧2 - D * y⇧2 = 1}"

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 ∈ ℤ"

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

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

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"

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))"

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

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"

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)⇧2)" and
    X_variance: "⋀n. variance (X n) = σ⇧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 * σ⇧2)))
        (density lborel std_normal_density)"

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

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

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

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

theorem transcendental_pi: "¬algebraic pi"

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'"

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"

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))"

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))"

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

 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)"

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"

lemma Cevas:
  fixes a :: "'a::euclidean_space"
  assumes MidCol : "collinear {a,k,d} ∧ collinear {b,k,e} ∧ collinear {c,k,f}"
  assumes TriCol : "collinear {a,f,b} ∧ collinear {a,e,c} ∧ collinear {b,d,c}"
  assumes Triangle : "¬ collinear {a,b,c}"
  shows "dist a f * dist b d * dist c e = dist f b * dist d c * dist e a"

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

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)"

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

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)"

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

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)"

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"

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)"

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

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"

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)"

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

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"

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"

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)"

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

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

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"

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"

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

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

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"

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

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

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

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

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)"

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¦"

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

theorem pick:
fixes p :: "R_to_R2"
assumes "polygon p"
assumes "p = make_polygonal_path vts"
assumes "all_integral vts"
assumes "I = card {x. integral_vec x ∧ x ∈ path_inside p}"
assumes "B = card {x. integral_vec x ∧ x ∈ path_image p}"
shows "measure lebesgue (path_inside p) = I + B/2 - 1"

lemma birthday_paradox:
  assumes "card S = 23" "card T = 365"
  shows "2 * card {f ∈ S→⇩E S T. ¬ inj_on f S} ≥ card (S →⇩E T)"

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)"

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:
    "radiant_of (A - center) ≤ radiant_of (B - center)"
    "radiant_of (B - center) ≤ radiant_of (C - center)"
    "radiant_of (C - center) ≤ radiant_of (D - center)"
  shows "dist A C * dist B D = dist A B * dist C D + dist A D * dist B C"

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)))"

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)"

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

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))"

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