let n be Nat; :: thesis: for p being Prime st 2 < n & n div 2 < p & p <= 2 * (n div 2) holds
p |-count (n !) = 1
let p be Prime; :: thesis: ( 2 < n & n div 2 < p & p <= 2 * (n div 2) implies p |-count (n !) = 1 )
assume A1: ( 2 < n & n div 2 < p & p <= 2 * (n div 2) ) ; :: thesis: p |-count (n !) = 1

per cases ( n is even or n is odd ) ;

suppose n is even ; :: thesis: p |-count (n !) = 1

then consider k being Nat such that
A2: n = 2 * k by ABIAN:def 2;
A3: n div 2 = k by A2, NAT_D:18;
A4: p < 2 * k

proof

assume p >= 2 * k ; :: thesis: contradiction
then p = 2 * k by A1, A3, XXREAL_0:1;
hence contradiction by A2, A1, NUMBER06:2; :: thesis: verum

end;

A5: n < 2 * p by A2, A3, A1, XREAL_1:68;
A6: p |^ 1 divides n ! by A3, A1, A2, NEWTON:41;
A7: p <> 1 by INT_2:def 4;
not p |^ (1 + 1) divides n ! by A4, A2, Th36, A5;
hence p |-count (n !) = 1 by A6, A7, NAT_3:def 7; :: thesis: verum

end;

suppose n is odd ; :: thesis: p |-count (n !) = 1

then consider k being Nat such that
A8: n = (2 * k) + 1 by ABIAN:9;
1 div 2 = 0 by NAT_D:27;
then A9: n div 2 = k + 0 by A8, NAT_D:61;
k + 1 <= p by A9, A1, NAT_1:13;
then (k + 1) + k < p + p by A9, A1, XREAL_1:8;
then A10: n < 2 * p by A8;
A11: p <= (2 * k) + 1 by A9, A1, NAT_1:13;
then A12: p |^ 1 divides n ! by A8, NEWTON:41;
A13: p <> 1 by INT_2:def 4;
not p |^ (1 + 1) divides n ! by A8, A11, Th36, A10;
hence p |-count (n !) = 1 by A12, A13, NAT_3:def 7; :: thesis: verum

end;

end;