reconsider x1 = 1, x2 = 0 as set ;
let n, m, r be Nat; :: thesis: for p being Prime st n = (p |^ r) * m & not p divides m holds
(n choose (p |^ r)) mod p <> 0
let p be Prime; :: thesis: ( n = (p |^ r) * m & not p divides m implies (n choose (p |^ r)) mod p <> 0 )
assume A1: n = (p |^ r) * m ; :: thesis: ( p divides m or (n choose (p |^ r)) mod p <> 0 )
reconsider n9 = n as Real ;
reconsider k2 = m as Element of NAT by ORDINAL1:def 12;
reconsider p9 = p as prime Element of NAT by ORDINAL1:def 12;
reconsider k1 = p9 |^ r as non zero Element of NAT by ORDINAL1:def 12;
set S = INT.Group k1;
set CS = the carrier of (INT.Group k1);
set T = Segm k2;
A2: card (Segm k2) = m ;
assume A3: not p divides m ; :: thesis: (n choose (p |^ r)) mod p <> 0
then A4: k2 <> 0 by NAT_D:6;
then reconsider T = Segm k2 as non empty finite set ;
set X = [: the carrier of (INT.Group k1),T:];
reconsider X9 = [: the carrier of (INT.Group k1),T:] as non empty finite set ;
set E = the_subsets_of_card (k1,X9);
multMagma(# (Segm k1),(addint k1) #) = INT.Group k1 by GR_CY_1:def 5;
then card the carrier of (INT.Group k1) = p |^ r ;
then A5: card [: the carrier of (INT.Group k1),T:] = n by A1, A2, CARD_2:46;

now :: thesis: not p |^ r > n

assume p |^ r > n ; :: thesis: contradiction
then (p |^ r) * m > n * m by A4, XREAL_1:68;
then n9 / n9 > (n9 * m) / n9 by A1, XREAL_1:74;
then 1 > (n9 * m) / n9 by A5, XCMPLX_1:60;
then 1 > (n9 / n9) * m by XCMPLX_1:74;
then 1 > 1 * m by A5, XCMPLX_1:60;
then m < 0 + 1 ;
hence contradiction by A4, NAT_1:13; :: thesis: verum

end;

then A6: card (Segm k1) c= card (Segm (card [: the carrier of (INT.Group k1),T:])) by A5, NAT_1:40;
then reconsider E9 = the_subsets_of_card (k1,X9) as non empty finite set by Th1;
card (Choose ([: the carrier of (INT.Group k1),T:],k1,x1,x2)) = card E9 by Th2;
then A7: card E9 = n choose k1 by A5, CARD_FIN:16;
set LO = the_left_operation_of ((INT.Group k1),T);
set LO9 = the_extension_of_left_operation_of (k1,(the_left_operation_of ((INT.Group k1),T)));

A8: now :: thesis: not m mod p9 = 0

assume m mod p9 = 0 ; :: thesis: contradiction
then m = (p * (m div p)) + 0 by NAT_D:2;
hence contradiction by A3, NAT_D:def 3; :: thesis: verum

end;

A9: card (INT.Group k1) = k1 by Lm1;
then card (the_fixed_points_of (the_extension_of_left_operation_of (k1,(the_left_operation_of ((INT.Group k1),T))))) = card { [: the carrier of (INT.Group k1),{t}:] where t is Element of T : verum } by A6, Lm4
.= card k2 by Lm3 ;
then A10: card (the_fixed_points_of (the_extension_of_left_operation_of (k1,(the_left_operation_of ((INT.Group k1),T))))) = m ;
INT.Group k1 is p -group by A9;
hence (n choose (p |^ r)) mod p <> 0 by A7, A10, A8, Th9; :: thesis: verum