1. The Irrationality of the Square Root of 2
SQRT_2_IRRATIONAL

  |- ~rational(sqrt(&2))

2. Fundamental Theorem of Algebra
FTA

  |- !a n. a(0) = Cx(&0) \/ ~(!k. k IN 1..n ==> a(k) = Cx(&0))
           ==> ?z. vsum(0..n) (\i. a(i) * z pow i) = Cx(&0)

3. The Denumerability of the Rational Numbers
DENUMERABLE_RATIONALS

  |- denumerable { x:real | rational(x)}

4. Pythagorean Theorem
PYTHAGORAS

  |- !A B C:real^2.
          orthogonal (A - B) (C - B)
          ==> norm(C - A) pow 2 = norm(B - A) pow 2 + norm(C - B) pow 2

5. Prime Number Theorem
PNT

  |- ((\n. &(CARD {p | prime p /\ p <= n}) / (&n / log(&n)))
      ---> &1) sequentially

6. Gödel's Incompleteness Theorem
G1_TRAD

  |- !A. consistent A /\
         complete_for (SIGMA 1 INTER closed) A /\
         definable_by (SIGMA 1) (IMAGE gform A)
         ==> ?G. PI 1 G /\ closed G /\ true G /\ ~(A |-- G) /\
                 (sound_for (SIGMA 1 INTER closed) A ==> ~(A |-- Not G))

7. Law of Quadratic Reciprocity
RECIPROCITY_LEGENDRE

 |- !p q. prime p /\ prime q /\ ODD p /\ ODD q /\ ~(p = q)
          ==> legendre(p,q) * legendre(q,p) =
              --(&1) pow ((p - 1) DIV 2 * (q - 1) DIV 2)

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

  |- !y. ~(constructible(vector[cos(pi / &9); y]))

DOUBLE_THE_CUBE

  |- !x. x pow 3 = &2 ==> ~(constructible(vector[x; &0]))

9. The Area of a Circle
AREA_OF_CIRCLE

  |- !a:real^2 r.
          measurable {z | dist(a,z) <= r} /\
          (&0 <= r ==> measure {z | dist(a,z) <= r} = pi * r pow 2)

10. Euler's Generalization of Fermat's Little Theorem
FERMAT_LITTLE

  |- !a n. coprime(a,n) ==> (a EXP (phi n) == 1) (mod n)

11. The Infinitude of Primes
PRIMES_INFINITE

  |- INFINITE {p | prime p}

12. The Independence of the Parallel Postulate
AXIOM_10_EUCLIDEAN

  |- !a b c d t:real^N.
          between d (a,t) /\ between d (b,c) /\ ~(a = d)
          ==> ?x y. between b (a,x) /\ between c (a,y) /\ between t (x,y)

NOT_AXIOM_10_NONEUCLIDEAN

  |- ~(!a b c d t.
        B a d t /\ B b d c /\ ~(a = d) ==> ?x y. B a b x /\ B a c y /\ B x t y

13. Polyhedron Formula
EULER_RELATION

  |- !p:real^3->bool.
         polytope p /\ aff_dim p =&3
         ==>  (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

14. Euler's Summation of 1 + (1/2)^2 + (1/3)^2 + ....
EULER_HARMONIC_SUM

  |- (\m. inv (&(m + 1) pow 2)) sums pi pow 2 / &6

15. Fundamental Theorem of Integral Calculus
FTC1

  |- !f f' a b. a <= b /\ (!x. a <= x /\ x <= b ==> (f diffl f'(x))(x))
          ==> defint(a,b) f' (f(b) - f(a))

17. De Moivre's Theorem
DEMOIVRE

  |- !t n. (Cx(cos t) + ii * Cx(sin t)) pow n =
           Cx(cos(&n * t)) + ii * Cx(sin(&n * t))

18. Liouville's Theorem and the Construction of Trancendental Numbers
LIOUVILLE

  |- !x. algebraic x
         ==> ?n c. c > &0 /\
                   !p q. ~(q = 0) ==> &p / &q = x \/
                                      abs(x - &p / &q) > c / &q pow n

TRANSCENDENTAL_LIOUVILLE

  |- transcendental(liouville)

