DONE 70 items (as of 1.08.2023):
1. The Irrationality of the Square Root of 2
2. Fundamental Theorem of Algebra
3. The Denumerability of the Rational Numbers
4. Pythagorean Theorem
7. Law of Quadratic Reciprocity
10. Euler's Generalization of Fermat's Little Theorem
11. The Infinitude of Primes
13. Polyhedron Formula
14. Euler's Summation of 1 + (1/2)^2 + (1/3)^2 + .... by K. Pak and A. Kornilowicz
15. Fundamental Theorem of Integral Calculus
17. De Moivre's Theorem
18. Liouville's Theorem and the Construction of Transcendental Numbers
19. Four Squares Theorem
20. All Primes (1 mod 4) Equal the Sum of Two Squares
22. The Non-Denumerability of the Continuum
23. Formula for Pythagorean Triples
25. Schroeder-Bernstein Theorem
26. Leibniz's Series for Pi
27. Sum of the Angles of a Triangle
28. Pascal's Hexagon Theorem by R. Coghetto
30. The Ballot Problem
31. Ramsey's Theorem
34. Divergence of the Harmonic Series
35. Taylor's Theorem
36. Brouwer Fixed Point Theorem
37. The Solution of a Cubic
38. Arithmetic Mean/Geometric Mean
39. Solutions to Pell's Equation by M. Acewicz and K. Pak
42. Sum of the Reciprocals of the Triangular Numbers
44. The Binomial Theorem
45. The Partition Theorem
46. The Solution of the General Quartic Equation
51. Wilson's Theorem
52. The Number of Subsets of a Set
54. Konigsberg Bridges Problem
55. Product of Segments of Chords
57. Heron's Formula
58. Formula for the Number of Combinations
60. Bezout's Theorem
61. Theorem of Ceva
63. Cantor's Theorem
64. L'Hôpital's Rule
65. Isosceles Triangle Theorem
66. Sum of a Geometric Series
68. Sum of an arithmetic series
69. Greatest Common Divisor Algorithm
70. The Perfect Number Theorem
71. Order of a Subgroup
72. Sylow's Theorem
73. Ascending or Descending Sequences
74. The Principle of Mathematical Induction
75. The Mean Value Theorem
78. The Cauchy-Schwarz Inequality
79. The Intermediate Value Theorem
80. The Fundamental Theorem of Arithmetic
81. Divergence of the Prime Reciprocal Series (done by M. Carneiro)
83. The Friendship Theorem
84. Morley's Theorem
85. Divisibility by 3 Rule
86. Lebesgue Measure and Integration
87. Desargues's Theorem
88. Derangements Formula
89. The Factor and Remainder Theorems
91. The Triangle Inequality
93. The Birthday Problem
94. The Law of Cosines
95. Ptolemy's Theorem
96. Principle of Inclusion/Exclusion
97. Cramer's Rule
98. Bertrand's Postulate
TODO:
5. Prime Number Theorem
6. Gödel's Incompleteness Theorem
8. The Impossibility of Trisecting the Angle and Doubling the Cube
9. The Area of a Circle
12. The Independence of the Parallel Postulate
16. Insolvability of General Higher Degree Equations
21. Green's Theorem
24. The Undecidability of the Continuum Hypothesis
29. Feuerbach's Theorem
32. The Four Color Problem
33. Fermat's Last Theorem
40. Minkowski's Fundamental Theorem
41. Puiseux's Theorem
43. The Isoperimetric Theorem
47. The Central Limit Theorem
48. Dirichlet's Theorem
49. The Cayley-Hamilton Theorem
50. The Number of Platonic Solids
53. π is Transcendental
56. The Hermite-Lindemann Transcendence Theorem
59. The Laws of Large Numbers
62. Fair Games Theorem
67. e is Transcendental
76. Fourier Series
77. Sum of kth powers
82. Dissection of Cubes (J.E. Littlewood's "elegant" proof)
90. Stirling's Formula
92. Pick's Theorem
99. Buffon Needle Problem
100. Descartes Rule of Signs
1. The Irrationality of the Square Root of 2
IRRAT_1:1
theorem :: IRRAT_1:1 p is prime implies sqrt p is irrational;
2. Fundamental Theorem of Algebra
POLYNOM5:74
theorem :: POLYNOM5:74
for p be Polynomial of F_Complex st len p > 1 holds
p is with_roots;
3. The Denumerability of the Rational Numbers
TOPGEN_3:17
theorem :: TOPGEN_3:17
Card RAT = alef 0;
4. Pythagorean Theorem
EUCLID_3:46
theorem :: EUCLID_3:46
for p1,p2,p3 st p1<>p2 & p3<>p2 &
(angle(p1,p2,p3)=PI/2 or angle(p1,p2,p3)=3/2*PI) holds
(|.p1-p2.|^2+|.p3-p2.|^2=|.p1-p3.|^2);
7. Law of Quadratic Reciprocity
INT_5:49
theorem :: INT_5:49
p>2 & q>2 & p<>q
implies Lege(p,q)*Lege(q,p)=(-1)|^(((p-'1) div 2)*((q-'1) div 2));
10. Euler's Generalization of Fermat's Little Theorem
EULER_2:18
theorem :: EULER_2:18 ::Euler's theorem
a <> 0 & m > 1 & a,m are_relative_prime
implies (a |^ Euler m) mod m = 1;
11. The Infinitude of Primes
NEWTON:79
theorem :: NEWTON:79
SetPrimes is infinite;
13. Polyhedron Formula
POLYFORM:91
theorem :: POLYFORM:91
p is simply-connected & dim(p) = 3
implies num-vertices(p) - num-edges(p) + num-faces(p) = 2;
14. Euler's Summation of 1 + (1/2)^2 + (1/3)^2 + ....
BASEL_2:32
theorem :: BASEL_2:32
Sum Basel-seq = PI^2/6;
15. Fundamental Theorem of Integral Calculus
INTEGRA5:13
theorem :: INTEGRA5:13 for f being PartFunc of REAL,REAL st A c= X & f is_differentiable_on X & f`|X is_integrable_on A & f`|X is_bounded_on A holds integral(f`|X,A) = f.(sup A)-f.(inf A);
17. De Moivre's Theorem
SIN_COS3:50
theorem :: SIN_COS3:50 for n being Nat, z being Element of COMPLEX holds (cos_C/.z + <i>*sin_C/.z) #N n = cos_C/.([*n,0*]*z) + <i>*sin_C/.([*n,0*]*z);
18. Liouville's Theorem and the Construction of Transcendental Numbers
LIOUVIL2:27
theorem :: LIOUVIL2:27
for f being non-zero INT -valued Polynomial of F_Real
for a being irrational Element of F_Real st a is_a_root_of f
ex A being positive Real st
for p being Integer, q being positive Nat holds
|. a-p/q .| > A/(q|^len f);
registration
cluster -> transcendental for Liouville;
end;
19. Four Squares Theorem
LAGRA4SQ:18
theorem :: LAGRA4SQ:18
for n be Nat holds
ex x1,x2,x3,x4 be Nat st n = x1^2 + x2^2 + x3^2 + x4^2 ;
20. All Primes (1 mod 4) Equal the Sum of Two Squares
NAT_5:23
theorem :: NAT_5:23
p is prime & p mod 4 = 1 implies ex n,m st p = n^2 + m^2;
22. The Non-Denumerability of the Continuum
TOPGEN_3:30
theorem :: TOPGEN_3:30
alef 0 <` continuum;
23. Formula for Pythagorean Triples
PYTHTRIP:def 5
definition
redefine mode Pythagorean_triple means
:: PYTHTRIP:def 5
ex k,m,n st m <= n & it = { k*(n^2 - m^2), k*(2*m*n), k*(n^2 + m^2) };
end;
25. Schroeder-Bernstein Theorem
KNASTER:10
theorem :: KNASTER:10 :: Schroeder-Bernstein
f is one-to-one & g is one-to-one implies
ex h being Function of X,Y st h is bijective;
26. Leibniz's Series for Pi
LEIBNIZ1:14
theorem :: LEIBNIZ1:14
PI/4 = Sum Leibniz_Series;
27. Sum of the Angles of a Triangle
COMPLEX2:84
theorem :: COMPLEX2:84
a <> b & b <> c & 0 < angle(a,b,c) & angle(a,b,c) < PI
implies angle(a,b,c)+angle(b,c,a)+angle(c,a,b) = PI &
0 < angle(b,c,a) & 0 < angle(c,a,b);
28. Pascal's Hexagon Theorem
PASCAL:36
theorem :: PASCAL:36
not (a = 0 & b = 0 & c = 0 & d = 0 & e = 0 & f = 0) &
{P1,P2,P3,P4,P5,P6} c= conic(a,b,c,d,e,f) &
P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration
implies
P7,P8,P9 are_collinear;
30. The Ballot Problem
BALLOT_1:28
theorem :: BALLOT_1:28
A <> B & n >= k implies prob DominatedElection(A,n,B,k) = (n-k) / (n+k);
31. Ramsey's Theorem
RAMSEY_1:15
theorem :: RAMSEY_1:15
for X being infinite set,
P being a_partition of the_subsets_of_card(n,X)
st Card P = k holds
ex H being Subset of X st H is infinite & H is_homogeneous_for P;
34. Divergence of the Harmonic Series
SERIES_1:33
theorem :: SERIES_1:33
p<=1 & (for n st n>=1 holds s.n=1/n to_power p) implies s is not summable;
35. Taylor's Theorem
TAYLOR_1:33
theorem :: TAYLOR_1:33
for n be Nat, f be PartFunc of REAL,REAL, x0,r be Real st
( 0 < r & f is_differentiable_on n+1, ].x0-r,x0+r.[ )
for x be Real st x in ].x0-r, x0+r.[ holds
ex s be Real st 0 < s & s < 1 &
f.x=Partial_Sums(Taylor(f, ].x0-r,x0+r.[,x0,x)).n
+ (diff(f,].x0-r,x0+r.[).(n+1)).(x0+s*(x-x0))
* (x-x0) |^ (n+1) / ((n+1)!);
36. Brouwer Fixed Point Theorem
BROUWER2:8
theorem :: BROUWER2:8
for A st A is compact non boundary
for h be continuous Function of(TOP-REAL n) |A,(TOP-REAL n) |A
holds h has_a_fixpoint;
37. The Solution of a Cubic
POLYEQ_5:15
theorem :: POLYEQ_5:15
q = (3*a1 - a2|^2)/9 & q <> 0 & r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 &
s = 2-root(q|^3+r|^2) & s1 = 3-root(r+s) & s2 = -q/s1 implies
( z|^3+a2*z|^2+a1*z+a0 = 0
iff
z = s1+s2-a2/3 or
z = -(s1+s2)/2-a2/3+(s1-s2)*(2-root 3)*<i>/2 or
z = -(s1+s2)/2-a2/3-(s1-s2)*(2-root 3)*<i>/2);
theorem :: POLYEQ_5:16
q = (3*a1 - a2|^2)/9 & q = 0 & r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 &
s1 = 3-root(2*r) implies
( z|^3+a2*z|^2+a1*z+a0 = 0 iff
z = s1-a2/3 or
z = -s1/2-a2/3+s1*(2-root 3)*<i>/2 or
z = -s1/2-a2/3-s1*(2-root 3)*<i>/2);
38. Arithmetic Mean/Geometric Mean
RVSUM_3:47
theorem :: RVSUM_3:47
for f being non empty positive real-valued FinSequence holds
GMean f <= Mean f;
39. Solutions to Pell's Equation
PELLS_EQ:14
theorem :: PELLS_EQ:14
D is non square implies
ex x,y be Nat st x^2 - D * y^2 = 1 & y <> 0;
42. Sum of the Reciprocals of the Triangular Numbers
NUMPOLY1:89
definition
func ReciTriangRS -> Real_Sequence means
:: NUMPOLY1:def 13
for i being Nat holds
it.i = 1 / Triangle i;
end;
theorem :: NUMPOLY1:89
Sum ReciTriangRS = 2;
44. The Binomial Theorem
BINOM:25
theorem :: BINOM:25
for R being Abelian add-associative left_zeroed right_zeroed
commutative associative add-cancelable
distributive unital (non empty doubleLoopStr),
a,b being Element of R,
n being Nat
holds (a+b)|^n = Sum((a,b) In_Power n);
45. The Partition Theorem
EULRPART:16
theorem :: EULRPART:16
card the set of all p where p is odd-valued a_partition of n
=
card the set of all p where p is one-to-one a_partition of n;
46. The Solution of the General Quartic Equation
POLYEQ_5:30
definition
let a0,a1,a2 be complex number;
func 1_root_of_cubic(a0,a1,a2) -> complex number means
:: POLYEQ_5:def 2
ex r,s1 st r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s1 = 3-root(2*r) &
it = s1-a2/3 if 3*a1 - a2|^2 = 0
otherwise ex q,r,s,s1,s2 st q = (3*a1 - a2|^2)/9 &
r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s = 2-root(q|^3+r|^2) &
s1 = 3-root(r+s) & s2 = -q/s1 & it = s1+s2-a2/3;
func 2_root_of_cubic(a0,a1,a2) -> complex number means
:: POLYEQ_5:def 3
ex r,s1 st r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s1 = 3-root(2*r) &
it = -s1/2-a2/3+s1*(2-root 3)*<i>/2 if 3*a1 - a2|^2 = 0
otherwise ex q,r,s,s1,s2 st q = (3*a1 - a2|^2)/9 &
r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s = 2-root(q|^3+r|^2) &
s1 = 3-root(r+s) & s2 = -q/s1 &
it = -(s1+s2)/2-a2/3+(s1-s2)*(2-root 3)*<i>/2;
func 3_root_of_cubic(a0,a1,a2) -> complex number means
:: POLYEQ_5:def 4
ex r,s1 st r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s1 = 3-root(2*r) &
it = -s1/2-a2/3-s1*(2-root 3)*<i>/2 if 3*a1 - a2|^2 = 0
otherwise ex q,r,s,s1,s2 st q = (3*a1 - a2|^2)/9 &
r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s = 2-root(q|^3+r|^2) &
s1 = 3-root(r+s) & s2 = -q/s1 &
it = -(s1+s2)/2-a2/3-(s1-s2)*(2-root 3)*<i>/2;
end;
definition
let a0,a1,a2,a3 be complex number;
func 1_root_of_quartic(a0,a1,a2,a3) -> complex number means
:: POLYEQ_5:def 5
ex p,r,s1 st p = (8*a2-3*a3|^2)/32 &
r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(p|^2-r) &
it = 2-root(-2*(p-s1))-a3/4 if 8*a1 -4*a2*a3 + a3|^3 = 0
otherwise ex p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 &
q = (8*a1 -4*a2*a3 + a3|^3)/64 &
r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 &
s1 = 2-root(1_root_of_cubic(-q|^2,p|^2-r,2*p)) &
s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)) & s3 = -q/(s1*s2) &
it = s1+s2+s3-a3/4;
func 2_root_of_quartic(a0,a1,a2,a3) -> complex number means
:: POLYEQ_5:def 6
ex p,r,s1 st p = (8*a2-3*a3|^2)/32 &
r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(p|^2-r) &
it = -2-root(-2*(p-s1))-a3/4 if 8*a1 -4*a2*a3 + a3|^3 = 0
otherwise ex p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 &
q = (8*a1 -4*a2*a3 + a3|^3)/64 &
r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 &
s1 = 2-root(1_root_of_cubic(-q|^2,p|^2-r,2*p)) &
s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)) & s3 = -q/(s1*s2) &
it = -s1-s2+s3-a3/4;
func 3_root_of_quartic(a0,a1,a2,a3) -> complex number means
:: POLYEQ_5:def 7
ex p,r,s1 st p = (8*a2-3*a3|^2)/32 &
r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(p|^2-r) &
it = 2-root(-2*(p+s1))-a3/4 if 8*a1 -4*a2*a3 + a3|^3 = 0
otherwise ex p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 &
q = (8*a1 -4*a2*a3 + a3|^3)/64 &
r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 &
s1 = 2-root(1_root_of_cubic(-q|^2,p|^2-r,2*p)) &
s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)) & s3 = -q/(s1*s2) &
it = -s1+s2-s3-a3/4;
func 4_root_of_quartic(a0,a1,a2,a3) -> complex number means
:: POLYEQ_5:def 8
ex p,r,s1 st p = (8*a2-3*a3|^2)/32 &
r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(p|^2-r) &
it = -2-root(-2*(p+s1))-a3/4 if 8*a1 -4*a2*a3 + a3|^3 = 0
otherwise ex p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 &
q = (8*a1 -4*a2*a3 + a3|^3)/64 &
r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 &
s1 = 2-root(1_root_of_cubic(-q|^2,p|^2-r,2*p)) &
s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)) & s3 = -q/(s1*s2) &
it = s1-s2-s3-a3/4;
end;
theorem :: POLYEQ_5:30
a4 <> 0 implies (a4*z|^4 + a3*z|^3 + a2*z|^2 + a1*z + a0 = 0
iff z = 1_root_of_quartic(a0/a4,a1/a4,a2/a4,a3/a4) or
z = 2_root_of_quartic(a0/a4,a1/a4,a2/a4,a3/a4) or
z = 3_root_of_quartic(a0/a4,a1/a4,a2/a4,a3/a4) or
z = 4_root_of_quartic(a0/a4,a1/a4,a2/a4,a3/a4));
theorem :: NAT_5:22
n is prime iff (n-'1)! + 1 mod n = 0 & n>1;
52. The Number of Subsets of a Set
CARD_2:31
theorem :: CARD_2:31
exp(2,Card X) = Card bool X;
54. Konigsberg Bridges Problem
GRAPH_3A:5
theorem :: GRAPH_3A:5
not ex p being Path of KoenigsbergBridges st p is cyclic Eulerian;
55. Product of Segments of Chords
EUCLID_6:38
theorem :: EUCLID_6:38
p1 in circle(a,b,r) & p2 in circle(a,b,r) & p3 in circle(a,b,r) &
p4 in circle(a,b,r) & p in LSeg(p1,p3) & p in LSeg(p2,p4) implies
|.p1-p.|*|.p-p3.| = |.p2-p.|*|.p-p4.|;
57. Heron's Formula
EUCLID_6:39
theorem :: EUCLID_6:39
a = |.p2-p1.| & b = |.p3-p2.| & c = |.p1-p3.| &
s = the_perimeter_of_polygon3(p1,p2,p3)/2 implies
abs(the_area_of_polygon3(p1,p2,p3)) = sqrt(s*(s-a)*(s-b)*(s-c));
58. Formula for the Number of Combinations
CARD_FIN:16
theorem :: CARD_FIN:16
x<>y implies card Choose(X,k,x,y)=card X choose k;
60. Bezout's Theorem
NEWTON:67
theorem :: NEWTON:67 for m,n st m>0 or n>0 holds ex i,i1 st i*m + i1*n = m hcf n;
61. Theorem of Ceva
MENELAUS:21
theorem :: MENELAUS:21
(A, B, C is_a_triangle &
A1 = (1 - lambda) * B + lambda * C &
B1 = (1 - mu) * C + mu * A &
C1 = (1 - nu) * A + nu * B &
lambda <> 1 & mu <> 1 & nu <> 1 & ((1 - mu) + lambda * mu) <> 0 &
((1 - lambda) + nu * lambda) <> 0 & ((1 - nu) + mu * nu) <> 0) implies
((lambda / (1 - lambda)) * (mu / (1 - mu)) * (nu / (1 - nu)) = 1
iff
(ex A2 st A, A1, A2 is_collinear &
B, B1, A2 is_collinear &
C, C1, A2 is_collinear));
63. Cantor's Theorem
CARD_1:14
theorem :: CARD_1:14
Card X <` Card bool X;
64. L'Hôpital's Rule
L_HOSPIT:10
theorem :: L_HOSPIT:10
(ex N being Neighbourhood of x0 st f is_differentiable_on N &
g is_differentiable_on N & N \ {x0} c= dom (f/g) &
N c= dom ((f`|N)/(g`|N)) & f.x0 = 0 & g.x0 = 0 &
(f`|N)/(g`|N) is_continuous_in x0)
implies f/g is_convergent_in x0 & lim(f/g,x0) = diff(f,x0)/diff(g,x0);
65. Isosceles Triangle Theorem
EUCLID_6:16
theorem :: EUCLID_6:16
|.p3-p1.|=|.p2-p3.| & p1<>p2 implies angle(p3,p1,p2)=angle(p1,p2,p3);
66. Sum of a Geometric Series
SERIES_1:22
theorem :: SERIES_1:22 a <> 1 implies Partial_Sums(a GeoSeq).n = (1 - a to_power (n+1))/(1-a);
68. Sum of an arithmetic series
SERIES_2:42
theorem :: SERIES_2:42
(for n holds s.n = a*n+b) implies
for n holds Partial_Sums(s).n = (n+1)*(s.0 + s.n)/2;
69. Greatest Common Divisor Algorithm
NAT_D:sch 1
scheme :: NAT_D:sch 1
Euklides { Q(Nat)->Nat, a,b()->Nat } :
ex n st Q(n) = a() hcf b() & Q(n + 1) = 0
provided
0 < b() & b() < a() and
Q(0) = a() & Q(1) = b() and
for n holds Q(n + 2) = Q(n) mod Q(n + 1);
70. The Perfect Number Theorem
NAT_5:39
theorem :: NAT_5:39
n0 is even & n0 is perfect implies
ex p being natural number
st 2|^p -' 1 is prime & n0 = 2|^(p -' 1)*(2|^p -' 1);
71. Order of a Subgroup
GROUP_2:147
theorem :: GROUP_2:147 G is finite implies ord G = ord H * index H;
72. Sylow's Theorem
GROUP_10:10
theorem :: GROUP_10:12
for G being finite Group, p being prime (natural number)
holds ex P being Subgroup of G st P is_Sylow_p-subgroup_of_prime p;
theorem :: GROUP_10:12
for G being finite Group, p being prime (natural number) holds
(for H being Subgroup of G st H is_p-group_of_prime p holds
ex P being Subgroup of G st
P is_Sylow_p-subgroup_of_prime p & H is Subgroup of P) &
(for P1,P2 being Subgroup of G
st P1 is_Sylow_p-subgroup_of_prime p & P2 is_Sylow_p-subgroup_of_prime p
holds P1,P2 are_conjugated);
theorem :: GROUP_10:13
for G being finite Group, p being prime (natural number) holds
card the_sylow_p-subgroups_of_prime(p,G) mod p = 1 &
card the_sylow_p-subgroups_of_prime(p,G) divides ord G;
73. Ascending or Descending Sequences
DILWORTH:56
theorem :: DILWORTH:56
for f being real-valued FinSequence, n being Nat
st card f = n^2+1 & f is one-to-one
ex g being real-valued FinSubsequence
st g c= f & card g >= n+1 & (g is increasing or g is decreasing);
74. The Principle of Mathematical Induction
NAT_1:sch 2
scheme :: NAT_1:sch 2
Ind { P[Nat] } :
for k being Nat holds P[k]
provided
P[0] and
for k being Nat st P[k] holds P[k + 1];
75. The Mean Value Theorem
ROLLE:3
theorem :: ROLLE:3 for p,g st p<g for f st f is_continuous_on [.p,g.] & f is_differentiable_on ].p,g.[ ex x0 st x0 in ].p,g.[ & diff(f,x0)=(f.g-f.p)/(g-p);
78. The Cauchy-Schwarz Inequality
HERMITAN:45
theorem :: HERMITAN:45 :: Schwarz inequality for V be VectSp of F_Complex, v,w be Vector of V for f be diagReR+0valued hermitan-Form of V holds |. f.[v,w] .|^2 <= signnorm(f,v) * signnorm(f,w);
79. The Intermediate Value Theorem
TOPREAL5:4
theorem :: TOPREAL5:8 :: General Intermediate Value Point Theorem
for X being non empty TopSpace,xa,xb being Point of X,
a,b,d being Real,f being continuous map of X,R^1 st
X is connected & f.xa=a & f.xb=b & a<=d & d<=b
ex xc being Point of X st f.xc =d;
80. The Fundamental Theorem of Arithmetic
NAT_3:61
theorem :: NAT_3:61 Product ppf n = n;
theorem :: INT_7:15
for p,q be bag of SetPrimes st p is prime-factorization-like &q
is prime-factorization-like& Product p = Product q holds p=q;
83. The Friendship Theorem
FRIENDS1:14
theorem :: FRIENDS1:14
FSG is non empty implies FSG is with_universal_friend;
84. Morley's Theorem
EUCLID11:22
theorem :: EUCLID11:22
A,B,C is_a_triangle & angle(A,B,C) < PI &
angle(E,C,A) = angle(B,C,A) / 3 &
angle(C,A,E) = angle(C,A,B) / 3 &
angle(A,B,F) = angle(A,B,C) / 3 &
angle(F,A,B) = angle(C,A,B) / 3 &
angle(B,C,G) = angle(B,C,A) / 3 &
angle(G,B,C) = angle(A,B,C) / 3
implies
|.F-E.| = |.G-F.| & |.F-E.| = |.E-G.| & |.G-F.| = |.E-G.|;
85. Divisibility by 3 Rule
NUMERAL1:9
theorem :: NUMERAL1:9
for n being natural number holds
3 divides n iff 3 divides Sum digits(n,10);
86. Lebesgue Measure and Integration
MESFUNC5:def 16
definition
let X be non empty set;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,ExtREAL;
func Integral(M,f) -> Element of ExtREAL equals
:: MESFUNC5:def 16
integral+(M,max+f)-integral+(M,max-f);
end;
87. Desargues's Theorem
registration in
ANPROJ_2
registration let V be up-3-dimensional RealLinearSpace; cluster ProjectiveSpace V -> Fanoian Desarguesian Pappian; end;
88. Derangements Formula
CARDFIN2:10
theorem :: CARDFIN2:10
for s being non empty finite set
holds card (derangements s) = round ((card s)! / number_e);
89. The Factor and Remainder Theorems
UPROOTS:50
theorem :: UPROOTS:50 :: Factor theorem (Bezout)
for L being non degenerated comRing, r being Element of L,
p being Polynomial of L st r is_a_root_of p holds
p = <%-r,1.L%>*'poly_quotient(p,r);
91. The Triangle Inequality
EUCLID:16
theorem :: EUCLID:16 |.x1 - x2.| <= |.x1.| + |.x2.|;
93. The Birthday Problem
CARDFIN2:18
theorem :: CARDFIN2:18
for s, t being non empty finite set st card s = 23 & card t = 365
holds prob (not-one-to-one (s, t)) > 1/2;
94. The Law of Cosines
EUCLID_6:7
theorem :: EUCLID_6:7
a = |.p1-p2.| & b = |.p3-p2.| & c = |.p3-p1.|
implies c^2 = a^2 + b^2 - 2*a*b * cos angle(p1,p2,p3);
95. Ptolemy's Theorem
EUCLID_6:40
theorem :: EUCLID_6:40
p1 in circle(a,b,r) & p2 in circle(a,b,r) & p3 in circle(a,b,r) &
p4 in circle(a,b,r) & p in LSeg(p1,p3) & p in LSeg(p2,p4) implies
|.p3-p1.|*|.p4-p2.| = |.p2-p1.|*|.p4-p3.| + |.p3-p2.|*|.p4-p1.|;
96. Principle of Inclusion/Exclusion
CARD_FIN:56
theorem :: CARD_FIN:56
for Fy be finite-yielding Function,X st dom Fy=X
for XFS be XFinSequence of INT st
dom XFS= card X &
for n st n in dom XFS holds XFS.n=((-1)|^n)*Card_Intersection(Fy,n+1)
holds
Card union rng Fy=Sum XFS;
theorem :: LAPLACE:40
for A be Matrix of n,K st Det A <> 0.K
for x,b be FinSequence of K st len x = n & x * A = <*b*> holds
<*x*> = b * A~ &
for i st i in Seg n holds
x.i = (Det A)" * Det ReplaceLine(A,i,b);
98. Bertrand's Postulate
NAT_4:56
theorem :: NAT_4:56
for n being Element of NAT st n>=1 holds ex p being Prime st n<p & p<=2*n;