hereby :: thesis: ( ( for n being Nat st n > 1 holds
ex p being Prime st p |-count (n !) = 1 ) implies for n being Nat st n > 1 holds
ex p being Prime st
( n < p & p < 2 * n ) )

assume A1: for n being Nat st n > 1 holds
ex p being Prime st
( n < p & p < 2 * n ) ; :: thesis: for n being Nat st n > 1 holds
ex p being Prime st b₃ |-count (p !) = 1
let n be Nat; :: thesis: ( n > 1 implies ex p being Prime st b₂ |-count (p !) = 1 )
assume A2: n > 1 ; :: thesis: ex p being Prime st b₂ |-count (p !) = 1
( not not n = 0 & ... & not n = 3 or n > 3 ) ;

per cases then ( n = 2 or n = 3 or ( n > 3 & n is even ) or ( n > 3 & n is odd ) ) by A2;

suppose n = 2 ; :: thesis: ex p being Prime st b₂ |-count (p !) = 1

then 2 |-count (n !) = 1 by NAT_3:22, NEWTON:14;
hence ex p being Prime st p |-count (n !) = 1 by XPRIMES1:2; :: thesis: verum

end;

suppose n = 3 ; :: thesis: ex p being Prime st b₂ |-count (p !) = 1

then n ! = 2 * 3 by STIRL2_1:50;
then 2 |-count (n !) = (2 |-count 2) + (2 |-count 3) by NAT_3:28, XPRIMES1:2
.= 1 + (2 |-count 3) by NAT_3:22
.= 1 + 0 by NAT_3:24, XPRIMES1:3 ;
hence ex p being Prime st p |-count (n !) = 1 by XPRIMES1:2; :: thesis: verum

end;

suppose A3: ( n > 3 & n is even ) ; :: thesis: ex p being Prime st b₂ |-count (p !) = 1

then consider k being Nat such that
A4: n = 2 * k by ABIAN:def 2;
k <> 0 by A4, A3;
then ( k >= 1 & k <> 1 ) by A4, A3, NAT_1:14;
then k > 1 by XXREAL_0:1;
then consider p being Prime such that
A5: ( k < p & p < 2 * k ) by A1;
take p = p; :: thesis: p |-count (n !) = 1
A6: 2 < n by A3, XXREAL_0:2;
n div 2 = k by A4, NAT_D:18;
hence p |-count (n !) = 1 by A6, A5, Th38; :: thesis: verum

end;

suppose A7: ( n > 3 & n is odd ) ; :: thesis: ex p being Prime st b₂ |-count (p !) = 1

then consider k being Nat such that
A8: n = (2 * k) + 1 by ABIAN:9;
k <> 0 by A8, A7;
then ( k >= 1 & k <> 1 ) by A8, A7, NAT_1:14;
then k > 1 by XXREAL_0:1;
then consider p being Prime such that
A9: ( k < p & p < 2 * k ) by A1;
take p = p; :: thesis: p |-count (n !) = 1
A10: 2 < n by A7, XXREAL_0:2;
1 div 2 = 0 by NAT_D:27;
then n div 2 = k + 0 by A8, NAT_D:61;
then n div 2 = k ;
hence p |-count (n !) = 1 by A10, A9, Th38; :: thesis: verum

end;

end;

end;

assume A11: for n being Nat st n > 1 holds
ex p being Prime st p |-count (n !) = 1 ; :: thesis: for n being Nat st n > 1 holds
ex p being Prime st
( n < p & p < 2 * n )
let n be Nat; :: thesis: ( n > 1 implies ex p being Prime st
( n < p & p < 2 * n ) )
assume A12: n > 1 ; :: thesis: ex p being Prime st
( n < p & p < 2 * n )
( n + n > 1 + 1 & 1 + 1 >= 1 ) by A12, XREAL_1:8;
then 2 * n > 1 by XXREAL_0:2;
then consider p being Prime such that
A13: p |-count ((2 * n) !) = 1 by A11;
take p ; :: thesis: ( n < p & p < 2 * n )
p <> 1 by INT_2:def 4;
then p |^ 1 divides (2 * n) ! by A13, NAT_3:def 7;
then A14: p <= 2 * n by NAT_4:19;
thus n < p :: thesis: p < 2 * n

proof

assume n >= p ; :: thesis: contradiction
then A15: 2 * n >= 2 * p by XREAL_1:66;
0 + p < p + p by XREAL_1:8;
then A16: p * (2 * p) divides (2 * n) ! by A15, Th37;
p |^ (1 + 1) = (p |^ 1) * p by NEWTON:6;
then p |^ 2 divides 2 * (p * p) ;
hence contradiction by A13, A16, INT_2:9, MOEBIUS2:40; :: thesis: verum

end;

assume p >= 2 * n ; :: thesis: contradiction
then A17: p = 2 * n by A14, XXREAL_0:1;
then p = 2 by NUMBER06:2;
hence contradiction by A17, A12; :: thesis: verum