19. Four Squares Theorem
LAGRANGE_INT

  |- !a. &0 <= a <=> ?w x y z. a = w pow 2 + x pow 2 + y pow 2 + z pow 2

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

  |- !p k. prime(p) /\ (p = 4 * k + 1) ==> ?x y. p = x EXP 2 + y EXP 2

22. The Non-Denumerability of the Continuum
UNCOUNTABLE_REALS

  |- ~countable(UNIV:real->bool)

23. Formula for Pythagorean Triples
PYTHAG_COCLASSIFY

  |- !u v w. ((u EXP 2) + (v EXP 2) = w EXP 2) /\ coprime(u,v) /\
                  (EVEN(u) /\ ODD(v) /\ ODD(w)) ==>
                       ?p q. coprime(p,q) /\
                             (u = 2 * p * q) /\
                             (v = (p EXP 2) - (q EXP 2)) /\
                             (w = (p EXP 2) + (q EXP 2))

25. Schroeder-Bernstein Theorem
CARD_LE_ANTISYM

  |- !s:A->bool t:B->bool. s <=_c t /\ t <=_c s <=> (s =_c t)

26. Leibniz's Series for Pi
LEIBNIZ_PI

  |- (\n. (-- &1) pow n / &(2 * n + 1)) sums (pi / &4)

27. Sum of the Angles of a Triangle
TRIANGLE_ANGLE_SUM

  |- !A B C:real^N. ~(A = B /\ B = C /\ A = C)
                    ==> angle(B,A,C) + angle(A,B,C) + angle(B,C,A) = pi

28. Pascal's Hexagon Theorem
PASCAL_AFFINE_CIRCLE

  |- !c r x1 x2 x3 x4 x5 x6 x7 x8 x9:real^2.
          PAIRWISE (\x y. ~(x = y)) [x1;x2;x3;x4;x5;x6] /\
          dist(c,x1) = r /\ dist(c,x2) = r /\ dist(c,x3) = r /\
          dist(c,x4) = r /\ dist(c,x5) = r /\ dist(c,x6) = r /\
          collinear {x1,x9,x5} /\
          collinear {x1,x8,x6} /\
          collinear {x2,x9,x4} /\
          collinear {x2,x7,x6} /\
          collinear {x3,x8,x4} /\
          collinear {x3,x7,x5}
          ==> collinear {x7,x8,x9}

29. Feuerbach's Theorem
FEUERBACH

  |- !a b c mbc mac mab pbc pac pab ncenter icenter nradius iradius.
        ~(collinear {a,b,c}) /\
        midpoint(a,b) = mab /\
        midpoint(b,c) = mbc /\
        midpoint(c,a) = mac /\
        dist(ncenter,mbc) = nradius /\
        dist(ncenter,mac) = nradius /\
        dist(ncenter,mab) = nradius /\
        dist(icenter,pbc) = iradius /\
        dist(icenter,pac) = iradius /\
        dist(icenter,pab) = iradius /\
        collinear {a,b,pab} /\ orthogonal (a - b) (icenter - pab) /\
        collinear {b,c,pbc} /\ orthogonal (b - c) (icenter - pbc) /\
        collinear {a,c,pac} /\ orthogonal (a - c) (icenter - pac)
        ==> ncenter = icenter /\ nradius = iradius \/
            ?!x:real^2. dist(ncenter,x) = nradius /\ dist(icenter,x) = iradius

30. The Ballot Problem
BALLOT

  |- all_countings a b =
           let n = a + b in
           CARD {f | f IN (1..n --> {A,B}) /\
                     CARD { i | i IN 1..n /\ f(i) = A} = a /\
                     CARD { i | i IN 1..n /\ f(i) = B} = b}
  |- valid_countings a b =
           let n = a + b in
           CARD {f | f IN (1..n --> {A,B}) /\
                     CARD { i | i IN 1..n /\ f(i) = A} = a /\
                     CARD { i | i IN 1..n /\ f(i) = B} = b /\
                     !m. 1 <= m /\ m <= n
                         ==> CARD { i | i IN 1..m /\ f(i) = A} >
                             CARD { i | i IN 1..m /\ f(i) = B}}
  |- !a b. &(valid_countings a b) =
              if a <= b then if b = 0 then &1 else &0
              else (&a - &b) / (&a + &b) *  &(all_countings a b)

