1 by INT_2:def 4;
A7: x>1 by INT_2:def 4;
then x|^xca divides a by NAT_3:def 7;
then
A8: p|-count a1 =(p|-count a)-'(p|-count x|^xca) by A3,A5,NAT_3:31;
x|^xcb divides b by A7,NAT_3:def 7;
then
A9: p|-count b1 = (p|-count b)-'(p|-count x|^xcb) by A4,A5,NAT_3:31;
per cases;
suppose
x=p;
then p|-count x|^xca = p|-count a by A6,NAT_3:25;
hence thesis by A8,NAT_2:8;
end;
suppose
A10: x<>p;
p|-count x|^xcb=xcb * (p|-count x) by A5,NAT_3:32
.= xcb * 0 by A6,A10,NAT_3:24
.= 0;
then
A11: p|-count b1=(p|-count b)-0 by A9,XREAL_1:233
.=p|-count b;
p|-count x|^xca=xca * (p|-count x) by A5,NAT_3:32
.= xca * 0 by A6,A10,NAT_3:24
.= 0;
then p|-count a1=(p|-count a)-0 by A8,XREAL_1:233
.=p|-count a;
hence thesis by A2,A5,A11;
end;
end;
A12: for a being non zero Nat, x being Prime holds a div (x|^(x|-count a))
is non zero Nat
proof
let a be non zero Nat;
let x be Prime;
assume
A13: not a div (x|^(x|-count a)) is non zero Nat;
set xca=x|^(x|-count a);
x>1 by INT_2:def 4;
then
A14: xca divides a by NAT_3:def 7;
ex t being Nat st a = xca * (0 qua Nat) + t & t < xca by A13,NAT_D:def 1;
hence contradiction by A14,NAT_D:7;
end;
defpred P[Nat] means for a,b being non zero Nat st card(support
pfexp b)=$1 holds (for p being Element of NAT st p is prime holds p |-count a
<= p |-count b) implies (ex c being Element of NAT st b=a*c);
let a,b be non zero Nat;
assume
A15: for p being Element of NAT st p is prime holds p |-count a <= p |-count b;
A16: ex n1 being Element of NAT st n1=card(support pfexp b);
A17: for n1,n2 being non zero Nat st n1 divides n2 holds (n2 div n1)*n1 = n2
proof
let n1,n2 be non zero Nat;
assume n1 divides n2;
then ex a being Nat st n2=n1*a by NAT_D:def 3;
hence thesis by NAT_D:18;
end;
A18: for b,b1 being non zero Nat, x being Prime, n being Element of NAT st
card(support pfexp b)=n+1 & b1=b div (x|^(x|-count b)) & x in support pfexp b
holds card(support pfexp b1)=n
proof
let b,b1 be non zero Nat;
let x be Prime;
let n be Element of NAT;
assume
A19: card(support pfexp b)=n+1;
set xcb=x|-count b;
assume
A20: b1=b div (x|^(x|-count b));
A21: x>1 by INT_2:def 4;
then x|^xcb divides b by NAT_3:def 7;
then
A22: b=b1*x|^xcb by A17,A20;
reconsider b1 as Element of NAT by ORDINAL1:def 12;
A23: b1,x are_coprime
proof
assume not b1,x are_coprime;
then b1 gcd x = x by PEPIN:2;
then x divides b1 by NAT_D:def 5;
then consider c be Nat such that
A24: b1=x*c by NAT_D:def 3;
A25: not x|^(xcb+1) divides b by A21,NAT_3:def 7;
x|^xcb divides b by A21,NAT_3:def 7;
then b = x*c*x|^xcb by A17,A20,A24
.= c*(x|^xcb*x)
.= c*x|^(xcb+1) by NEWTON:6;
hence contradiction by A25,NAT_D:def 3;
end;
assume x in support pfexp b;
then (pfexp b).x<>0 by PRE_POLY:def 7;
then
A26: xcb<>0 by NAT_3:def 8;
reconsider b1 as non zero Nat;
card support pfexp (x|^xcb*b1) = card support pfexp x|^xcb + card
support pfexp b1 by A23,EULER_2:17,NAT_3:47;
then n+1=card {x} + card support pfexp b1 by A19,A22,A26,NAT_3:42;
then n+1=1+card (support pfexp b1) by CARD_2:42;
hence thesis;
end;
A27: for n being Nat holds P[n] implies P[n+1]
proof
let n be Nat;
assume
A28: P[n];
for a,b being non zero Nat st card(support pfexp b)=n+1 holds (for p
being Element of NAT st p is prime holds p |-count a <= p |-count b) implies ex
c being Element of NAT st b=a*c
proof
let a,b be non zero Nat;
assume
A29: card(support pfexp b)=n+1;
then support pfexp b<>{};
then consider x being object such that
A30: x in support pfexp b;
reconsider x as Prime by A30,NAT_3:34;
set a1=a div (x|^(x|-count a));
set b1=b div (x|^(x|-count b));
reconsider a1,b1 as non zero Nat by A12;
assume
A31: for p being Element of NAT st p is prime holds p |-count a <= p
|-count b;
then
A32: for p being Element of NAT st p is prime holds p |-count a1 <= p
|-count b1 by A1;
set xca=x|-count a;
set xcb=x|-count b;
x in NAT by ORDINAL1:def 12;
then
A33: xcb-xca=xcb-'xca by A31,XREAL_1:233;
n in NAT by ORDINAL1:def 12;
then card(support pfexp b1)=n by A18,A29,A30;
then consider d be Element of NAT such that
A34: b1=a1*d by A28,A32;
reconsider e=d*x|^(xcb-'xca) as Element of NAT by ORDINAL1:def 12;
take e;
A35: x<>1 by INT_2:def 4;
then
A36: x|^(xca) divides a by NAT_3:def 7;
x|^(xcb) divides b by A35,NAT_3:def 7;
then b = d*(a div (x|^xca))*(x|^(xca+(xcb-'xca))) by A17,A34,A33
.= d*(a div (x|^xca))*(x|^xca*x|^(xcb-'xca)) by NEWTON:8
.= d*((a div (x|^xca))*x|^xca)*x|^(xcb-'xca)
.= d*a*x|^(xcb-'xca) by A17,A36
.= a*(d*x|^(xcb-'xca));
hence thesis;
end;
hence thesis;
end;
A37: P[0]
proof
let a,b be non zero Nat;
assume
A38: card support pfexp b=0;
(for p being Element of NAT st p is prime holds p |-count a <= p
|-count b) implies ex c being Element of NAT st b=a*c
proof
set d=1;
assume
A39: for p being Element of NAT st p is prime holds p |-count a <= p
|-count b;
take d;
A40: (support pfexp b)={} by A38;
(support pfexp a)={}
proof
assume (support pfexp a)<>{};
then consider x be object such that
A41: x in support pfexp a;
reconsider x as Prime by A41,NAT_3:34;
reconsider x as prime Element of NAT by ORDINAL1:def 12;
(pfexp a).x<>0 by A41,PRE_POLY:def 7;
then x|-count a<>0 by NAT_3:def 8;
then x|-count b>0 by A39;
then (pfexp b).x<>0 by NAT_3:def 8;
hence contradiction by A40,PRE_POLY:def 7;
end;
then a=1 by NAT_3:52;
hence thesis by A40,NAT_3:52;
end;
hence thesis;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A37,A27);
hence thesis by A15,A16;
end;
theorem Th21:
for a,b being non zero Nat holds (for p being Element of NAT st
p is prime holds p |-count a = p |-count b) implies a=b
proof
let a,b be non zero Nat;
assume
A1: for p being Element of NAT st p is prime holds p |-count a = p |-count b;
then
for p being Element of NAT st p is prime holds p |-count a <= p |-count b;
then consider c being Element of NAT such that
A2: b=a*c by Th20;
for p being Element of NAT st p is prime holds p |-count b <= p |-count
a by A1;
then consider d being Element of NAT such that
A3: a=b*d by Th20;
a=a*(c*d) by A2,A3;
then c = 1 by NAT_1:15,XCMPLX_1:7;
hence thesis by A2;
end;
theorem Th22:
for p1,p2 being Prime, m being non zero Element of NAT st p1|^(
p1 |-count m) = p2|^(p2 |-count m) & p1 |-count m > 0 holds p1=p2
proof
let p1,p2 be Prime;
let m be non zero Element of NAT;
assume
A1: p1|^(p1 |-count m) = p2|^(p2 |-count m);
A2: p1 > 1 by INT_2:def 4;
assume p1 |-count m > 0;
then p1 to_power (p1 |-count m) > 1 by A2,POWER:35;
then
A3: p1|^(p1|-count m) > 1 by POWER:41;
assume p1 <> p2;
then p1 <> 1 & not p1 divides p2|^(p2 |-count m) by INT_2:def 4,NAT_3:6;
then p1 |-count (p1|^(p1 |-count m)) = 0 by A1,NAT_3:27;
then p1 |-count m = 0 by A2,NAT_3:25;
hence contradiction by A3,NEWTON:4;
end;
begin :: Pocklington's theorem.
theorem Th23:
for n,k,q,p,n1,p,a being Element of NAT st n-1=k*q|^n1 & k>0 &
n1>0 & q is prime & a|^(n-'1) mod n = 1 & p is prime & p divides n holds p
divides (a|^((n-'1) div q) -' 1) or p mod q|^n1 = 1
proof
let n,k,q,p,n1,p,a be Element of NAT;
assume that
A1: n-1=k*q|^n1 and
A2: k>0 and
A3: n1>0 and
A4: q is prime;
A5: n-1+1 > 0+1 by A1,A2,A4,XREAL_1:6;
assume
A6: a|^(n-'1) mod n = 1;
a|^((n-'1) div q)>=1
proof
assume a|^((n-'1) div q)<1;
then
A7: a=0 by NAT_1:14;
n-'1 + 1 > 1 by A5,XREAL_1:233;
then n-'1 >= 1 by NAT_1:13;
then a|^(n-'1) mod n = 0*n mod n by A7,NEWTON:11
.= 0 by NAT_D:13;
hence contradiction by A6;
end;
then
A8: a|^((n-'1) div q)-'1=a|^((n-'1) div q)-1 by XREAL_1:233;
n1+1 > 0+1 by A3,XREAL_1:6;
then n1>=1 by NAT_1:13;
then
A9: n1-'1=n1-1 by XREAL_1:233;
then
A10: (n-'1) div q = (q|^(n1-'1+1))*k div q by A1,A5,XREAL_1:233
.=q*q|^(n1-'1)*k div q by NEWTON:6
.=q*(q|^(n1-'1)*k) div q
.=k*q|^(n1-'1) by A4,NAT_D:18;
assume that
A11: p is prime and
A12: p divides n;
consider i being Nat such that
A13: n=p*i by A12,NAT_D:def 3;
assume not p divides (a|^((n-'1) div q)-'1);
then
A14: not a|^((n-'1) div q) mod p = 1 by A11,A8,PEPIN:8;
set nn=n-'1;
n1+1 > 0+1 by A3,XREAL_1:6;
then n1>=1 by NAT_1:13;
then
A15: n1-'1=n1-1 by XREAL_1:233;
A16: p > 1 by A11,INT_2:def 4;
then p-'1=p-1 by XREAL_1:233;
then
A17: p-'1+1=p;
reconsider i as Element of NAT by ORDINAL1:def 12;
i*p<>0 by A1,A13;
then
A18: a|^(n-'1) mod p = 1 by A6,A16,A13,PEPIN:9;
0+1

1-1 by A7,XREAL_1:9;
then
A12: p-'1>0 by A7,XREAL_1:233;
A13: for q1 being Element of NAT st q1 in support (pfexp f) & q1 |-count f >
0 holds p mod q1|^(q1 |-count f) = 1
proof
let q1 be Element of NAT;
set n1=q1 |-count f;
assume
A14: q1 in support (pfexp f);
then
A15: q1 is prime by NAT_3:34;
A16: q1 is prime by A14,NAT_3:34;
then consider a be Element of NAT such that
A17: a|^(n-'1) mod n = 1 and
A18: (a|^((n-'1) div q1)-'1) gcd n = 1 by A5,A14,NAT_3:36;
assume
A19: q1 |-count f > 0;
A20: not p divides (a|^((n-'1) div q1)-'1)
by A6,NEWTON:50,A7,A18,NAT_D:7;
q1<>1 by A16,INT_2:def 4;
then q1|^(q1 |-count f) divides f by A2,NAT_3:def 7;
then consider d be Nat such that
A21: f=q1|^n1*d by NAT_D:def 3;
reconsider d as Element of NAT by ORDINAL1:def 12;
set k=d*c;
A22: k>0
proof
assume k<=0;
then d=0 by A3;
hence contradiction by A2,A21;
end;
n-1=k*q1|^n1 by A1,A21;
hence thesis by A6,A9,A19,A17,A22,A15,A20,Th23;
end;
for q1 being Element of NAT st q1 is prime holds q1 |-count f <= q1
|-count (p-'1)
proof
let q1 be Element of NAT;
assume
A23: q1 is prime;
per cases;
suppose
A24: q1 in support (pfexp f);
then (pfexp f).q1<>0 by PRE_POLY:def 7;
then q1 |-count f>0 by A23,NAT_3:def 8;
then p mod q1|^(q1 |-count f) = 1 by A13,A24;
then
A25: q1 |-count (q1|^(q1 |-count f)) <= q1 |-count (p-'1) by A11,A10,A23,
NAT_3:30,PEPIN:8;
q1>1 by A23,INT_2:def 4;
hence thesis by A25,NAT_3:25;
end;
suppose
not q1 in support (pfexp f);
then (pfexp f).q1=0 by PRE_POLY:def 7;
hence thesis by A23,NAT_3:def 8;
end;
end;
then ex n2 being Element of NAT st (p-'1)=f*n2 by A2,A12,Th20;
then f divides (p-'1) by NAT_D:def 3;
then f<=(p-'1) by A12,NAT_D:7;
then p-1+1>=f+1 by A10,XREAL_1:6;
then p>f by NAT_1:13;
then
A26: p^2>f^2 by SQUARE_1:16;
c>=0+1 by A3,NAT_1:13;
then
A27: c+1>=1+1 by XREAL_1:6;
f>=c+1 by A2,NAT_1:13;
then f>=2 by A27,XXREAL_0:2;
then f-1>=2-1 by XREAL_1:9;
then
A28: n+(f-1)>=n+1 by XREAL_1:6;
f>=c+1 by A2,NAT_1:13;
then f*f>=f*(c+1) by XREAL_1:64;
then p^2>f+(n-1) by A1,A26,XXREAL_0:2;
then p^2>=n+1 by A28,XXREAL_0:2;
hence contradiction by A8,NAT_1:13;
end;
::$N Pocklington's theorem
theorem Th25:
for n,f,d,n1,a,q being Element of NAT st n-1=q|^n1*d & q|^n1>d &
d>0 & q is prime & a|^(n-'1) mod n = 1 & (a|^((n-'1) div q)-'1) gcd n = 1 holds
n is prime
proof
let n,f,d,n1,a,q be Element of NAT;
assume that
A1: n-1=q|^n1*d & q|^n1>d & d>0 and
A2: q is prime;
set f=q|^n1;
assume
A3: a|^(n-'1) mod n = 1;
assume
A4: (a|^((n-'1) div q)-'1) gcd n = 1;
for q1 being Element of NAT st q1 divides f & q1 is prime holds ex a
being Element of NAT st a|^(n-'1) mod n = 1 & (a|^((n-'1) div q1)-'1) gcd n = 1
proof
let q1 be Element of NAT;
assume
A5: q1 divides f;
assume
A6: q1 is prime;
consider a be Element of NAT such that
A7: a|^(n-'1) mod n = 1 & (a|^((n-'1) div q)-'1) gcd n = 1 by A3,A4;
take a;
thus thesis by A2,A5,A6,A7,Th18;
end;
hence thesis by A1,Th24;
end;
Lm2: for n being Element of NAT st 1

=1 by FINSEQ_1:1; then m+(p |-count n) > 0+(p |-count n) by XREAL_1:6; then A25: x1 > p |-count n by A24,CARD_1:def 7; A26: not p |^ x1 divides n proof assume p |^ x1 divides n; then A27: p |-count (p |^ x1) <= p |-count n by A2,NAT_3:30; p>1 by INT_2:def 4; hence contradiction by A25,A27,NAT_3:25; end; ff2.m=0; then f1.x=0 by A23,A24,FINSEQ_1:def 7; hence thesis by A9,A10,A15,A26; end; end; take f; thus len f = n by A9,FINSEQ_1:def 3; thus for k being Element of NAT st k in dom f holds (f.k=1 iff p|^k divides n) & (f.k=0 iff not p|^k divides n) by A9,A10; dom f = dom f1 by A9,A13,FINSEQ_1:def 3; hence thesis by A14,A1,FUNCT_1:2; end; theorem Th47: for n being Element of NAT, p being Prime ex f being FinSequence of NAT st len f = n & (for k being Element of NAT st k in dom f holds f.k=[\ n/ (p|^k) /]) & p |-count (n!) = Sum f proof defpred P[Nat] means for p being Prime ex f being FinSequence of NAT st len f = $1 & (for k being Element of NAT st k in dom f holds f.k=[\ $1/( p|^k) /]) & p |-count ($1!) = Sum f; let n be Element of NAT; let p be Prime; A1: for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume A2: P[n]; for p being Prime ex f being FinSequence of NAT st len f = n+1 & (for k being Element of NAT st k in dom f holds f.k=[\ (n+1)/(p|^k) /]) & p |-count ((n+1)!) = Sum f proof let p be Prime; consider fn being FinSequence of NAT such that A3: len fn = n and A4: for k being Element of NAT st k in dom fn holds fn.k=[\ n/(p|^k) /] and A5: p |-count (n!) = Sum fn by A2; reconsider fnn=fn as FinSequence of REAL by FINSEQ_2:24,NUMBERS:19; set fn0=fnn ^ <* In(0,REAL) *>; consider fn1 being FinSequence of NAT such that A6: len fn1 = n + 1 and A7: for k being Element of NAT st k in dom fn1 holds (fn1.k=1 iff p |^k divides (n+1)) & (fn1.k=0 iff not p|^k divides (n+1)) and A8: p |-count (n+1) = Sum fn1 by Th46; A9: Seg(n+1) = dom fn1 by A6,FINSEQ_1:def 3; set f = (fn ^ <* 0 *>)+fn1; for y being object st y in rng f holds y in NAT by ORDINAL1:def 12; then rng f c= NAT; then reconsider f as FinSequence of NAT by FINSEQ_1:def 4; take f; reconsider fn0 as FinSequence of REAL; reconsider fn1 as FinSequence of REAL by FINSEQ_2:24,NUMBERS:19; A10: dom f = dom fn0 /\ dom fn1 by VALUED_1:def 1; A11: len fn0 = len fn + len <* 0 *> by FINSEQ_1:22 .= n + 1 by A3,FINSEQ_1:39; then Seg(n+1) = dom fn0 by FINSEQ_1:def 3; hence len f = n+1 by A10,A9,FINSEQ_1:def 3; thus for k being Element of NAT st k in dom f holds f.k=[\ (n+1)/(p|^k) /] proof let k be Element of NAT; A12: (p|^k)/(p|^k)=1 by XCMPLX_1:60; assume A13: k in dom f; then A14: f.k = fn0.k + fn1.k by VALUED_1:def 1; A15: k in dom fn0 by A10,A13,XBOOLE_0:def 4; A16: fn0.k=[\ n/(p|^k) /] proof per cases by A15,FINSEQ_1:25; suppose A17: k in dom fn; then fn.k=[\ n/(p|^k) /] by A4; hence thesis by A17,FINSEQ_1:def 7; end; suppose ex n1 being Nat st n1 in dom <* 0 *> & k=len fn + n1; then consider n1 being Nat such that A18: n1 in dom <* 0 *> and A19: k=len fn + n1; n1 in Seg 1 by A18,FINSEQ_1:38; then A20: n1=1 by FINSEQ_1:2,TARSKI:def 1; p>1 by INT_2:def 4; then A21: p*p|^n>1*p|^n & p|^n>n by Th3,XREAL_1:68; p|^(n+1)=p|^n*p by NEWTON:6; then p|^k>n by A3,A19,A20,A21,XXREAL_0:2; then n/(p|^k)<1 by XREAL_1:189; then A22: n/(p|^k)-1<1-1 by XREAL_1:9; fn0.(n+1)=<* 0 *>.1 by A3,A18,A20,FINSEQ_1:def 7; then fn0.k=0 by A3,A19,A20,FINSEQ_1:40; hence thesis by A22,INT_1:def 6; end; end; A23: k in dom fn1 by A10,A13,XBOOLE_0:def 4; per cases; suppose A24: p|^k divides (n+1); then consider r being Nat such that A25: n+1=(p|^k)*r by NAT_D:def 3; A26: (n+1)/(p|^k) = r/((p|^k)/(p|^k)) by A25,XCMPLX_1:77 .= r/(1/1) by XCMPLX_1:60 .= r; ((p|^k)/(p|^k))+((-1)/(p|^k))-1<0 by A12; then A27: (p|^k+(-1))/(p|^k)-1<0 by XCMPLX_1:62; [\ n/(p|^k) /] + 1 = [\ n/(p|^k) +1 /] by INT_1:28 .=[\ n/(p|^k) + (p|^k)/(p|^k) /] by XCMPLX_1:60 .=[\ (n+p|^k)/(p|^k) /] by XCMPLX_1:62 .=[\ ((n+1)+(p|^k -1))/(p|^k) /] .=[\ (n+1)/(p|^k) + (p|^k-1)/(p|^k) /] by XCMPLX_1:62 .=(n+1)/(p|^k) + [\ (p|^k-1)/(p|^k) /] by A26,INT_1:28 .=(n+1)/(p|^k) + 0 by A27,INT_1:def 6 .=[\ (n+1)/(p|^k) /] by A26,INT_1:25; hence thesis by A7,A14,A23,A16,A24; end; suppose A28: not p|^k divides (n+1); set m=(n+1) mod (p|^k); set d=(n+1) div (p|^k); A29: n+1 = (p|^k) * d + m by NAT_D:2; then not m=0 by A28,NAT_D:def 3; then m+1>0+1 by XREAL_1:6; then m>=1 by NAT_1:13; then A30: m-1>=1-1 by XREAL_1:9; m

NAT; let p be Prime; take f; thus len f = 0; thus for k being Element of NAT st k in dom f holds f.k=[\ 0/(p|^k) /]; p<>1 by INT_2:def 4; hence thesis by NAT_3:21,NEWTON:12,RVSUM_1:72; end; for n being Nat holds P[n] from NAT_1:sch 2(A35,A1); then consider f being FinSequence of NAT such that A36: ( len f = n & for k being Element of NAT st k in dom f holds f.k=[\ n/(p|^k) /] )& p |-count (n!) = Sum f; take f; thus thesis by A36; end; theorem Th48: for n being Element of NAT, p being Prime ex f being FinSequence of REAL st len f = 2*n & (for k being Element of NAT st k in dom f holds f.k=[\ (2*n)/(p|^k)/] - 2*[\n/(p|^k)/]) & p |-count (2*n choose n) = Sum f proof let n be Element of NAT; let p be Prime; set f0=n|->0; consider f1 being FinSequence of NAT such that A1: len f1 = n and A2: for k being Element of NAT st k in dom f1 holds f1.k=[\ n/(p|^k) /] and A3: p |-count (n!) = Sum f1 by Th47; consider f2 being FinSequence of NAT such that A4: len f2 = 2*n and A5: for k being Element of NAT st k in dom f2 holds f2.k=[\ (2*n)/(p|^k) /] and A6: p |-count ((2*n)!) = Sum f2 by Th47; reconsider f2 as FinSequence of REAL by FINSEQ_2:24,NUMBERS:19; set f = f2+((-(f1^f0))+(-(f1^f0))); take f; A7: dom (f1^f0) = Seg (len f1 + len f0) by FINSEQ_1:def 7 .= Seg (n+n) by A1,CARD_1:def 7 .= Seg (2*n); A8: dom ((-(f1^f0))+(-(f1^f0))) = dom (-(f1^f0)) /\ dom (-(f1^f0)) by VALUED_1:def 1 .= Seg (2*n) by A7,VALUED_1:8; A9: dom f = dom f2 /\ dom ((-(f1^f0))+(-(f1^f0))) by VALUED_1:def 1 .= Seg (2*n) /\ Seg (2*n) by A4,A8,FINSEQ_1:def 3; hence len f = 2*n by FINSEQ_1:def 3; thus for k being Element of NAT st k in dom f holds f.k=[\(2*n)/(p|^k)/]- 2* [\n/(p|^k)/] proof let k be Element of NAT; assume A10: k in dom f; then A11: k in dom f2 by A4,A9,FINSEQ_1:def 3; A12: f.k = f2.k+((-(f1^f0))+(-(f1^f0))).k by A10,VALUED_1:def 1 .=f2.k+((-(f1^f0)).k+(-(f1^f0)).k) by A8,A9,A10,VALUED_1:def 1 .=f2.k+2*(-(f1^f0)).k .=f2.k+2*(-(f1^f0).k) by RVSUM_1:17 .=f2.k-2*(f1^f0).k .=[\(2*n)/(p|^k)/]-2*(f1^f0).k by A5,A11; per cases by A7,A9,A10,FINSEQ_1:25; suppose A13: k in dom f1; then (f1^f0).k=f1.k by FINSEQ_1:def 7 .=[\n/(p|^k)/] by A2,A13; hence thesis by A12; end; suppose ex e being Nat st e in dom f0 & k=len f1 + e; then consider e being Nat such that A14: e in dom f0 and A15: k=len f1 + e; dom f0 = Seg n by FUNCOP_1:13; then e >= 1 by A14,FINSEQ_1:1; then e + len f1 >= 1 + len f1 by XREAL_1:6; then A16: k > 1 + n or k = 1 + n by A1,A15,XXREAL_0:1; A17: (f1^f0).k = f0.e by A14,A15,FINSEQ_1:def 7 .= 0; p>1 by INT_2:def 4; then p to_power k >= p to_power (1+n) by A16,POWER:39; then p|^k >= p to_power (1+n) by POWER:41; then A18: p|^k >= p|^(1+n) by POWER:41; A19: p>1 by INT_2:def 4; then p*p|^n>1*p|^n by XREAL_1:68; then p|^(1+n)>p|^n by NEWTON:6; then A20: p|^k>p|^n by A18,XXREAL_0:2; per cases; suppose n=0; hence thesis by A12,A17,INT_1:25; end; suppose A21: n<>0; (p|^n)/(p|^n)>n/(p|^n) by A19,Th3,XREAL_1:74; then A22: 1>n/(p|^n) by XCMPLX_1:60; n/(p|^n)>n/(p|^k) by A20,A21,XREAL_1:76; then 1>n/(p|^k) by A22,XXREAL_0:2; then 1-1>n/(p|^k)-1 by XREAL_1:9; hence thesis by A12,A17,INT_1:def 6; end; end; end; p |-count (2*n choose n) = Sum f proof per cases; suppose A23: n=0; then A24: 2*n choose n = 1 by NEWTON:19; p>1 by INT_2:def 4; then A25: p |-count (2*n choose n) = 0 by A24,NAT_3:21; len f = 0 by A9,A23,FINSEQ_1:def 3; hence thesis by A25,PROB_3:62; end; suppose A26: n<>0; A27: 2*n-n=n; A28: n+n>n+0 by A26,XREAL_1:6; then (2*n choose n)*((n!)*(n!)) = ((2*n)!)/((n!)*(n!))*((n!)*(n!)) by A27 ,NEWTON:def 3 .= (2*n)! by XCMPLX_1:87; then A29: ((n!) * (n!)) divides ((2*n)!) by NAT_D:def 3; 2*n choose n = ((2*n)!)/((n!)*(n!)) by A28,A27,NEWTON:def 3; then A30: 2*n choose n = ((n!) * (n!)) * (((2*n)!) div ((n!) * (n!))) /((n!)* (n!)) by A29,NAT_D:3 .= ((2*n)!) div ((n!) * (n!)) by XCMPLX_1:89; A31: -(f1^f0) is Element of len(-(f1^f0))-tuples_on REAL by FINSEQ_2:92; A32: p |-count (((2*n)!) div ((n!)*(n!))) = p |-count ((2*n)!) -' p |-count ((n!)*(n!)) by A29,NAT_3:31 .= p |-count ((2*n)!) - p |-count ((n!)*(n!)) by A29,NAT_3:30 ,XREAL_1:233; A33: ((-(f1^f0))+(-(f1^f0))) is Element of len((-(f1^f0))+(-(f1^f0))) -tuples_on REAL by FINSEQ_2:92; len((-(f1^f0))+(-(f1^f0)))=len f2 & f2 is Element of len(f2) -tuples_on REAL by A4,A8,FINSEQ_1:def 3,FINSEQ_2:92; then Sum f = Sum f2 + Sum((-(f1^f0))+(-(f1^f0))) by A33,RVSUM_1:89 .= Sum f2 + (Sum(-(f1^f0)) + Sum(-(f1^f0))) by A31,RVSUM_1:89 .= Sum f2 + (- Sum(f1^f0) + Sum(-(f1^f0))) by RVSUM_1:88 .= Sum f2 + (- Sum(f1^f0) + (- Sum(f1^f0))) by RVSUM_1:88 .= Sum f2 - 2*Sum(f1^f0) .= Sum f2 - 2*(Sum(f1) + Sum(f0)) by RVSUM_1:75 .= Sum f2 - 2*(Sum f1 + n*0) by RVSUM_1:80 .= p |-count ((2*n)!) -(p |-count (n!) + p |-count (n!)) by A3,A6 .= p |-count (((2*n)!) div ((n!)*(n!))) by A32,NAT_3:28; hence thesis by A30; end; end; hence thesis; end; Lm8: for n,r being Element of NAT, p being Prime, f being FinSequence of REAL st p|^r <= 2*n & 2*n < p|^(r+1) & len f = 2*n & (for k being Element of NAT st k in dom f holds f.k=[\(2*n)/(p|^k)/] - 2*[\n/(p|^k)/]) holds Sum f <= r proof let n,r be Element of NAT; let p be Prime; let f be FinSequence of REAL; set f0 = (r |-> 1)^((2*n -' r)|-> 0); A1: p>1 by INT_2:def 4; assume A2: p|^r <= 2*n; A3: 2*n >= r proof assume 2*n < r; then p to_power (2*n)

1) + len((2*n -' r)|-> 0) by FINSEQ_1:22
.= r + len((2*n -' r)|->0) by CARD_1:def 7
.= r + (2*n -' r) by CARD_1:def 7
.= r + (2*n - r) by A3,XREAL_1:233
.= len f by A5;
assume
A7: for k being Element of NAT st k in dom f holds f.k=[\(2*n)/(p|^k)/]
- 2*[\n/(p|^k)/];
A8: for k be Element of NAT st k in dom f holds f.k <= f0.k
proof
let k be Element of NAT;
assume
A9: k in dom f;
then
A10: f.k=[\(2*n)/(p|^k)/] - 2*[\n/(p|^k)/] by A7;
k in Seg (2*n) by A5,A9,FINSEQ_1:def 3;
then
A11: k in dom f0 by A5,A6,FINSEQ_1:def 3;
per cases by A11,FINSEQ_1:25;
suppose
A12: k in dom (r |-> 1);
[\n/(p|^k)/] <= n/(p|^k) by INT_1:def 6;
then -[\n/(p|^k)/] >= -n/(p|^k) by XREAL_1:24;
then
(2*n)/(p|^k) - 1 < [\(2*n)/(p|^k)/] & (-[\n/(p|^k)/])*2 >= (-n/(p|^
k))*2 by INT_1:def 6,XREAL_1:64;
then ((2*n)/(p|^k) - 1) + 2*(-n/(p|^k)) < [\(2*n)/(p|^k)/] + (-2*[\n/(p
|^k)/]) by XREAL_1:8;
then [\(2*n)/(p|^k)/] -2*[\n/(p|^k)/] > 2*(n/(p|^k)) -1 + 2*(-n/(p|^k))
by XCMPLX_1:74;
then f.k >= -1 +1 by A10,INT_1:7;
then
A13: f.k is Element of NAT by A10,INT_1:3;
n/(p|^k) - 1 < [\n/(p|^k)/] by INT_1:def 6;
then -[\n/(p|^k)/] < -(n/(p|^k) - 1) by XREAL_1:24;
then [\(2*n)/(p|^k)/] <= (2*n)/(p|^k) & (-[\n/(p|^k)/])*2 < (-(n/(p|^k)
- 1))*2 by INT_1:def 6,XREAL_1:68;
then
(2*n)/(p|^k)= 2*(n/(p|^k)) & -2*[\n/(p|^k)/] + [\(2*n)/(p|^k)/] < 2
*(-n/(p|^ k) + 1) + (2*n)/(p|^k) by XCMPLX_1:74,XREAL_1:8;
then
A14: f.k < 1+1 by A10;
A15: k in Seg r by A12,FUNCOP_1:13;
f0.k = (r |-> 1).k by A12,FINSEQ_1:def 7
.= 1 by A15,FUNCOP_1:7;
hence thesis by A13,A14,NAT_1:13;
end;
suppose
A16: ex n0 being Nat st n0 in dom ((2*n -' r)|-> 0) & k=len (r |-> 1 )+ n0;
reconsider k1=k as Element of NAT;
consider n0 be Nat such that
A17: n0 in dom ((2*n -' r)|-> 0) and
A18: k=len (r |-> 1)+ n0 by A16;
n0 in Seg (2*n -' r) by A17,FUNCOP_1:13;
then 1<=n0 by FINSEQ_1:1;
then
A19: 1+r<=n0+r by XREAL_1:6;
k=r + n0 by A18,CARD_1:def 7;
then r+1

=3; A2: for n,r being Element of NAT, p being Prime st n>=2 & p|^r <= 2*n & 2*n < p|^(r+1) holds p |-count (2*n choose n) <= r proof let n,r be Element of NAT; let p be Prime; assume that n>=2 and A3: p|^r <= 2*n & 2*n < p|^(r+1); ex f be FinSequence of REAL st len f = 2*n &( for k being Element of NAT st k in dom f holds f.k=[\(2*n)/(p|^k)/] - 2*[\n/(p|^k)/])& p |-count (2*n choose n) = Sum f by Th48; hence thesis by A3,Lm8; end; thus p>2*n implies p |-count (2*n choose n) = 0 proof set r = 0; assume p>2*n; then A4: p|^(r+1)>2*n; A5: n>=2 by A1,XXREAL_0:2; then n*2>=2*2 by XREAL_1:64; then 2*n>=1 by XXREAL_0:2; then p|^r <= 2*n by NEWTON:4; hence thesis by A2,A5,A4; end; thus n

=2 by A1,XXREAL_0:2; then 2

0; assume A10: 2*n/3

1 by INT_2:def 4; then p to_power 2 <= p to_power k by A27,POWER:39; then p|^2 <= p to_power k by POWER:41; then A29: p|^2 <= p|^k by POWER:41; then 2*n < p|^k by A28,XXREAL_0:2; then 2*n/(p|^k) < (p|^k)/(p|^k) by XREAL_1:74; then 2*n/(p|^k) < 1 by XCMPLX_1:60; then 2*n/(p|^k) - 1 < 1-1 by XREAL_1:9; then A30: [\2*n/(p|^k)/] = 0 by INT_1:def 6; 1*n<=2*n by XREAL_1:64; then n

0 by A1,SQUARE_1:25; then sqrt(2*n)*sqrt(2*n)

=2 by A1,XXREAL_0:2; hence thesis by A2,A36,A35; end; assume p<=sqrt(2*n); then sqrt(2*n)*p >= p*p & sqrt(2*n)*sqrt(2*n) >= p*sqrt(2*n) by XREAL_1:64; then (sqrt(2*n))^2 >= p*p by XXREAL_0:2; then A37: 2*n>=p*p by SQUARE_1:def 2; set k0=p |-count (2*n choose n); set r = [\ log(p,2*n) /]; A38: r <= log(p,2*n) by INT_1:def 6; A39: log(p,2*n) - 1 < r by INT_1:def 6; A40: p>1 by INT_2:def 4; then p*p>1*p by XREAL_1:68; then 2*n>p by A37,XXREAL_0:2; then log(p,2*n)>log(p,p) by A40,POWER:57; then log(p,2*n)>1 by A40,POWER:52; then log(p,2*n)-1>1-1 by XREAL_1:9; then reconsider r as Element of NAT by A39,INT_1:3; r < log(p,2*n) or r = log(p,2*n) by A38,XXREAL_0:1; then p to_power r <= p to_power log(p,2*n) by A40,POWER:39; then p|^r <= p to_power log(p,2*n) by POWER:41; then A41: p|^r <= 2*n by A40,A37,POWER:def 3; log(p,2*n) - 1 +1 < r +1 by A39,XREAL_1:6; then p to_power log(p,2*n) < p to_power (r+1) by A40,POWER:39; then p to_power log(p,2*n) < p|^(r+1) by POWER:41; then A42: 2*n < p|^(r+1) by A40,POWER:def 3; n>=2 by A1,XXREAL_0:2; then k0 <= r by A2,A41,A42; then k0 = r or k0 < r by XXREAL_0:1; then p to_power k0 <= p to_power r by A40,POWER:39; then p|^k0 <= p to_power r by POWER:41; then p|^k0 <= p|^r by POWER:41; hence thesis by A41,XXREAL_0:2; end; definition let f be FinSequence of NAT,p be Prime; func p |-count f -> FinSequence of NAT means :Def1: len it = len f & for i being set st i in dom it holds it.i = p |-count f.i; existence proof deffunc F(Nat) = p |-count f.$1; consider g being FinSequence such that A1: len g = len f and A2: for k being Nat st k in dom g holds g.k = F(k) from FINSEQ_1:sch 2; now let y be object; assume y in rng g; then consider x be object such that A3: x in dom g and A4: y=g.x by FUNCT_1:def 3; reconsider x as Element of NAT by A3; y=F(x) by A2,A3,A4; hence y in NAT; end; then rng g c= NAT; then reconsider g as FinSequence of NAT by FINSEQ_1:def 4; take g; thus len g = len f by A1; let i be set; assume i in dom g; hence thesis by A2; end; uniqueness proof let g,h be FinSequence of NAT such that A5: len g = len f and A6: for i being set st i in dom g holds g.i = p |-count f.i and A7: len h = len f and A8: for i being set st i in dom h holds h.i = p |-count f.i; A9: dom g = Seg len g & dom h = Seg len h by FINSEQ_1:def 3; for k being Nat st k in dom g holds g.k = h.k proof let k be Nat; assume A10: k in dom g; hence g.k = p |-count f.k by A6 .= h.k by A5,A7,A8,A9,A10; end; hence thesis by A5,A7,A9,FINSEQ_1:13; end; end; theorem Th49: for p being Prime, f being FinSequence of NAT st f={} holds p |-count f = {} proof let p be Prime; let f be FinSequence of NAT; assume f={}; then len (p |-count f) = len {} by Def1; hence thesis; end; theorem Th50: for p being Prime, f1,f2 being FinSequence of NAT holds p |-count (f1^f2) = (p |-count f1)^(p |-count f2) proof let p be Prime; let f1,f2 be FinSequence of NAT; A1: len (p |-count f2) = len f2 by Def1; A2: dom (p |-count (f1^f2)) = Seg len (p |-count (f1^f2)) by FINSEQ_1:def 3 .= Seg len (f1^f2) by Def1; A3: for k being Nat st k in dom (p |-count (f1^f2)) holds (p |-count (f1^f2) ).k = ((p |-count f1)^(p |-count f2)).k proof let k be Nat; assume A4: k in dom (p |-count (f1^f2)); then A5: k in dom (f1^f2) by A2,FINSEQ_1:def 3; per cases by A5,FINSEQ_1:25; suppose A6: k in dom f1; A7: dom f1 = Seg len f1 by FINSEQ_1:def 3 .= Seg len (p |-count f1) by Def1 .= dom (p |-count f1) by FINSEQ_1:def 3; (p |-count (f1^f2)).k = p |-count (f1^f2).k by A4,Def1 .= p |-count (f1.k) by A6,FINSEQ_1:def 7 .= (p |-count f1).k by A6,A7,Def1; hence thesis by A6,A7,FINSEQ_1:def 7; end; suppose A8: ex n being Nat st n in dom f2 & k=len f1 + n; A9: dom f2 = Seg len f2 by FINSEQ_1:def 3 .= Seg len (p |-count f2) by Def1 .= dom (p |-count f2) by FINSEQ_1:def 3; consider n be Nat such that A10: n in dom f2 and A11: k=len f1 + n by A8; A12: ((p |-count f1)^(p |-count f2)).k = ((p |-count f1)^(p |-count f2)) .(len (p |-count f1) + n) by A11,Def1 .= (p |-count f2).n by A10,A9,FINSEQ_1:def 7; (f1^f2).k = f2.n by A10,A11,FINSEQ_1:def 7; then (p |-count (f1^f2)).k = p |-count (f2.n) by A4,Def1 .= (p |-count f2).n by A10,A9,Def1; hence thesis by A12; end; end; Seg len (f1^f2) = Seg (len f1 + len f2) by FINSEQ_1:22 .= Seg (len (p |-count f1) + len (p |-count f2)) by A1,Def1 .= Seg len ((p |-count f1)^(p |-count f2)) by FINSEQ_1:22 .= dom ((p |-count f1)^(p |-count f2)) by FINSEQ_1:def 3; hence thesis by A2,A3,FINSEQ_1:13; end; theorem Th51: for p being Prime, n being non zero Element of NAT holds p |-count <*n*> = <* (p |-count n) *> proof let p be Prime; let n be non zero Element of NAT; A1: dom (p |-count <*n*>) = Seg len (p |-count <*n*>) by FINSEQ_1:def 3 .= Seg len <*n*> by Def1 .= Seg 1 by FINSEQ_1:39; A2: for k being Nat st k in dom (p |-count <*n*>) holds (p |-count <*n*>).k = <* p |-count n *>.k proof let k be Nat; assume A3: k in dom (p |-count <*n*>); then 1<=k & k<=1 by A1,FINSEQ_1:1; then A4: k=1 by XXREAL_0:1; (p |-count <*n*>).k = p |-count <*n*>.k by A3,Def1; then (p |-count <*n*>).k = p |-count n by A4,FINSEQ_1:40; hence thesis by A4,FINSEQ_1:40; end; Seg 1 = Seg len <* p |-count n *> by FINSEQ_1:39; then dom (p |-count <*n*>) = dom <* (p |-count n) *> by A1,FINSEQ_1:def 3; hence thesis by A2,FINSEQ_1:13; end; theorem Th52: for f being FinSequence of NAT, p being Prime st Product f <> 0 holds p |-count (Product f) = Sum (p |-count f) proof let f be FinSequence of NAT; defpred P[Nat] means for f being FinSequence of NAT, p being Prime st $1=len f & Product f <> 0 holds p |-count (Product f) = Sum (p |-count f); let p be Prime; assume A1: Product f<>0; A2: ex n being Element of NAT st n=len f; A3: for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume A4: P[n]; for f being FinSequence of NAT, p being Prime st n+1=len f & Product f <> 0 holds p |-count (Product f) = Sum (p |-count f) proof let f be FinSequence of NAT; let p be Prime; assume that A5: n+1=len f and A6: Product f <> 0; consider g being FinSequence of NAT, d being Element of NAT such that A7: f = g^<*d*> by A5,FINSEQ_2:19; len f = len g + len <*d*> by A7,FINSEQ_1:22; then A8: n+1 = len g + 1 by A5,FINSEQ_1:39; A9: (Product g) * d <> 0 by A6,A7,RVSUM_1:96; then A10: Product g <> 0; A11: d <> 0 by A9; p |-count (Product f) = p |-count ((Product g) * d) by A7,RVSUM_1:96 .= (p |-count (Product g)) + (p |-count d) by A10,A11,NAT_3:28 .= Sum (p |-count g) + (p |-count d) by A4,A10,A8 .= Sum ((p |-count g)^<*(p |-count d)*>) by RVSUM_1:74 .= Sum ((p |-count g)^(p |-count <*d*>)) by A11,Th51 .= Sum (p |-count (g^<*d*>)) by Th50; hence thesis by A7; end; hence thesis; end; A12: P[0] proof let f be FinSequence of NAT; let p be Prime; assume that A13: 0=len f and Product f<>0; A14: p<>1 by INT_2:def 4; A15: f={} by A13; then Sum (p |-count f) = 0 by Th49,RVSUM_1:72; hence thesis by A15,A14,NAT_3:21,RVSUM_1:94; end; for n being Nat holds P[n] from NAT_1:sch 2(A12,A3); hence thesis by A1,A2; end; theorem Th53: for f1,f2 being FinSequence of REAL st len f1 = len f2 & (for k being Element of NAT st k in dom f1 holds f1.k<=f2.k & f1.k>0) holds Product f1 <= Product f2 proof let f1,f2 be FinSequence of REAL; defpred P[Nat] means for f1,f2 being FinSequence of REAL st len f1 = len f2 & $1 = len f1 & (for k being Element of NAT st k in dom f1 holds f1 .k<=f2.k & f1.k>0) holds Product f1 <= Product f2; assume A1: len f1 = len f2; A2: for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume A3: P[n]; for f1,f2 being FinSequence of REAL st len f1 = len f2 & n+1 = len f1 & (for k being Element of NAT st k in dom f1 holds f1.k<=f2.k & f1.k>0) holds Product f1 <= Product f2 proof let f1,f2 be FinSequence of REAL; assume that A4: len f1=len f2 and A5: n+1=len f1; consider g2 be FinSequence of REAL, r2 be Element of REAL such that A6: f2 = g2^<*r2*> by A4,A5,FINSEQ_2:19; len f2 = len g2 + len <* r2 *> by A6,FINSEQ_1:22; then A7: n+1 = len g2 + 1 by A4,A5,FINSEQ_1:39; A8: Product f2 = (Product g2) * r2 by A6,RVSUM_1:96; consider g1 be FinSequence of REAL, r1 be Element of REAL such that A9: f1 = g1^<*r1*> by A5,FINSEQ_2:19; set k1 = len g1+1; A10: Product f1 = (Product g1) * r1 by A9,RVSUM_1:96; len f1 = len g1 + len <* r1 *> by A9,FINSEQ_1:22; then A11: n+1 = len g1 + 1 by A5,FINSEQ_1:39; assume A12: for k being Element of NAT st k in dom f1 holds f1.k<=f2.k & f1. k>0; A13: now let k be Element of NAT; A14: dom g1 c= dom f1 by A9,FINSEQ_1:26; assume A15: k in dom g1; then k in Seg len g2 by A11,A7,FINSEQ_1:def 3; then k in dom g2 by FINSEQ_1:def 3; then A16: f2.k=g2.k by A6,FINSEQ_1:def 7; f1.k=g1.k by A9,A15,FINSEQ_1:def 7; hence g1.k<=g2.k & g1.k>0 by A12,A15,A16,A14; end; then A17: for k being Element of NAT st k in dom g1 holds g1.k > 0; Product g1 <= Product g2 by A3,A11,A7,A13; then A18: Product g2 > 0 by A17,Th41; n+1>=0+1 by XREAL_1:6; then k1 in Seg (n+1) by A11,FINSEQ_1:1; then A19: k1 in dom f1 by A5,FINSEQ_1:def 3; then f1.k1<=f2.k1 by A12; then r1 <= f2.k1 by A9,FINSEQ_1:42; then r1 <= r2 by A6,A11,A7,FINSEQ_1:42; then A20: r1 * (Product g2) <= r2 * (Product g2) by A18,XREAL_1:64; f1.k1>0 by A12,A19; then r1>0 by A9,FINSEQ_1:42; then (Product g1) * r1 <= (Product g2) * r1 by A3,A11,A7,A13,XREAL_1:64; hence thesis by A10,A8,A20,XXREAL_0:2; end; hence thesis; end; A21: P[0] proof let f1,f2 be FinSequence of REAL; assume len f1 = len f2 & 0=len f1; then f1={} & f2 = {}; hence thesis; end; A22: for n being Nat holds P[n] from NAT_1:sch 2(A21,A2); assume for k being Element of NAT st k in dom f1 holds f1.k<=f2.k & f1.k>0; hence thesis by A22,A1; end; theorem Th54: for n being Element of NAT, r being Real st r>0 holds Product (n |-> r) = r to_power n proof defpred P[Nat] means for r being Real st r>0 holds Product ($1 |-> r) = r to_power $1; A1: for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume A2: P[n]; now let r be Real; assume A3: r>0; Product ((n+1)|-> r) = Product ((n |-> r) ^ <*r*>) by FINSEQ_2:60 .= Product (n |-> r) * r by RVSUM_1:96 .= (r to_power n) * r by A2,A3 .= (r to_power n) * (r to_power 1) by POWER:25; hence Product ((n+1)|-> r) = r to_power (n+1) by A3,POWER:27; end; hence thesis; end; A4: P[0] by POWER:24,RVSUM_1:94; for n being Nat holds P[n] from NAT_1:sch 2(A4,A1); hence thesis; end; scheme scheme1 { P[set,set,set] } : for p being Prime, n being Element of NAT, m being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]} holds Product Sgm X > 0 proof let p be Prime; let n be Element of NAT; let m be non zero Element of NAT; let X be set; set f = Sgm X; assume A1: X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]}; A2: for k being Element of NAT st k in dom f holds f.k > 0 proof set XX=Seg m; let k be Element of NAT; now let x be object; assume x in X; then ex y9 being prime Element of NAT st y9|^(y9 |-count m) = x & P[n,m, y9] by A1; then ex b being Element of NAT st b=x & 1<=b & b<=m by Th16; hence x in XX by FINSEQ_1:1; end; then X c= Seg m; then A3: rng f = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m, p9]} by A1,FINSEQ_1:def 13; assume k in dom f; then f.k in {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9 ]} by A3,FUNCT_1:3; then ex y9 being prime Element of NAT st y9|^(y9 |-count m) = f.k & P[n,m, y9]; hence thesis; end; rng f c= REAL; then f is FinSequence of REAL by FINSEQ_1:def 4; hence thesis by A2,Th41; end; scheme scheme2 { P[set,set,set] } : for p being Prime, n being Element of NAT, m being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]} & not p|^(p |-count m) in X holds p |-count (Product Sgm X) = 0 proof let p be Prime; let n be Element of NAT; let m be non zero Element of NAT; let X be set; assume A1: X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]}; set f=p |-count (Sgm X); set g=(len f) |-> 0; assume A2: not p|^(p |-count m) in X; A3: for k being Nat st 1 <=k & k <= len f holds f.k=g.k proof set XX=Seg m; let k be Nat; assume A4: 1 <=k; assume k <= len f; then A5: k in Seg len f by A4,FINSEQ_1:1; then k in dom f by FINSEQ_1:def 3; then A6: f.k = p |-count (Sgm X).k by Def1; now let x be object; assume x in X; then ex y9 being prime Element of NAT st y9|^(y9 |-count m) = x & P[n,m, y9] by A1; then ex b being Element of NAT st b=x & 1<=b & b<=m by Th16; hence x in XX by FINSEQ_1:1; end; then X c= Seg m; then A7: rng Sgm X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n ,m,p9]} by A1,FINSEQ_1:def 13; len f = len (Sgm X) by Def1; then k in dom Sgm X by A5,FINSEQ_1:def 3; then (Sgm X).k in {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[ n,m,p9]} by A7,FUNCT_1:3; then consider p1 be prime Element of NAT such that A8: p1|^(p1 |-count m) = (Sgm X).k and A9: P[n,m,p1]; p1<>p by A1,A2,A9; then p<>1 & not p divides p1|^(p1 |-count m) by INT_2:def 4,NAT_3:6; then f.k = 0 by A6,A8,NAT_3:27; hence thesis; end; for p being Prime, n being Element of NAT, m being non zero Element of NAT , X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]} holds Product Sgm X > 0 from scheme1; then Product Sgm X <> 0 by A1; then A10: p |-count (Product Sgm X) = Sum (p |-count (Sgm X)) by Th52; len f = len g & Sum g = (len f)*0 by CARD_1:def 7,RVSUM_1:80; hence thesis by A10,A3,FINSEQ_1:14; end; scheme scheme3 { P[set,set,set] } : for p being Prime, n being Element of NAT, m being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]} & p|^(p |-count m) in X holds p |-count ( Product Sgm X) = p |-count m proof let p be Prime; let n be Element of NAT; let m be non zero Element of NAT; let X be set; set XX=Seg m; defpred P1[Element of NAT,Element of NAT,Prime] means P[$1,$2,$3] & $3|^($3 |-count $2) <= p|^(p |-count $2); defpred P2[Element of NAT,Element of NAT,Prime] means P[$1,$2,$3] & $3|^($3 |-count $2) > p|^(p |-count $2); set X1 = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P1[n,m,p9]}; set X2 = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P2[n,m,p9]}; A1: now let k1,k2 be Nat; assume k1 in X1 & k2 in X2; then ( ex p1 being prime Element of NAT st p1|^(p1 |-count m)=k1 & P1[n, m ,p1])& ex p2 being prime Element of NAT st p2|^(p2 |-count m)=k2 & P2[n,m,p2]; hence k1 < k2 by XXREAL_0:2; end; A2: now assume p|^(p |-count m) in X2; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p |-count m) & P2[n,m,p9]; hence contradiction; end; set m1=p|^(p |-count m); defpred P12[Element of NAT,Element of NAT,Prime] means P[$1,$2,$3] & $3|^($3 |-count $2) = p|^(p |-count $2); defpred P11[Element of NAT,Element of NAT,Prime] means P[$1,$2,$3] & $3|^($3 |-count $2) < p|^(p |-count $2); set X11 = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P11[n,m,p9]}; set X12 = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P12[n,m,p9]}; A3: now let k1,k2 be Nat; assume k1 in X11 & k2 in X12; then ( ex p1 being prime Element of NAT st p1|^(p1 |-count m)=k1 & P11[n,m ,p1])& ex p2 being prime Element of NAT st p2|^(p2 |-count m)=k2 & P12[n,m,p2]; hence k1 < k2; end; now let x be object; assume x in X1; then consider p9 being prime Element of NAT such that A4: p9|^(p9 |-count m)=x & P1[n,m,p9]; p9|^(p9 |-count m)=x & P11[n,m,p9] or p9|^(p9 |-count m)=x & P12[n,m, p9] by A4,XXREAL_0:1; then x in X11 or x in X12; hence x in X11 \/ X12 by XBOOLE_0:def 3; end; then A5: X1 c= X11 \/ X12; assume A6: X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]}; now let x be object; assume x in X; then ex y9 being prime Element of NAT st y9|^(y9 |-count m) = x & P[n,m,y9 ] by A6; then ex b being Element of NAT st b=x & 1<=b & b<=m by Th16; hence x in XX by FINSEQ_1:1; end; then A7: X c= Seg m; now let x be object; assume x in X12; then ex p9 be prime Element of NAT st p9|^(p9 |-count m) = x & P12[n,m,p9]; hence x in {p|^(p |-count m)} by TARSKI:def 1; end; then A8: X12 c= {p|^(p |-count m)}; for p being Prime, n being Element of NAT, m being non zero Element of NAT , X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]} holds Product Sgm X > 0 from scheme1; then A9: Product Sgm X <> 0 by A6; A10: 1 < p by INT_2:def 4; A11: p |-count (p|^(p |-count m)) = (p |-count m) * (p |-count p) by NAT_3:32 .= (p |-count m) * 1 by A10,NAT_3:22; now let x be object; assume x in X1; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=x & P1[n,m,p9]; hence x in X by A6; end; then A12: X1 c= X; then A13: X1 c= Seg m by A7; now let x be object; assume x in X12; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=x & P12[n,m,p9 ]; hence x in X1; end; then A14: X12 c= X1; then A15: X12 c= Seg m by A13; now let x be object; assume x in X11; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=x & P11[n,m,p9 ]; hence x in X1; end; then A16: X11 c= X1; then A17: X11 c= Seg m by A13; X11 \/ X12 c= X1 \/ X1 by A16,A14,XBOOLE_1:13; then A18: Sum (p |-count (Sgm X1)) = Sum (p |-count (Sgm (X11 \/ X12))) by A5, XBOOLE_0:def 10 .= Sum (p |-count (Sgm(X11) ^ Sgm(X12))) by A17,A15,A3,FINSEQ_3:42 .= Sum ((p |-count Sgm(X11)) ^ (p |-count Sgm(X12))) by Th50 .= Sum (p |-count Sgm(X11)) + Sum (p |-count Sgm(X12)) by RVSUM_1:75; for p being Prime, n being Element of NAT, m being non zero Element of NAT , X2 being set st X2 = {p9|^(p9 |-count m) where p9 is prime Element of NAT : P2[n,m,p9]} & not p|^(p |-count m) in X2 holds p |-count (Product Sgm X2) = 0 from scheme2; then A19: p |-count (Product Sgm X2) = 0 by A2; for p being Prime, n being Element of NAT, m being non zero Element of NAT , X2 being set st X2 = {p9|^(p9 |-count m) where p9 is prime Element of NAT : P2[n,m,p9]} holds Product Sgm X2 > 0 from scheme1; then A20: Product Sgm(X2) <> 0; now let x be object; assume x in X; then consider p9 being prime Element of NAT such that A21: p9|^(p9 |-count m)=x & P[n,m,p9] by A6; p9|^(p9 |-count m)=x & P1[n,m,p9] or p9|^(p9 |-count m)=x & P2[n,m,p9 ] by A21; then x in X1 or x in X2; hence x in X1 \/ X2 by XBOOLE_0:def 3; end; then A22: X c= X1 \/ X2; now let x be object; assume x in X2; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=x & P2[n,m,p9]; hence x in X by A6; end; then A23: X2 c= X; then A24: X2 c= Seg m by A7; reconsider m1 as non zero Element of NAT by ORDINAL1:def 12; A25: now assume p|^(p |-count m) in X11; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p |-count m) & P11[n,m,p9]; hence contradiction; end; assume p|^(p |-count m) in X; then p|^(p |-count m) in X1 by A22,A2,XBOOLE_0:def 3; then p|^(p |-count m) in X12 by A5,A25,XBOOLE_0:def 3; then for x being object st x in {p|^(p |-count m)} holds x in X12 by TARSKI:def 1; then A26: {p|^(p |-count m)} c= X12; for p being Prime, n being Element of NAT, m being non zero Element of NAT , X11 being set st X11 = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P11[n,m,p9]} & not p|^(p |-count m) in X11 holds p |-count (Product Sgm X11) = 0 from scheme2; then A27: p |-count (Product Sgm X11) = 0 by A25; for p being Prime, n being Element of NAT, m being non zero Element of NAT , X11 being set st X11 = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P11[n,m,p9]} holds Product Sgm X11 > 0 from scheme1; then A28: Product Sgm(X11) <> 0; X1 \/ X2 c= X \/ X by A12,A23,XBOOLE_1:13; then Sum (p |-count (Sgm X)) = Sum (p |-count (Sgm (X1 \/ X2))) by A22, XBOOLE_0:def 10 .= Sum (p |-count (Sgm(X1) ^ Sgm(X2))) by A13,A24,A1,FINSEQ_3:42 .= Sum ((p |-count Sgm(X1)) ^ (p |-count Sgm(X2))) by Th50 .= Sum (p |-count Sgm(X1)) + Sum (p |-count Sgm(X2)) by RVSUM_1:75; then p |-count (Product Sgm X) = Sum (p |-count Sgm(X1)) + Sum (p |-count Sgm(X2)) by A9,Th52 .= Sum (p |-count Sgm(X1)) + 0 by A20,A19,Th52 .= 0 + Sum (p |-count Sgm(X12)) by A18,A28,A27,Th52 .= Sum (p |-count Sgm({p|^(p |-count m)})) by A26,A8,XBOOLE_0:def 10 .= Sum (p |-count <* m1 *>) by FINSEQ_3:44 .= Sum <* p |-count m1 *> by Th51 .= p |-count m1 by RVSUM_1:73; hence thesis by A11; end; Lm10: for n, m being Element of NAT st m = 2*n choose n & n>=3 holds m = Product Sgm {p|^(p |-count m) where p is prime Element of NAT: p<=sqrt(2*n) & p |-count m>0} * Product Sgm {p|^(p |-count m) where p is prime Element of NAT: sqrt(2*n)

0} * Product Sgm {p|^(p |-count m) where p is prime Element of NAT: n

0}
proof
defpred P3[Element of NAT,Element of NAT,Prime] means $1<$3 & $3<=2*$1 & $3
|-count $2>0;
defpred P2[Element of NAT,Element of NAT,Prime] means sqrt(2*$1)<$3 & $3<=2*
$1/3 & $3 |-count $2>0;
defpred P1[Element of NAT,Element of NAT,Prime] means $3<=sqrt(2*$1) & $3
|-count $2>0;
let n, m be Element of NAT;
assume
A1: m = 2*n choose n;
set X3 = {p|^(p |-count m) where p is prime Element of NAT: P3[n,m,p]};
set X2 = {p|^(p |-count m) where p is prime Element of NAT: P2[n,m,p]};
set X1 = {p|^(p |-count m) where p is prime Element of NAT: P1[n,m,p]};
set f1 = Sgm X1;
set f2 = Sgm X2;
set f3 = Sgm X3;
set n1=Product f1;
set n2=Product f2;
set n3=Product f3;
A2: for p being Prime, n being Element of NAT, m being non zero Element of
NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT:
P2[n,m,p9]} & not p|^(p |-count m) in X holds p |-count (Product Sgm X) = 0
from scheme2;
set k = Product f1 * Product f2 * Product f3;
A3: for p being Prime, n being Element of NAT, m being non zero Element of
NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT:
P1[n,m,p9]} holds Product Sgm X > 0 from scheme1;
assume
A4: n >= 3;
A5: now
2*n<3*n by A4,XREAL_1:68;
then
A6: 2*n/3<3*n/3 by XREAL_1:74;
assume n<2*n/3;
hence contradiction by A6;
end;
A7: now
sqrt 2 < sqrt 3 & sqrt 3 <= sqrt n by A4,SQUARE_1:26,27;
then
A8: sqrt 2 < sqrt n by XXREAL_0:2;
sqrt n > 0 by A4,SQUARE_1:25;
then (sqrt 2)*(sqrt n) < (sqrt n)*(sqrt n) by A8,XREAL_1:68;
then sqrt(2*n) < (sqrt n)*(sqrt n) by SQUARE_1:29;
then
A9: sqrt(2*n) < sqrt(n^2) by SQUARE_1:29;
assume n

0; then p|^(p |-count m) in X2 by A26,A27,A28; hence thesis by A10,A24; end; suppose A29: p |-count m = 0; now assume p|^(p |-count m) in X2; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p |-count m)& P2[n,m,p9]; hence contradiction by A10,A29,Th22; end; hence thesis by A10,A2,A29; end; end; A30: for p being Prime, n being Element of NAT, m being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P3[n,m,p9]} & p|^(p |-count m) in X holds p |-count (Product Sgm X) = p |-count m from scheme3; A31: for p being Prime st n

0; then p|^(p |-count m) in X3 by A32,A33,A34; hence thesis by A10,A30; end; suppose A35: p |-count m = 0; now assume p|^(p |-count m) in X3; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p |-count m)& P3[n,m,p9]; hence contradiction by A10,A35,Th22; end; hence thesis by A10,A15,A35; end; end; A36: for p being Prime, n being Element of NAT, m being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P1[n,m,p9]} & p|^(p |-count m) in X holds p |-count (Product Sgm X) = p |-count m from scheme3; A37: for p being Prime st p<=sqrt(2*n) holds p |-count n2 = 0 & p |-count n3 = 0 & p |-count n1 = p |-count m proof let p be Prime; A38: p in NAT by ORDINAL1:def 12; assume A39: p<=sqrt(2*n); now assume p|^(p |-count m) in X2; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p |-count m) & P2[n,m,p9]; hence contradiction by A10,A39,Th22; end; hence p |-count n2 = 0 by A10,A2; now assume p|^(p |-count m) in X3; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p |-count m) & P3[n,m,p9]; then n

0; then p|^(p |-count m) in X1 by A39,A38; hence thesis by A10,A36; end; suppose A40: p |-count m = 0; now assume p|^(p |-count m) in X1; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p |-count m)& P1[n,m,p9]; hence contradiction by A10,A40,Th22; end; hence thesis by A10,A16,A40; end; end; A41: for p being Element of NAT st p is prime holds p |-count m = p |-count k proof reconsider n3 as non zero Element of NAT by A10,A11; reconsider n2 as non zero Element of NAT by A10,A13; reconsider n1 as non zero Element of NAT by A10,A3; let p be Element of NAT; assume A42: p is prime; then A43: p |-count k = (p |-count (n1*n2)) + (p |-count n3) by NAT_3:28 .= (p |-count n1)+(p |-count n2)+(p |-count n3) by A42,NAT_3:28; per cases; suppose A44: p>2*n; then A45: p |-count n2 = 0 by A17,A42; p |-count m = 0 & p |-count n1 = 0 by A1,A4,A17,A42,A44,Lm9; hence thesis by A17,A42,A43,A44,A45; end; suppose A46: n

0 by A10,A3; hence thesis by A10,A14,A12,A41,Th21; end; scheme scheme4 { A(set,set) -> set, P[set,set] } : for n,m being Element of NAT, r being Real, X being finite set st X = {A(p,m) where p is prime Element of NAT: p <= r & P[p,m]} & r>=0 holds card X <= [\ r /] proof let n,m be Element of NAT; defpred P1[Nat] means for n,m being Element of NAT, r being Real, X being finite set st X = {A(p,m) where p is prime Element of NAT: p <= r & P[p ,m]} & r>=0 & $1 = [\ r /] holds card X <= [\ r /]; A1: for n being Nat st P1[n] holds P1[n+1] proof let n be Nat; assume A2: P1[n]; now let m be Element of NAT; let r be Real; let X be finite set; set r1 = r - 1; set X1 = {A(p,m) where p is prime Element of NAT: p <= r1 & P[p,m]}; set X2 = {A(p,m) where p is prime Element of NAT: r1 < p & p <= r & P[p, m]}; A3: 0+n <= 1+n by XREAL_1:6; assume A4: X = {A(p,m) where p is prime Element of NAT: p <= r & P[p,m]}; now let x be object; assume A5: x in X1 \/ X2; per cases by A5,XBOOLE_0:def 3; suppose x in X1; then consider p being prime Element of NAT such that A6: A(p,m)=x and A7: p<=r1 and A8: P[p,m]; -1+r<=0+r by XREAL_1:6; then p<=r by A7,XXREAL_0:2; hence x in X by A4,A6,A8; end; suppose x in X2; then ex p being prime Element of NAT st A(p,m)=x & r1 < p & p<=r & P [p,m]; hence x in X by A4; end; end; then A9: X1 \/ X2 c= X; assume r >= 0; now let x be object; assume x in X; then consider p being prime Element of NAT such that A10: A(p,m)=x & p<=r & P[p,m] by A4; A(p,m)=x & p<=r1 & P[p,m] or A(p,m)=x & r1

=0 by INT_1:def 6;
then
A15: card X1 <= [\ r1 /] by A2,A13;
per cases;
suppose
not ex x being object st x in X2;
then X2={} by XBOOLE_0:def 1;
hence card X <= [\ r /] by A12,A13,A11,A15,A3,XXREAL_0:2;
end;
suppose
A16: ex x being set st x in X2;
then consider x be set such that
A17: x in X2;
A18: now
assume X2<>{x};
then consider y be object such that
A19: y in X2 and
A20: y<>x by A16,ZFMISC_1:35;
consider p1 be prime Element of NAT such that
A21: A(p1,m)=x and
A22: r1

=1; per cases; suppose n<4000; then n<4001 by XXREAL_0:2; hence thesis by A1,Lm7; end; suppose A2: n>=4000; set m = 2*n choose n; set X1={p|^(p |-count m) where p is prime Element of NAT: p<=sqrt(2*n) & p |-count m>0}; set X2={p|^(p |-count m) where p is prime Element of NAT: sqrt(2*n)

0}; set X3={p|^(p |-count m) where p is prime Element of NAT: n

0}; assume A3: not ex p being Prime st n

{}; then consider x be object such that A4: x in X3 by XBOOLE_0:def 1; ex p be prime Element of NAT st p|^(p |-count m)=x & n

0 by A4; hence contradiction by A3; end; then A5: m = (Product Sgm X1)*(Product Sgm X2)*1 by A2,Lm10,FINSEQ_3:43,RVSUM_1:94 ,XXREAL_0:2; A6: 4|^n / (2*n) <= m by Th6; set X = {p where p is prime Element of NAT: p<=2*n/3}; A7: n>=3 by A2,XXREAL_0:2; then n/3>=3/3 by XREAL_1:72; then (n/3)*2>=1*2 by XREAL_1:64; then A8: Product Sgm X <= (4 to_power ((2*n/3)-1)) by Th45; set mm=[/ 2*n/3 \]; reconsider mm as Element of NAT by INT_1:53; set XX=Seg mm; A9: now assume {} in X; then ex p being prime Element of NAT st p = {} & p<=2*n/3; hence contradiction; end; -1+(2*n/3)<0+(2*n/3) by XREAL_1:6; then A10: 4 to_power ((2*n/3)-1) < 4 to_power (2*n/3) by POWER:39; now let x be object; assume x in X2; then consider p be prime Element of NAT such that A11: p|^(p |-count m)=x and A12: sqrt(2*n)

0; p |-count m <= 1 by A7,A12,A13,Lm9; then p |-count m < 1+1 by NAT_1:13; then p |-count m = 1 by A14,NAT_1:23; then p=x by A11; hence x in X by A13; end; then A15: X2 c= X; now let x be object; assume x in X; then consider p being prime Element of NAT such that A16: p = x and A17: p<=2*n/3; A18: 1<=p by INT_2:def 4; 2*n/3<=[/ 2*n/3 \] by INT_1:def 7; then p<=[/ 2*n/3 \] by A17,XXREAL_0:2; hence x in XX by A16,A18,FINSEQ_1:1; end; then A19: X c= Seg mm; then X c= NAT by XBOOLE_1:1; then Product Sgm X2 <= Product Sgm X by A19,A9,A15,Th42; then A20: Product Sgm X2 <= (4 to_power ((2*n/3)-1)) by A8,XXREAL_0:2; n>=3 by A2,XXREAL_0:2; then Product Sgm X1 <= (2*n) to_power sqrt(2*n) by Lm11; then m <= ((2*n) to_power sqrt(2*n))*(4 to_power ((2*n/3)-1)) by A20,A5, XREAL_1:66; then A21: 4|^n / (2*n) <= ((2*n) to_power sqrt(2*n))*(4 to_power ((2*n/3)-1 )) by A6,XXREAL_0:2; A22: 4 to_power (2*n/3)>0 by POWER:34; (2*n) to_power sqrt(2*n)>0 by A2,POWER:34; then (4 to_power ((2*n/3)-1))*((2*n) to_power sqrt(2*n)) < (4 to_power (2* n/3))*((2*n) to_power sqrt(2*n)) by A10,XREAL_1:68; then 4|^n / (2*n) <= ((2*n) to_power sqrt(2*n))*(4 to_power (2*n/3)) by A21 ,XXREAL_0:2; then 4|^n/(2*n)*(2*n)<=((2*n) to_power sqrt(2*n))*(4 to_power (2*n/3))*(2* n) by XREAL_1:64; then 4|^n = 4 to_power (3*n/3) & 4|^n<=((2*n) to_power sqrt(2*n))*(2*n)*(4 to_power (2*n/3)) by A2,POWER:41,XCMPLX_1:87; then (4 to_power (3*n/3))/(4 to_power (2*n/3)) <= (((2*n) to_power sqrt(2* n))*(2*n))* (4 to_power (2*n/3))/(4 to_power (2*n/3)) by A22,XREAL_1:72; then (4 to_power (3*n/3))/(4 to_power (2*n/3)) <= ((2*n) to_power sqrt(2*n ))*(2*n) by A22,XCMPLX_1:89; then 4 to_power ((3*n/3)-(2*n/3)) <= ((2*n) to_power sqrt(2*n))*(2*n) by POWER:29; then 4 to_power (n/3) <= ((2*n) to_power sqrt(2*n))*((2*n) to_power 1) by POWER:25; then 4 to_power (n/3) <= (2*n) to_power (sqrt(2*n)+1) by A2,POWER:27; then A23: 4 to_power (n/3) < (2*n) to_power (sqrt(2*n)+1) or 4 to_power (n/3) = (2*n) to_power (sqrt(2*n)+1) by XXREAL_0:1; 4 to_power (n/3)>0 by POWER:34; then (4 to_power (n/3)) to_power 3 <= ((2*n) to_power (sqrt(2*n)+1)) to_power 3 by A23,POWER:37; then 4 to_power ((n/3)*3) <= ((2*n) to_power (sqrt(2*n)+1)) to_power 3 by POWER:33; then A24: 4 to_power n <= (2*n) to_power ((sqrt(2*n)+1)*3) by A2,POWER:33; reconsider 2n=2*n as Real; A25: 6-root(2*n) to_power 6 = 6-root(2n) |^ 6 by POWER:41 .= 2n by COMPTRIG:4; 2 to_power 2 = 2|^2 by POWER:41 .= Product <* 2, 2 *> by FINSEQ_2:61 .= 2*2 by RVSUM_1:99; then A26: 2 to_power (2*n)>0 & 4 to_power n = 2 to_power (2*n) by POWER:33,34; set n1=[\ 6-root(2*n) /]; 6-root(2*n) -1 < n1 by INT_1:def 6; then A27: 6-root(2*n) -1 +1 < n1 +1 by XREAL_1:6; 6-root(2*n) > 6-root 0 by A2,POWER:17; then A28: 6-root(2*n) > 0 by POWER:5; then reconsider n1 as Element of NAT by INT_1:53; n1 <= 6-root(2*n) by INT_1:def 6; then n1 < 6-root(2*n) or n1 = 6-root(2*n) by XXREAL_0:1; then A29: 2 to_power n1 <= 2 to_power (6-root(2*n)) by POWER:39; n1+1 <= 2|^n1 by NEWTON:85; then n1+1 <= 2 to_power n1 by POWER:41; then n1+1 <= 2 to_power (6-root(2*n)) by A29,XXREAL_0:2; then n1+1 < 2 to_power (6-root(2*n)) or n1+1 = 2 to_power (6-root(2*n)) by XXREAL_0:1; then A30: (n1+1) to_power 6 <= (2 to_power (6-root(2*n))) to_power 6 by POWER:37; 6-root(2*n) to_power 6 < (n1+1) to_power 6 by A27,A28,POWER:37; then 2*n < (2 to_power (6-root(2*n))) to_power 6 by A30,A25,XXREAL_0:2; then A31: 2*n < 2 to_power ((6-root(2*n))*6) by POWER:33; sqrt(2*n)>0 by A2,SQUARE_1:25; then (2*n) to_power ((sqrt(2*n)+1)*3) < (2 to_power ((6-root(2*n))*6)) to_power ((sqrt(2*n)+1)*3) by A2,A31,POWER:37; then 4 to_power n < (2 to_power ((6-root(2*n))*6)) to_power ((sqrt(2*n)+1) *3) by A24,XXREAL_0:2; then 4 to_power n < 2 to_power (((6-root(2*n))*6)*((sqrt(2*n)+1)*3)) by POWER:33; then log(2,2 to_power (2*n)) < log(2,2 to_power (((6-root(2*n))*6)*((sqrt( 2*n)+1)*3))) by A26,POWER:57; then (2*n)*log(2,2) < log(2,2 to_power (((6-root(2*n))*6)*((sqrt(2*n)+1)*3 ))) by POWER:55; then (2*n)*log(2,2) < (((6-root(2*n))*6)*((sqrt(2*n)+1)*3))*log(2,2) by POWER:55; then (2*n)*1 < (((6-root(2*n))*6)*((sqrt(2*n)+1)*3))*log(2,2) by POWER:52; then A32: 2*n < (((6-root(2*n))*6)*((sqrt(2*n)+1)*3))*1 by POWER:52; 42 < n by A2,XXREAL_0:2; then 42*2 < n*2 by XREAL_1:68; then 81 < 2*n by XXREAL_0:2; then A33: sqrt(81) < sqrt(2*n) by SQUARE_1:27; 81=9^2; then sqrt 81 = 9 by SQUARE_1:22; then 9*2 < sqrt(2*n)*2 by A33,XREAL_1:68; then 18 + 18*sqrt(2*n) < 2*sqrt(2*n)+18*sqrt(2*n) by XREAL_1:6; then (18 + 18*sqrt(2*n))*(6-root(2*n)) < 20*sqrt(2*n)*(6-root(2*n)) by A28, XREAL_1:68; then 2*n < 20*(sqrt(2*n)*(6-root(2*n))) by A32,XXREAL_0:2; then 2*n < 20*((2-Root(2*n))*(6-root(2*n))) by PREPOWER:32; then 2*n < 20*((2-root(2*n))*(6-root(2*n))) by POWER:def 1; then 2*n < 20*(((2*n) to_power (1/2))*(6-root(2*n))) by POWER:45; then 2*n < 20*(((2*n) to_power (1/2))*((2*n) to_power (1/6))) by POWER:45; then A34: 2*n < 20*((2*n) to_power (1/2+1/6)) by A2,POWER:27; A35: (2*n) to_power (2/3)<>0 by A2,POWER:34; (2*n) to_power (2/3)>0 by A2,POWER:34; then (2*n)/((2*n) to_power (2/3)) < 20*((2*n) to_power (2/3))/((2*n) to_power (2/3)) by A34,XREAL_1:74; then (2*n)/((2*n) to_power (2/3)) < 20 by A35,XCMPLX_1:89; then ((2*n) to_power 1)/((2*n) to_power (2/3)) < 20 by POWER:25; then A36: ((2*n) to_power (1-(2/3))) < 20 by A2,POWER:29; (2*n) to_power (1/3)>0 by A2,POWER:34; then ((2*n) to_power (1/3)) to_power 3 < 20 to_power 3 by A36,POWER:37; then ((2*n) to_power ((1/3)*3)) < 20 to_power 3 by A2,POWER:33; then 2*n < 20 to_power (2+1) by POWER:25; then 2*n < (20 to_power 2)*(20 to_power 1) by POWER:27; then 2*n < (20 to_power (1+1))*20 by POWER:25; then 2*n < (20 to_power 1)*(20 to_power 1)*20 by POWER:27; then 2*n < (20 to_power 1)*20*20 by POWER:25; then 2*n < 20*20*20 by POWER:25; then 2*n/2 < 8000/2 by XREAL_1:74; hence contradiction by A2; end; end;