let n be Nat; :: thesis: for p being natural prime number st ( for r being natural number holds n <> p |^ r ) holds
ex s being Element of NAT st
( s is prime & s divides n & s <> p )
let p be natural prime number ; :: thesis: ( ( for r being natural number holds n <> p |^ r ) implies ex s being Element of NAT st
( s is prime & s divides n & s <> p ) )
assume A2: for r being natural number holds n <> p |^ r ; :: thesis: ex s being Element of NAT st
( s is prime & s divides n & s <> p )
per cases ( n = 0 or n <> 0 ) ;
suppose a0: n = 0 ; :: thesis: ex s being Element of NAT st
( s is prime & s divides n & s <> p )
per cases ( p = 2 or p <> 2 ) ;
suppose a1: p = 2 ; :: thesis: ex s being Element of NAT st
( s is prime & s divides n & s <> p )
take s = 3; :: thesis: ( s is prime & s divides n & s <> p )
thus s is prime by PEPIN:44; :: thesis: ( s divides n & s <> p )
thus s divides n by a0, INT_2:16; :: thesis: s <> p
thus s <> p by a1; :: thesis: verum
end;
suppose a1: p <> 2 ; :: thesis: ex s being Element of NAT st
( s is prime & s divides n & s <> p )
take s = 2; :: thesis: ( s is prime & s divides n & s <> p )
thus s is prime by INT_2:44; :: thesis: ( s divides n & s <> p )
thus s divides n by a0, INT_2:16; :: thesis: s <> p
thus s <> p by a1; :: thesis: verum
end;
end;
end;
suppose A1: n <> 0 ; :: thesis: ex s being Element of NAT st
( s is prime & s divides n & s <> p )
A3: p > 1 by INT_2:def 5;
reconsider r1 = p |-count n as Element of NAT ;
A4: p |^ r1 divides n by A1, A3, NAT_3:def 7;
A5: not p |^ (r1 + 1) divides n by A1, A3, NAT_3:def 7;
consider s1 being natural number such that
A6: n = (p |^ r1) * s1 by A4, NAT_D:def 3;
s1 >= 2
proof
assume not s1 >= 2 ; :: thesis: contradiction
then s1 < 1 + 1 ;
then s1 <= 1 by NAT_1:13;
then ( s1 = 0 or s1 = 1 ) by NAT_1:26;
hence contradiction by A1, A2, A6; :: thesis: verum
end;
then consider s being Element of NAT such that
A7: s is prime and
A8: s divides s1 by INT_2:48;
A9: s1 divides n by A6, NAT_D:def 3;
take s ; :: thesis: ( s is prime & s divides n & s <> p )
s <> p
proof
assume s = p ; :: thesis: contradiction
then consider s2 being natural number such that
A10: s1 = p * s2 by A8, NAT_D:def 3;
n = ((p |^ r1) * p) * s2 by A6, A10
.= (p |^ (r1 + 1)) * s2 by NEWTON:11 ;
hence contradiction by A5, NAT_D:def 3; :: thesis: verum
end;
hence ( s is prime & s divides n & s <> p ) by A7, A8, A9, NAT_D:4; :: thesis: verum
end;
end;