31. Ramsey's Theorem
RAMSEY

  |- !M N C s.
          INFINITE(s:A->bool) /\
          (!t. t SUBSET s /\ t HAS_SIZE N ==> C(t) <= M)
          ==> ?t c. INFINITE(t) /\ t SUBSET s /\
                    (!u. u SUBSET t /\ u HAS_SIZE N ==> (C(u) = c))

34. Divergence of the Harmonic Series
HARMONIC_DIVERGES'

  |- ~(convergent (\n. sum(1..n) (\i. &1 / &i)))

35. Taylor's Theorem
MCLAURIN

  |- !f diff h n.
      &0 < h /\
      0 < n /\
      (diff(0) = f) /\
      (!m t. m < n /\ &0 <= t /\ t <= h ==>
             (diff(m) diffl diff(SUC m)(t))(t)) ==>
     (?t. &0 < t /\ t < h /\
          (f(h) = sum(0,n)(\m. (diff(m)(&0) / &(FACT m)) * (h pow m)) +
                  ((diff(n)(t) / &(FACT n)) * (h pow n))))

36. Brouwer Fixed Point Theorem
BROUWER

  |- !f:real^N->real^N s.
          compact s /\ convex s /\ ~(s = {}) /\
          f continuous_on s /\ IMAGE f s SUBSET s
          ==> ?x. x IN s /\ f x = x

37. The Solution of a Cubic
CUBIC

  |- ~(a = Cx(&0))
     ==> let p = (Cx(&3) * a * c - b pow 2) / (Cx(&9) * a pow 2)
         and q = (Cx(&9) * a * b * c - Cx(&2) * b pow 3 - Cx(&27) * a pow 2 * d) /
                 (Cx(&54) * a pow 3) in
         let s = csqrt(q pow 2 + p pow 3) in
         let s1 = if p = Cx(&0) then ccbrt(Cx(&2) * q) else ccbrt(q + s) in
         let s2 = --s1 * (Cx(&1) + ii * csqrt(Cx(&3))) / Cx(&2)
         and s3 = --s1 * (Cx(&1) - ii * csqrt(Cx(&3))) / Cx(&2) in
         if p = Cx(&0) then
           a * x pow 3 + b * x pow 2 + c * x + d = Cx(&0) <=>
              x = s1 - b / (Cx(&3) * a) \/
              x = s2 - b / (Cx(&3) * a) \/
              x = s3 - b / (Cx(&3) * a)
         else
           ~(s1 = Cx(&0)) /\
           (a * x pow 3 + b * x pow 2 + c * x + d = Cx(&0) <=>
               x = s1 - p / s1 - b / (Cx(&3) * a) \/
               x = s2 - p / s2 - b / (Cx(&3) * a) \/
               x = s3 - p / s3 - b / (Cx(&3) * a))

38. Arithmetic Mean/Geometric Mean
AGM_ROOT

  |- !n a. 1 <= n /\ (!i. 1 <= i /\ i <= n ==> &0 <= a(i))
           ==> root n (product(1..n) a) <= sum(1..n) a / &n

39. Solutions to Pell's Equation
SOLUTIONS_ARE_XY

  |- !a x y.
      ~(a = 0) /\
      (x EXP 2 = (a EXP 2 - 1) * y EXP 2 + 1)
      ==> ?n. (x = X a n) /\ (y = Y a n)

40. Minkowski's Fundamental Theorem
MINKOWSKI

  |- !s:real^N->bool.
          convex s /\
          bounded s /\
          (!x. x IN s ==> (--x) IN s) /\
          &2 pow dimindex(:N) < measure s
          ==> ?u. ~(u = vec 0) /\
                  (!i. 1 <= i /\ i <= dimindex(:N) ==> integer(u$i)) /\
                  u IN s

42. Sum of the Reciprocals of the Triangular Numbers
TRIANGLE_CONVERGES'

  |- (\n. sum(1..n) (\k. &1 / &(triangle k))) --> &2

