defpred S1[ Element of NAT , Element of NAT , Prime] means ( $1 < $3 & $3 <= 2 * $1 & $3 |-count $2 > 0 );
defpred S2[ Element of NAT , Element of NAT , Prime] means ( sqrt (2 * $1) < $3 & $3 <= (2 * $1) / 3 & $3 |-count $2 > 0 );
defpred S3[ Element of NAT , Element of NAT , Prime] means ( $3 <= sqrt (2 * $1) & $3 |-count $2 > 0 );
let n, m be Element of NAT ; :: thesis: ( m = (2 * n) choose n & n >= 3 implies 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) < p & p <= (2 * n) / 3 & p |-count m > 0 ) } ))) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( n < p & p <= 2 * n & p |-count m > 0 ) } )) )
assume A1: m = (2 * n) choose n ; :: thesis: ( not n >= 3 or 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) < p & p <= (2 * n) / 3 & p |-count m > 0 ) } ))) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( n < p & p <= 2 * n & p |-count m > 0 ) } )) )
set X3 = { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } ;
set X2 = { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ;
set X1 = { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } ;
set f1 = Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } ;
set f2 = Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ;
set f3 = Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } ;
set n1 = Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } );
set n2 = Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } );
set n3 = Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } );
A2: for p being Prime
for n being Element of NAT
for m being non empty Element of NAT
for X being set st X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } & not p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = 0 from NAT_4:sch 2();
 set k = ((Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ))) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } ));
A3: for p being Prime
for n being Element of NAT
for m being non empty Element of NAT
for X being set st X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } holds
Product (Sgm X) > 0 from NAT_4:sch 1();
 assume A4: n >= 3 ; :: thesis: 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) < p & p <= (2 * n) / 3 & p |-count m > 0 ) } ))) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( n < p & p <= 2 * n & p |-count m > 0 ) } ))
A5: now
2 * n < 3 * n by A4, XREAL_1:70;
then A6: (2 * n) / 3 < (3 * n) / 3 by XREAL_1:76;
assume n < (2 * n) / 3 ; :: thesis: contradiction
hence contradiction by A6; :: thesis: verum
end;
A7: now
( sqrt 2 < sqrt 3 & sqrt 3 <= sqrt n ) by A4, SQUARE_1:94, SQUARE_1:95;
then A8: sqrt 2 < sqrt n by XXREAL_0:2;
sqrt n > 0 by A4, SQUARE_1:93;
then (sqrt 2) * (sqrt n) < (sqrt n) * (sqrt n) by A8, XREAL_1:70;
then sqrt (2 * n) < (sqrt n) * (sqrt n) by SQUARE_1:97;
then A9: sqrt (2 * n) < sqrt (n ^2 ) by SQUARE_1:97;
assume n < sqrt (2 * n) ; :: thesis: contradiction
hence contradiction by A9, SQUARE_1:def 4; :: thesis: verum
end;
m * (2 * n) >= ((4 |^ n) / (2 * n)) * (2 * n) by A1, Th6, XREAL_1:66;
then A10: m <> 0 by A4;
A11: for p being Prime
for n being Element of NAT
for m being non empty Element of NAT
for X being set st X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } holds
Product (Sgm X) > 0 from NAT_4:sch 1();
 then A12: Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } ) > 0 by A10;
A13: for p being Prime
for n being Element of NAT
for m being non empty Element of NAT
for X being set st X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } holds
Product (Sgm X) > 0 from NAT_4:sch 1();
 then A14: Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ) > 0 by A10;
A15: for p being Prime
for n being Element of NAT
for m being non empty Element of NAT
for X being set st X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } & not p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = 0 from NAT_4:sch 2();
 A16: for p being Prime
for n being Element of NAT
for m being non empty Element of NAT
for X being set st X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } & not p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = 0 from NAT_4:sch 2();
 A17: for p being Prime st p > 2 * n holds
