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] ** 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