43. The Isoperimetric Theorem
ISOPERIMETRIC_THEOREM

  |- !L g.
        rectifiable_path g /\
        simple_path g /\
        pathfinish g = pathstart g /\
        path_length g = L
        ==> measure(inside (path_image g)) <= L pow 2 / (&4 * pi) /\
            (measure(inside (path_image g)) = L pow 2 / (&4 * pi)
             ==> (?a r. path_image g = sphere (a,r)))

44. The Binomial Theorem
REAL_BINOMIAL_THEOREM

  |- !n. (x + y) pow n = sum(0..n) (\k. &(binom(n,k)) * x pow k * y pow (n - k))

45. The Partition Theorem
EULER_PARTITION_THEOREM

  |- FINITE {p | p partitions n /\ !i. p(i) <= 1} /\
     FINITE {p | p partitions n /\ !i. ~(p(i) = 0) ==> ODD i} /\
     CARD {p | p partitions n /\ !i. p(i) <= 1} =
     CARD {p | p partitions n /\ !i. ~(p(i) = 0) ==> ODD i}

46. The Solution of the General Quartic Equation
QUARTIC_SOLUTION

  |- y pow 3 - b * y pow 2 + (a * c - Cx(&4) * d) * y -
       a pow 2 * d + Cx(&4) * b * d - c pow 2 = Cx(&0)
     ==> let R = csqrt(a pow 2 / Cx(&4) - b + y) in
         let s = csqrt(y pow 2 - Cx(&4) * d) in
         let D = csqrt(if R = Cx(&0)
                       then Cx(&3) * a pow 2 / Cx(&4) - Cx(&2) * b + Cx(&2) * s
                       else Cx(&3) * a pow 2 / Cx(&4) - R pow 2 - Cx(&2) * b +
                       (Cx(&4) * a * b - Cx(&8) * c - a pow 3) / (Cx(&4) * R)) in
         let E = csqrt(if R = Cx(&0)
                       then Cx(&3) * a pow 2 / Cx(&4) - Cx(&2) * b - Cx(&2) * s
                       else Cx(&3) * a pow 2 / Cx(&4) - R pow 2 - Cx(&2) * b -
                            (Cx(&4) * a * b - Cx(&8) * c - a pow 3) /
                            (Cx(&4) * R)) in
         x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = Cx(&0) <=>
         x = --a / Cx(&4) + R / Cx(&2) + D / Cx(&2) \/
         x = --a / Cx(&4) + R / Cx(&2) - D / Cx(&2) \/
         x = --a / Cx(&4) - R / Cx(&2) + E / Cx(&2) \/
         x = --a / Cx(&4) - R / Cx(&2) - E / Cx(&2)

48. Dirichlet's Theorem
DIRICHLET

  |- !d k. 1 <= d /\ coprime(k,d)
           ==> INFINITE {p | prime p /\ (p == k) (mod d)}

49. The Cayley-Hamilton Theorem
CAYLEY_HAMILTON

  |- !A. msum(0..dimindex(:N)) (\i. char_poly A i %% A mpow i) = mat 0

50. The Number of Platonic Solids
PLATONIC_SOLIDS

  |- !m n.
     (?p:real^3->bool.
       polytope p /\ aff_dim p =&3 /\
       (!f. f face_of p /\ aff_dim(f) =&2
            ==>  CARD {e | e face_of p /\ aff_dim(e) =&1 /\ e SUBSET f} =
            m) /\
       (!v. v face_of p /\ aff_dim(v) =&0
            ==>  CARD {e | e face_of p /\ aff_dim(e) =&1 /\ v SUBSET e} =
            n))
     <=>  m = 3 /\ n = 3 \/       // Tetrahedron
         m = 4 /\ n = 3 \/       // Cube
         m = 3 /\ n = 4 \/       // Octahedron
         m = 5 /\ n = 3 \/       // Dodecahedron
         m = 3 /\ n = 5          // Icosahedron

51. Wilson's Theorem
WILSON_EQ

  |- !p. ~(p = 1) ==> (prime p <=> (FACT(p - 1) == p - 1) (mod p))

52. The Number of Subsets of a Set
HAS_SIZE_POWERSET

  |- !(s:A->bool) n. s HAS_SIZE n ==> {t | t SUBSET s} HAS_SIZE (2 EXP n)