( p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0 )
proof
let p be Prime; :: thesis: ( p > 2 * n implies ( p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0 ) )
assume A18: p > 2 * n ; :: thesis: ( p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0 )
then A19: p |-count m = 0 by A1, A4, Lm9;
now
assume p |^ (p |-count m) in { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } ; :: thesis: contradiction
then ex p' being prime Element of NAT st
( p' |^ (p' |-count m) = p |^ (p |-count m) & S3[n,m,p'] ) ;
hence contradiction by A10, A19, Th22; :: thesis: verum
end;
hence p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = 0 by A10, A16; :: thesis: ( p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0 )
now
assume p |^ (p |-count m) in { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ; :: thesis: contradiction
then ex p' being prime Element of NAT st
( p' |^ (p' |-count m) = p |^ (p |-count m) & S2[n,m,p'] ) ;
hence contradiction by A10, A19, Th22; :: thesis: verum
end;
hence p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = 0 by A10, A2; :: thesis: p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0
now
assume p |^ (p |-count m) in { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } ; :: thesis: contradiction
then ex p' being prime Element of NAT st
( p' |^ (p' |-count m) = p |^ (p |-count m) & S1[n,m,p'] ) ;
hence contradiction by A10, A18, Th22; :: thesis: verum
end;
hence p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0 by A10, A15; :: thesis: verum
end;
A20: for p being Prime st (2 * n) / 3 < p & p <= n holds
( p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0 )
proof
let p be Prime; :: thesis: ( (2 * n) / 3 < p & p <= n implies ( p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0 ) )
assume that
A21: (2 * n) / 3 < p and
A22: p <= n ; :: thesis: ( p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0 )
A23: p |-count m = 0 by A1, A4, A21, A22, Lm9;
now
assume p |^ (p |-count m) in { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } ; :: thesis: contradiction
then ex p' being prime Element of NAT st
( p' |^ (p' |-count m) = p |^ (p |-count m) & S3[n,m,p'] ) ;
hence contradiction by A10, A23, Th22; :: thesis: verum
end;
hence p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = 0 by A10, A16; :: thesis: ( p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0 )
now
assume p |^ (p |-count m) in { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ; :: thesis: contradiction
then ex p' being prime Element of NAT st
( p' |^ (p' |-count m) = p |^ (p |-count m) & S2[n,m,p'] ) ;
hence contradiction by A10, A21, Th22; :: thesis: verum
end;
hence p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = 0 by A10, A2; :: thesis: p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0
now
assume p |^ (p |-count m) in { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } ; :: thesis: contradiction
then ex p' being prime Element of NAT st
( p' |^ (p' |-count m) = p |^ (p |-count m) & S1[n,m,p'] ) ;
hence contradiction by A10, A22, Th22; :: thesis: verum
end;
hence p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0 by A10, A15; :: thesis: verum
end;
A24: for p being Prime
for n being Element of NAT
for m being non empty Element of NAT
for X being set st X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } & p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = p |-count m from NAT_4:sch 3();
 A25: for p being Prime st sqrt (2 * n) < p & p <= (2 * n) / 3 holds
( p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = p |-count m )
proof
let p be Prime; :: thesis: ( sqrt (2 * n) < p & p <= (2 * n) / 3 implies ( p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = p |-count m ) )
assume that
A26: sqrt (2 * n) < p and
A27: p <= (2 * n) / 3 ; :: thesis: ( p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = p |-count m )
now
assume p |^ (p |-count m) in { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } ; :: thesis: contradiction
then ex p' being prime Element of NAT st
( p' |^ (p' |-count m) = p |^ (p |-count m) & S3[n,m,p'] ) ;
hence contradiction by A10, A26, Th22; :: thesis: verum
end;
hence p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = 0 by A10, A16; :: thesis: ( p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = p |-count m )
now
assume p |^ (p |-count m) in { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } ; :: thesis: contradiction
then ex p' being prime Element of NAT st
( p' |^ (p' |-count m) = p |^ (p |-count m) & S1[n,m,p'] ) ;
then n < p by A10, Th22;
hence contradiction by A5, A27, XXREAL_0:2; :: thesis: verum
end;
hence p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0 by A10, A15; :: thesis: p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = p |-count m
A28: p in NAT by ORDINAL1:def 13;
per cases ( p |-count m > 0 or p |-count m = 0 ) ;
suppose p |-count m > 0 ; :: thesis: p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = p |-count m
then p |^ (p |-count m) in { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } by A26, A27, A28;
hence p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = p |-count m by A10, A24; :: thesis: verum
end;
suppose A29: p |-count m = 0 ; :: thesis: p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = p |-count m
now
assume p |^ (p |-count m) in { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ; :: thesis: contradiction
then ex p' being prime Element of NAT st
( p' |^ (p' |-count m) = p |^ (p |-count m) & S2[n,m,p'] ) ;
hence contradiction by A10, A29, Th22; :: thesis: verum
end;
hence p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = p |-count m by A10, A2, A29; :: thesis: verum
end;
end;
end;
A30: for p being Prime
for n being Element of NAT
for m being non empty Element of NAT
for X being set st X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } & p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = p |-count m from NAT_4:sch 3();
 A31: for p being Prime st n < p & p <= 2 * n holds
( p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = p |-count m )
proof
let p be Prime; :: thesis: ( n < p & p <= 2 * n implies ( p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = p |-count m ) )
assume that
A32: n < p and
A33: p <= 2 * n ; :: thesis: ( p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = p |-count m )
now
assume p |^ (p |-count m) in { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } ; :: thesis: contradiction
then ex p' being prime Element of NAT st
( p' |^ (p' |-count m) = p |^ (p |-count m) & S3[n,m,p'] ) ;
then p <= sqrt (2 * n) by A10, Th22;
hence contradiction by A7, A32, XXREAL_0:2; :: thesis: verum
end;
hence p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = 0 by A10, A16; :: thesis: ( p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = p |-count m )
now
assume p |^ (p |-count m) in { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ; :: thesis: contradiction
then ex p' being prime Element of NAT st
( p' |^ (p' |-count m) = p |^ (p |-count m) & S2[n,m,p'] ) ;
then p <= (2 * n) / 3 by A10, Th22;
hence contradiction by A5, A32, XXREAL_0:2; :: thesis: verum
end;
hence p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = 0 by A10, A2; :: thesis: p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = p |-count m
A34: p in NAT by ORDINAL1:def 13;
per cases ( p |-count m > 0 or p |-count m = 0 ) ;
suppose p |-count m > 0 ; :: thesis: p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = p |-count m
then p |^ (p |-count m) in { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } by A32, A33, A34;
hence p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = p |-count m by A10, A30; :: thesis: verum
end;
suppose A35: p |-count m = 0 ; :: thesis: p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = p |-count m
now
assume p |^ (p |-count m) in { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } ; :: thesis: contradiction
then ex p' being prime Element of NAT st
( p' |^ (p' |-count m) = p |^ (p |-count m) & S1[n,m,p'] ) ;
hence contradiction by A10, A35, Th22; :: thesis: verum
end;
hence p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = p |-count m by A10, A15, A35; :: thesis: verum
end;
end;
end;
A36: for p being Prime
for n being Element of NAT
for m being non empty Element of NAT
for X being set st X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } & p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = p |-count m from NAT_4:sch 3();
 A37: for p being Prime st p <= sqrt (2 * n) holds
( p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = p |-count m )
proof
let p be Prime; :: thesis: ( p <= sqrt (2 * n) implies ( p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = p |-count m ) )
A38: p in NAT by ORDINAL1:def 13;
assume A39: p <= sqrt (2 * n) ; :: thesis: ( p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = p |-count m )
now
assume p |^ (p |-count m) in { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ; :: thesis: contradiction
then ex p' being prime Element of NAT st
( p' |^ (p' |-count m) = p |^ (p |-count m) & S2[n,m,p'] ) ;
hence contradiction by A10, A39, Th22; :: thesis: verum
end;
hence p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } )) = 0 by A10, A2; :: thesis: ( p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0 & p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = p |-count m )
now
assume p |^ (p |-count m) in { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } ; :: thesis: contradiction
then ex p' being prime Element of NAT st
( p' |^ (p' |-count m) = p |^ (p |-count m) & S1[n,m,p'] ) ;
then n < p by A10, Th22;
hence contradiction by A7, A39, XXREAL_0:2; :: thesis: verum
end;
hence p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )) = 0 by A10, A15; :: thesis: p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = p |-count m
per cases ( p |-count m > 0 or p |-count m = 0 ) ;
suppose p |-count m > 0 ; :: thesis: p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = p |-count m
then p |^ (p |-count m) in { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } by A39, A38;
hence p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = p |-count m by A10, A36; :: thesis: verum
end;
suppose A40: p |-count m = 0 ; :: thesis: p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = p |-count m
now
assume p |^ (p |-count m) in { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } ; :: thesis: contradiction
then ex p' being prime Element of NAT st
( p' |^ (p' |-count m) = p |^ (p |-count m) & S3[n,m,p'] ) ;
hence contradiction by A10, A40, Th22; :: thesis: verum
end;
hence p |-count (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) = p |-count m by A10, A16, A40; :: thesis: verum
end;
end;
end;
A41: for p being Element of NAT st p is prime holds
p |-count m = p |-count (((Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ))) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )))
proof
reconsider n3 = Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } ) as non empty Element of NAT by A10, A11;
reconsider n2 = Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ) as non empty Element of NAT by A10, A13;
reconsider n1 = Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } ) as non empty Element of NAT by A10, A3;
let p be Element of NAT ; :: thesis: ( p is prime implies p |-count m = p |-count (((Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ))) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } ))) )
assume A42: p is prime ; :: thesis: p |-count m = p |-count (((Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ))) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )))
then A43: p |-count (((Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ))) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } ))) = (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 ( p > 2 * n or ( n < p & p <= 2 * n ) or ( (2 * n) / 3 < p & p <= n ) or ( sqrt (2 * n) < p & p <= (2 * n) / 3 ) or p <= sqrt (2 * n) ) ;
suppose A44: p > 2 * n ; :: thesis: p |-count m = p |-count (((Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ))) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )))
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 p |-count m = p |-count (((Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ))) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } ))) by A17, A42, A43, A44, A45; :: thesis: verum
end;
suppose A46: ( n < p & p <= 2 * n ) ; :: thesis: p |-count m = p |-count (((Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ))) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )))
then ( p |-count n1 = 0 & p |-count n2 = 0 ) by A31, A42;
hence p |-count m = p |-count (((Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ))) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } ))) by A31, A42, A43, A46; :: thesis: verum
end;
suppose A47: ( (2 * n) / 3 < p & p <= n ) ; :: thesis: p |-count m = p |-count (((Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ))) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )))
then A48: p |-count n2 = 0 by A20, A42;
( p |-count m = 0 & p |-count n1 = 0 ) by A1, A4, A20, A42, A47, Lm9;
hence p |-count m = p |-count (((Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ))) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } ))) by A20, A42, A43, A47, A48; :: thesis: verum
end;
suppose A49: ( sqrt (2 * n) < p & p <= (2 * n) / 3 ) ; :: thesis: p |-count m = p |-count (((Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ))) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )))
then ( p |-count n1 = 0 & p |-count n2 = p |-count m ) by A25, A42;
hence p |-count m = p |-count (((Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ))) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } ))) by A25, A42, A43, A49; :: thesis: verum
end;
suppose A50: p <= sqrt (2 * n) ; :: thesis: p |-count m = p |-count (((Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ))) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } )))
then ( p |-count n1 = p |-count m & p |-count n2 = 0 ) by A37, A42;
hence p |-count m = p |-count (((Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } )) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S2[n,m,p] } ))) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S1[n,m,p] } ))) by A37, A42, A43, A50; :: thesis: verum
end;
end;
end;
Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : S3[n,m,p] } ) > 0 by A10, A3;
hence 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) < p & p <= (2 * n) / 3 & p |-count m > 0 ) } ))) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( n < p & p <= 2 * n & p |-count m > 0 ) } )) by A10, A14, A12, A41, Th21; :: thesis: verum