let X be finite set ; :: thesis: for X1 being set
for p being Prime
for i being Nat st X = { k where k is Nat : k divides p |^ i } & X1 = { k where k is Nat : k divides p |^ (i + 1) } holds
( not p |^ (i + 1) in X & X \/ {(p |^ (i + 1))} = X1 )
let X1 be set ; :: thesis: for p being Prime
for i being Nat st X = { k where k is Nat : k divides p |^ i } & X1 = { k where k is Nat : k divides p |^ (i + 1) } holds
( not p |^ (i + 1) in X & X \/ {(p |^ (i + 1))} = X1 )
let p be Prime; :: thesis: for i being Nat st X = { k where k is Nat : k divides p |^ i } & X1 = { k where k is Nat : k divides p |^ (i + 1) } holds
( not p |^ (i + 1) in X & X \/ {(p |^ (i + 1))} = X1 )
let i be Nat; :: thesis: ( X = { k where k is Nat : k divides p |^ i } & X1 = { k where k is Nat : k divides p |^ (i + 1) } implies ( not p |^ (i + 1) in X & X \/ {(p |^ (i + 1))} = X1 ) )
assume A1: ( X = { k where k is Nat : k divides p |^ i } & X1 = { k where k is Nat : k divides p |^ (i + 1) } ) ; :: thesis: ( not p |^ (i + 1) in X & X \/ {(p |^ (i + 1))} = X1 )
set i1 = i + 1;
set P = {(p |^ (i + 1))};
A2: p |^ (i + 1) = p * (p |^ i) by NEWTON:6;
p |^ (i + 1) in X1 by A1;
then A3: {(p |^ (i + 1))} c= X1 by ZFMISC_1:31;
X c= X1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in X1 )
assume x in X ; :: thesis: x in X1
then consider k being Nat such that
A4: ( x = k & k divides p |^ i ) by A1;
k divides p * (p |^ i) by A4, INT_2:2;
hence x in X1 by A4, A2, A1; :: thesis: verum

end;

then A5: X \/ {(p |^ (i + 1))} c= X1 by A3, XBOOLE_1:8;
A6: X1 c= X \/ {(p |^ (i + 1))}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X1 or x in X \/ {(p |^ (i + 1))} )
assume x in X1 ; :: thesis: x in X \/ {(p |^ (i + 1))}
then consider k being Nat such that
A7: ( x = k & k divides p |^ (i + 1) ) by A1;
consider t being Element of NAT such that
A8: ( k = p |^ t & t <= i + 1 ) by A7, PEPIN:34;

per cases ( t <= i or t = i + 1 ) by A8, NAT_1:9;

suppose t <= i ; :: thesis: x in X \/ {(p |^ (i + 1))}

then p |^ t divides p |^ i by NEWTON:89;
then x in X by A7, A8, A1;
hence x in X \/ {(p |^ (i + 1))} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose t = i + 1 ; :: thesis: x in X \/ {(p |^ (i + 1))}

then k in {(p |^ (i + 1))} by A8, TARSKI:def 1;
hence x in X \/ {(p |^ (i + 1))} by A7, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

not p |^ (i + 1) in X

proof

assume p |^ (i + 1) in X ; :: thesis: contradiction
then consider k being Nat such that
A9: ( k = p |^ (i + 1) & k divides p |^ i ) by A1;
consider t being Element of NAT such that
A10: ( p |^ (i + 1) = p |^ t & t <= i ) by A9, PEPIN:34;
p > 1 by NAT_4:14;
then i + 1 = t by A10, PEPIN:30;
hence contradiction by A10, NAT_1:13; :: thesis: verum

end;

hence ( not p |^ (i + 1) in X & X \/ {(p |^ (i + 1))} = X1 ) by A6, A5, XBOOLE_0:def 10; :: thesis: verum