54. Konigsberg Bridges Problem
KOENIGSBERG

  |- !G. vertices(G) = {0,1,2,3} /\
         edges(G) = {10,20,30,40,50,60,70} /\
         termini G (10) = {0,1} /\
         termini G (20) = {0,2} /\
         termini G (30) = {0,3} /\
         termini G (40) = {1,2} /\
         termini G (50) = {1,2} /\
         termini G (60) = {2,3} /\
         termini G (70) = {2,3}
         ==> ~(?es a b. eulerian G es (a,b))

55. Product of Segments of Chords
SEGMENT_CHORDS

  |- !centre radius q r s t b.
          between b (q,r) /\ between b (s,t) /\
          length(q,centre) = radius /\ length(r,centre) = radius /\
          length(s,centre) = radius /\ length(t,centre) = radius
          ==> length(q,b) * length(b,r) = length(s,b) * length(b,t)

57. Heron's Formula
HERON

  |- !A B C:real^2.
          let a = dist(C,B)
          and b = dist(A,C)
          and c = dist(B,A) in
          let s = (a + b + c) / &2 in
          measure(convex hull {A,B,C}) =
            sqrt(s * (s - a) * (s - b) * (s - c))

58. Formula for the Number of Combinations
NUMBER_OF_COMBINATIONS

  |- !n m s:A->bool.
          s HAS_SIZE n
          ==> {t | t SUBSET s /\ t HAS_SIZE m} HAS_SIZE binom(n,m)

60. Bezout's Theorem
INT_GCD_EXISTS_POS

  |- !a b. ?d. &0 <= d /\ d divides a /\ d divides b /\
               ?x y. d = a * x + b * y

61. Theorem of Ceva
CEVA

  |- !A B C X Y Z:real^2.
          ~(collinear {A,B,C}) /\
          between X (B,C) /\ between Y (C,A) /\ between Z (A,B)
          ==> (dist(B,X) * dist(C,Y) * dist(A,Z) =
               dist(X,C) * dist(Y,A) * dist(Z,B) <=>
               (?P. between P (A,X) /\ between P (B,Y) /\ between P (C,Z)))

63. Cantor's Theorem
CANTOR_THM

  |- !s:A->bool. s <_c {t | t SUBSET s}

