let n, m, r be natural number ; :: thesis: for p being natural prime number st n = (p |^ r) * m & not p divides m holds
(n choose (p |^ r)) mod p <> 0
let p be natural prime number ; :: 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 )
assume A2: not p divides m ; :: thesis: (n choose (p |^ r)) mod p <> 0
reconsider p' = p as prime Element of NAT by ORDINAL1:def 13;
reconsider k1 = p' |^ r as non zero Element of NAT by ORDINAL1:def 13;
set S = INT.Group k1;
A3: multMagma(# (Segm k1),(addint k1) #) = INT.Group k1 by GR_CY_1:def 6;
A4: card (INT.Group k1) = k1 by Lm2;
set CS = the carrier of (INT.Group k1);
card the carrier of (INT.Group k1) = card k1 by A3, CARD_1:def 12;
then A5: card the carrier of (INT.Group k1) = p |^ r by CARD_1:def 5;
reconsider k2 = m as Element of NAT by ORDINAL1:def 13;
set T = Segm k2;
card (Segm k2) = card k2 by CARD_1:def 12;
then A6: card (Segm k2) = m by CARD_1:def 5;
reconsider x1 = 1, x2 = 0 as set ;
A7: k2 <> 0 by A2, NAT_D:6;
then reconsider T = Segm k2 as non empty finite set ;
set X = [:the carrier of (INT.Group k1),T:];
A8: card [:the carrier of (INT.Group k1),T:] = n by A1, A5, A6, CARD_2:65;
reconsider X' = [:the carrier of (INT.Group k1),T:] as non empty finite set ;
A9: m > 0 by A7;
reconsider n' = n as real number ;

now

assume p |^ r > n ; :: thesis: contradiction
then (p |^ r) * m > n * m by A9, XREAL_1:70;
then n' / n' > (n' * m) / n' by A1, XREAL_1:76;
then 1 > (n' * m) / n' by A8, XCMPLX_1:60;
then 1 > (n' / n') * m by XCMPLX_1:75;
then 1 > 1 * m by A8, XCMPLX_1:60;
then m < 0 + 1 ;
hence contradiction by A9, NAT_1:13; :: thesis: verum

end;

then A10: card k1 c= card (card [:the carrier of (INT.Group k1),T:]) by A8, NAT_1:41;
set E = the_subsets_of_card k1,X';
set LO = the_left_operation_of (INT.Group k1),T;
reconsider E' = the_subsets_of_card k1,X' as non empty finite set by A10, Th2;
card (Choose [:the carrier of (INT.Group k1),T:],k1,x1,x2) = card E' by Th3;
then A11: card E' = n choose k1 by A8, CARD_FIN:18;
set LO' = the_extension_of_left_operation_of k1,(the_left_operation_of (INT.Group k1),T);
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 A4, A10, Lm4
.= card T by Lm3
.= card k2 by CARD_1:def 12 ;
then A12: card (the_fixed_points_of (the_extension_of_left_operation_of k1,(the_left_operation_of (INT.Group k1),T))) = m by CARD_1:def 5;
A13: INT.Group k1 is_p-group_of_prime p by A4, Def17;

now

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

end;

hence (n choose (p |^ r)) mod p <> 0 by A11, A12, A13, Th11; :: thesis: verum