let p1, p2 be Prime; :: thesis: for m being non zero Element of NAT st p1 |^ (p1 |-count m) = p2 |^ (p2 |-count m) & p1 |-count m > 0 holds
p1 = p2
let m be non zero Element of NAT ; :: thesis: ( p1 |^ (p1 |-count m) = p2 |^ (p2 |-count m) & p1 |-count m > 0 implies p1 = p2 )
assume A1: p1 |^ (p1 |-count m) = p2 |^ (p2 |-count m) ; :: thesis: ( not p1 |-count m > 0 or p1 = p2 )
A2: p1 > 1 by INT_2:def 4;
assume p1 |-count m > 0 ; :: thesis: p1 = p2
then p1 to_power (p1 |-count m) > 1 by A2, POWER:35;
then A3: p1 |^ (p1 |-count m) > 1 by POWER:41;
assume p1 <> p2 ; :: thesis: contradiction
then ( p1 <> 1 & not p1 divides p2 |^ (p2 |-count m) ) by INT_2:def 4, NAT_3:6;
then p1 |-count (p1 |^ (p1 |-count m)) = 0 by A1, NAT_3:27;
then p1 |-count m = 0 by A2, NAT_3:25;
hence contradiction by A3, NEWTON:4; :: thesis: verum