64. L'Hôpital's Rule
LHOPITAL

  |- !f g f' g' c L d.
          &0 < d /\
          (!x. &0 < abs(x - c) /\ abs(x - c) < d
               ==> (f diffl f'(x)) x /\ (g diffl g'(x)) x /\ ~(g'(x) = &0)) /\
          (f --> &0) c /\ (g --> &0) c /\ ((\x. f'(x) / g'(x)) --> L) c
          ==> ((\x. f(x) / g(x)) --> L) c

65. Isosceles Triangle Theorem
ISOSCELES_TRIANGLE_THEOREM

  |- !A B C:real^N. dist(A,C) = dist(B,C) ==> angle(C,A,B) = angle(A,B,C)

66. Sum of a Geometric Series
GP_FINITE

  |- !x. ~(x = &1) ==>
          !n. (sum(0,n) (\n. x pow n) = ((x pow n) - &1) / (x - &1))

GP

  |- !x. abs(x) < &1 ==> (\n. x pow n) sums inv(&1 - x)

67. e is Transcendental
transcedental_def

  |- transcedental (x:real) =
     ~ ? c.
           (ALL is_int c)
        /\ ((LENGTH c) > 1)
        /\ ((poly c x) = &0)
        /\ (HD c) > &0

e_DEF

  |- napier_e = exp (&1)

E_IS_TRANSCEDENTAL

  |- transcedental napier_e

68. Sum of an arithmetic series
ARITHMETIC_PROGRESSION

  |- !n. 1 <= n
         ==> nsum(0..n-1) (\i. a + d * i) = (n * (2 * a + (n - 1) * d)) DIV 2

69. Greatest Common Divisor Algorithm
egcd

  |- egcd(m,n) = if m = 0 then n
                 else if n = 0 then m
                 else if m <= n then egcd(m,n - m)
                 else egcd(m - n,n)

EGCD

  |- !a b. (egcd (a,b) divides a /\ egcd (a,b) divides b) /\
           (!e. e divides a /\ e divides b ==> e divides egcd (a,b))

70. The Perfect Number Theorem
PERFECT_EULER

  |- !n. EVEN(n) /\ perfect(n)
         ==> ?k. prime(2 EXP k - 1) /\ n = 2 EXP (k - 1) * (2 EXP k - 1)

71. Order of a Subgroup
GROUP_LAGRANGE_COSETS

  |- !g h ( ** ) i e.
          group (g,( ** ),i,e:A) /\ subgroup h (g,( ** ),i,e) /\ FINITE g
          ==> ?q. (CARD(g) = CARD(q) * CARD(h)) /\
                  (!b. b IN g ==> ?a x. a IN q /\ x IN h /\ (b = a ** x))

72. Sylow's Theorem
sylow1

  |- !e op i G p.
            group (G,op,i,e)
            ==> FINITE G
            ==> prime p
            ==> (!n. p EXP n divides CARD G
                     ==> (?H. subgroup op i H G /\ CARD H = p EXP n))

sylow2

  |- !e p G op i.
            group (G,op,i,e)
            ==> FINITE G
            ==> prime p
            ==> (!n H K.
                     ~(p EXP SUC n divides CARD G)
                     ==> subgroup op i H G
                     ==> subgroup op i K G
                     ==> CARD H = p EXP n
                     ==> CARD K = p EXP n
                     ==> (?g. g IN G /\ H = set_op1 (conjg (op,i) g) K)

sylow3_1

  |- !e p op i G.
            group (G,op,i,e)
            ==> FINITE G
            ==> prime p
            ==> (!n H.
                     ~(p EXP SUC n divides CARD G)
                     ==> subgroup op i H G
                     ==> CARD H = p EXP n
                     ==> CARD {K | subgroup op i K G /\ CARD K = p EXP n} =
                         CARD (cosets op G (normalizer op i G H)))

sylow3_2

  |- !e op i G p.
         group (G,op,i,e)
         ==> FINITE G
         ==> prime p
         ==> (!n m.
                  CARD G = p EXP n * m
                  ==> coprime (p,m)
                  ==> CARD {K | subgroup op i K G /\ CARD K = p EXP n} divides m)

sylow3_3

  |- !e op i G p.
          group (G,op,i,e)
          ==> FINITE G
          ==> prime p
          ==> (!n m.
                   CARD G = p EXP n * m
                   ==> coprime (p,m)
                   ==> CARD {K | subgroup op i K G /\ CARD K = p EXP n} MOD p = 1)

73. Ascending or Descending Sequences
ERDOS_SZEKERES

  |- !f:num->real m n.
          (?s. s SUBSET (1..m*n+1) /\ s HAS_SIZE (m + 1) /\ mono_on f (<=) s) \/
          (?s. s SUBSET (1..m*n+1) /\ s HAS_SIZE (n + 1) /\ mono_on f (>=) s)

74. The Principle of Mathematical Induction
num_INDUCTION

  |- !P. P 0 /\ (!n. P(n) ==> P(SUC n)) ==> (!n. P n)

75. The Mean Value Theorem
MVT

  |- !f a b. a < b /\
             (!x. a <= x /\ x <= b ==> f contl x) /\
             (!x. a < x /\ x < b ==> f differentiable x)
          ==> ?l z. a < z /\ z < b /\ (f diffl l)(z) /\
              (f(b) - f(a) = (b - a) * l)

76. Fourier Series
FOURIER_FEJER_CESARO_SUMMABLE

  |- !f x l r.
          f absolutely_real_integrable_on real_interval[--pi,pi] /\
          (!x. f(x + &2 * pi) = f x) /\
          (f ---> l) (atreal x within {x' | x' <= x}) /\
          (f ---> r) (atreal x within {x' | x' >= x})
          ==> ((\n. sum(0..n-1) (\m. sum (0..2*m)
                                         (\k. fourier_coefficient f k *
                                              trigonometric_set k x)) / &n)
               ---> (l + r) / &2)
              sequentially

77. Sum of kth powers
SUM_OF_POWERS

  |- !n. sum(0..n) (\k. &k pow m) =
          (bernpoly(SUC m) (&n + &1) - bernpoly(SUC m) (&0)) / (&m + &1)

78. The Cauchy-Schwarz Inequality
NORM_CAUCHY_SCHWARZ_ABS

  |- !x:real^N y. abs(x dot y) <= norm(x) * norm(y)

79. The Intermediate Value Theorem
IVT

  |- !f a b y. a <= b /\
               (f(a) <= y /\ y <= f(b)) /\
               (!x. a <= x /\ x <= b ==> f contl x)
          ==> (?x. a <= x /\ x <= b /\ (f(x) = y))

80. The Fundamental Theorem of Arithmetic
FTA

  |- !n. ~(n = 0)
         ==> ?!i. FINITE {p | ~(i p = 0)} /\
                  (!p. ~(i p = 0) ==> prime p) /\
                  n = product {p | ~(i p = 0)} (\p. p EXP (i p))

81. Divergence of the Prime Reciprocal Series
PRIMERECIP_DIVERGES

  |- ~(convergent (\n. sum {p | prime p /\ p <= n} (\p. &1 / &p)))

83. The Friendship Theorem
FRIENDSHIP

  |- !friend:person->person->bool.
        FINITE(:person) /\
        (!x. ~(friend x x)) /\
        (!x y. friend x y ==> friend y x) /\
        (!x y. ~(x = y) ==> ?!z. friend x z /\ friend y z)
        ==> ?u. !v. ~(v = u) ==> friend u v

84. Morley's Theorem
MORLEY

  |- !A B C:real^2 P Q R.
       ~collinear{A,B,C} /\ {P,Q,R} SUBSET convex hull {A,B,C} /\
       angle(A,B,R) = angle(A,B,C) / &3 /\
       angle(B,A,R) = angle(B,A,C) / &3 /\
       angle(B,C,P) = angle(B,C,A) / &3 /\
       angle(C,B,P) = angle(C,B,A) / &3 /\
       angle(C,A,Q) = angle(C,A,B) / &3 /\
       angle(A,C,Q) = angle(A,C,B) / &3
       ==> dist(R,P) = dist(P,Q) /\ dist(Q,R) = dist(P,Q)

85. Divisibility by 3 Rule
DIVISIBILITY_BY_3

  |- 3 divides (nsum(0..n) (\i. 10 EXP i * d(i))) <=>
     3 divides (nsum(0..n) (\i. d i))

86. Lebesgue Measure and Integration
MEASURABLE_ON_PREIMAGE_OPEN_HALFSPACE_COMPONENT_GE

  |- !f:real^M->real^N.
          f measurable_on (:real^M) <=>
          !a k. 1 <= k /\ k <= dimindex(:N)
                ==> lebesgue_measurable {x | f(x)$k >= a}

87. Desargues's Theorem
DESARGUES_DIRECT

   ~COLLINEAR {A',B,S} /\
   ~COLLINEAR {A,P,C} /\
   ~COLLINEAR {A,P,R} /\
   ~COLLINEAR {A,C,B} /\
   ~COLLINEAR {A,B,R} /\
   ~COLLINEAR {C',P,A'} /\
   ~COLLINEAR {C',P,B} /\
   ~COLLINEAR {C',P,B'} /\
   ~COLLINEAR {C',A',S} /\
   ~COLLINEAR {C',A',B'} /\
   ~COLLINEAR {P,C,A'} /\
   ~COLLINEAR {P,C,B} /\
   ~COLLINEAR {P,A',R} /\
   ~COLLINEAR {P,B,Q} /\
   ~COLLINEAR {P,Q,B'} /\
   ~COLLINEAR {C,B,S} /\
   ~COLLINEAR {A',Q,B'}
   ==> COLLINEAR {A,A',P} /\ COLLINEAR {B,B',P} /\ COLLINEAR {C,C',P} /\
       COLLINEAR {B,C,Q} /\ COLLINEAR {B',C',Q} /\
       COLLINEAR {A,C,R} /\ COLLINEAR {A',C',R} /\
       COLLINEAR {A,B,S} /\ COLLINEAR {A',B',S}
       ==> COLLINEAR {Q,R,S}

88. Derangements Formula
THE_DERANGEMENTS_FORMULA

  |- !n s. s HAS_SIZE n /\ ~(n = 0)
           ==> FINITE {p | p deranges s} /\
               let e = exp(&1) in
               &(CARD {p | p deranges s}) = round(&(FACT n) / e)

89. The Factor and Remainder Theorems
POLY_LINEAR_DIVIDES

  |- !a p. (poly p a = &0) <=> (p = []) \/ ?q. p = [--a; &1] ** q
POLY_LINEAR_REM
  |- !t h. ?q r. CONS h t = [r] ++ [--a; &1] ** q

90. Stirling's Formula
STIRLING

  |- (\n. ln(&(FACT n)) - ((&n + &1 / &2) * ln(&n) - &n + ln(&2 * pi) / &2))
     --> &0

91. The Triangle Inequality
NORM_TRIANGLE

  |- !x y. norm(x + y) <= norm(x) + norm(y)

92. Pick's Theorem
PICK

|- !p:(real^2)list.
        (!x. MEM x p ==> integral_vector x) /\
        simple_path (polygonal_path p) /\
        pathfinish (polygonal_path p) = pathstart (polygonal_path p)
        ==> measure(inside(path_image(polygonal_path p))) =
                &(CARD {x | x IN inside(path_image(polygonal_path p)) /\
                            integral_vector x}) +
                &(CARD {x | x IN path_image(polygonal_path p) /\
                            integral_vector x}) / &2 - &1

93. The Birthday Problem
BIRTHDAY_THM_EXPLICIT

  |- !s t. s HAS_SIZE 23 /\ t HAS_SIZE 365
           ==> 2 * CARD {f | f IN (s -> t) /\
                             ?x y. x IN s /\ y IN s /\ ~(x = y) /\ f(x) = f(y)}
               >= CARD (s -> t)

94. The Law of Cosines
LAW_OF_COSINES

  |- !A B C:real^2.
       length(B,C) pow 2 = length(A,B) pow 2 + length(A,C) pow 2 -
                           &2 * length(A,B) * length(A,C) * cos(angle(B,A,C))

95. Ptolemy's Theorem
PTOLEMY

  |- !A B C D:real^2 a b c d centre radius.
          A = centre + radius % vector [cos(a);sin(a)] /\
          B = centre + radius % vector [cos(b);sin(b)] /\
          C = centre + radius % vector [cos(c);sin(c)] /\
          D = centre + radius % vector [cos(d);sin(d)] /\
          &0 <= radius /\
          &0 <= a /\ a <= b /\ b <= c /\ c <= d /\ d <= &2 * pi
          ==> dist(A,C) * dist(B,D) =
              dist(A,B) * dist(C,D) + dist(A,D) * dist(B,C)

96. Principle of Inclusion/Exclusion
INCLUSION_EXCLUSION_USUAL

  |- !s:(A->bool)->bool.
          FINITE s /\ (!k. k IN s ==> FINITE k)
          ==> &(CARD(UNIONS s)) =
                  sum (1..CARD s) (\n. (-- &1) pow (n + 1) *
                                       sum {t | t SUBSET s /\ t HAS_SIZE n}
                                           (\t. &(CARD(INTERS t))))

97. Cramer's Rule
CRAMER

  |- !A:real^N^N x b.
          ~(det(A) = &0)
          ==> (A ** x = b <=>
               x = lambda k.
                     det((lambda i j. if j = k then b$i else A$i$j):real^N^N) /
                     det(A))

98. Bertrand's Postulate
BERTRAND

  |- !n. ~(n = 0) ==> ?p. prime p /\ n <= p /\ p <= 2 * n

100. Descartes Rule of Signs
DESCARTES_RULE_OF_SIGNS

 DESCARTES_RULE_OF_SIGNS =
   |- !f a n. f = (\x. sum(0..n) (\i. a i * x pow i)) /\
              (?i. i IN 0..n /\ ~(a i = &0))
              ==> ?d. EVEN d /\
                      variation(0..n) a =
                      nsum {r | &0 < r /\ f(r) = &0} (\r. multiplicity f r) + d