## Formalizing 100 Theorems in Mizar

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

```  theorem :: IRRAT_1:1
p is prime implies sqrt p is irrational;
```
```  theorem :: POLYNOM5:74
for p be Polynomial of F_Complex st len p > 1 holds
p is with_roots;
```
```  theorem :: TOPGEN_3:17
Card RAT = alef 0;
```
```  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);
```
```  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));
```
```  theorem :: EULER_2:18 ::Euler's theorem
a <> 0 & m > 1 & a,m are_relative_prime
implies (a |^ Euler m) mod m = 1;
```
```  theorem :: NEWTON:79
SetPrimes is infinite;
```
```  theorem :: POLYFORM:91
p is simply-connected & dim(p) = 3
implies num-vertices(p) - num-edges(p) + num-faces(p) = 2;
```
```  theorem :: BASEL_2:32
Sum Basel-seq = PI^2/6;
```
```  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);
```
```  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);
```
```  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;
```
```  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 ;
```
```  theorem :: NAT_5:23
p is prime & p mod 4 = 1 implies ex n,m st p = n^2 + m^2;
```
```  theorem :: TOPGEN_3:30
alef 0 <` continuum;
```
```  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;
```
```  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;
```
```  theorem :: LEIBNIZ1:14
PI/4 = Sum Leibniz_Series;
```
```  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);
```
```  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;
```

```  theorem :: BALLOT_1:28
A <> B & n >= k implies prob DominatedElection(A,n,B,k) = (n-k) / (n+k);
```
```  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;
```
```  theorem :: SERIES_1:33
p<=1 & (for n st n>=1 holds s.n=1/n to_power p) implies s is not summable;
```
```  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)!);
```
```  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;
```
```  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);
```
```  theorem :: RVSUM_3:47
for f being non empty positive real-valued FinSequence holds
GMean f <= Mean f;
```
```  theorem :: PELLS_EQ:14
D is non square implies
ex x,y be Nat st x^2 - D * y^2 = 1 & y <> 0;
```
```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;
```
```  theorem :: BINOM:25
for R being Abelian add-associative left_zeroed right_zeroed
distributive unital (non empty doubleLoopStr),
a,b being Element of R,
n being Nat
holds (a+b)|^n = Sum((a,b) In_Power n);
```
```  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;
```
```  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;
```
```  theorem :: CARD_2:31
exp(2,Card X) = Card bool X;
```
```  theorem :: GRAPH_3A:5
not ex p being Path of KoenigsbergBridges st p is cyclic Eulerian;
```
```  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.|;
```
```  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));
```
```  theorem :: CARD_FIN:16
x<>y implies card Choose(X,k,x,y)=card X choose k;
```
```  theorem :: NEWTON:67
for m,n st m>0 or n>0 holds ex i,i1 st i*m + i1*n = m hcf n;
```
```  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));
```
```  theorem :: CARD_1:14
Card X <` Card bool X;
```
```  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);
```
```  theorem :: EUCLID_6:16
|.p3-p1.|=|.p2-p3.| & p1<>p2 implies angle(p3,p1,p2)=angle(p1,p2,p3);
```
```  theorem :: SERIES_1:22
a <> 1 implies Partial_Sums(a GeoSeq).n = (1 - a to_power (n+1))/(1-a);
```
```  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;
```
```  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);
```
```  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);
```
```  theorem :: GROUP_2:147
G is finite implies ord G = ord H * index H;
```
```  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;
```
```  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);
```
```  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];
```
```  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);
```
```  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);
```
```  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;
```
```  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;
```
```  theorem :: FRIENDS1:14
FSG is non empty implies FSG is with_universal_friend;
```
```  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.|;
```
```  theorem :: NUMERAL1:9
for n being natural number holds
3 divides n iff 3 divides Sum digits(n,10);
```
```  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;
```
```  theorem :: CARDFIN2:10
for s being non empty finite set
holds card (derangements s) = round ((card s)! / number_e);
```
```  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);
```
```  theorem :: EUCLID:16
|.x1 - x2.| <= |.x1.| + |.x2.|;
```
```  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;
```
```  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);
```
```  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.|;
```
```  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);
```
```  theorem :: NAT_4:56
for n being Element of NAT st n>=1 holds ex p being Prime st n<p & p<=2*n;
```