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)
53. Pi is Transcendental
pi_is_transcendental
|- ~algebraic_number (Cx pi)
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] ** qPOLY_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