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:75
theorem :: POLYNOM5:75
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:55
theorem :: EUCLID_3:55
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:33
theorem :: EULER_2:33 ::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:97
theorem :: NEWTON:97 ::Euklidesa::
SetPrimes is infinite;
13. Polyhedron Formula
POLYFORM:92
theorem :: POLYFORM:92
p is simply-connected & dim(p) = 3
implies num-vertices(p) - num-edges(p) + num-faces(p) = 2;
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:51
theorem :: SIN_COS3:51 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);
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:12
theorem :: KNASTER:12 :: 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:98
theorem :: COMPLEX2:98
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);
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:37
theorem :: SERIES_1:37
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);
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 ;
POLYEQ_5:16
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);
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:26
theorem :: BINOM:26
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);
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));
51. Wilson's Theorem
NAT_5:22
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:44
theorem :: CARD_2:44
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:18
theorem :: CARD_FIN:18
x<>y implies card Choose(X,k,x,y)=card X choose k;
60. Bezout's Theorem
NEWTON:81
theorem :: NEWTON:81 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:30
theorem :: CARD_1:30
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:19
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:26
theorem :: SERIES_1:26 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_1:sch 8
scheme :: NAT_1:sch 8
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:177
theorem :: GROUP_2:177 G is finite implies ord G = ord H * index H;
72. Sylow's Theorem
GROUP_10:12
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;
GROUP_10:14
theorem :: GROUP_10:14
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);
GROUP_10:15
theorem :: GROUP_10:15
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 1
scheme :: NAT_1:sch 1
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:48
theorem :: HERMITAN:48 :: 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:10
theorem :: TOPREAL5:10 ::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;
INT_7:15
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:12
theorem :: NUMERAL1:12
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:52
theorem :: UPROOTS:52 :: 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;
96. Principle of Inclusion/Exclusion
CARD_FIN:67
theorem :: CARD_FIN:67
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;
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. 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;
97. Cramer's Rule
LAPLACE:40
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);