let p1, p2 be Prime; :: thesis: for m being non empty Element of NAT st p1 |^ (p1 |-count m) = p2 |^ (p2 |-count m) & p1 |-count m > 0 holds
p1 = p2
let m be non empty 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 )
assume A2: p1 |-count m > 0 ; :: thesis: p1 = p2
assume A3: p1 <> p2 ; :: thesis: contradiction
A4: ( p1 <> 1 & p1 > 1 ) by INT_2:def 5;
then p1 to_power (p1 |-count m) > 1 by A2, POWER:40;
then A5: p1 |^ (p1 |-count m) > 1 by POWER:46;
not p1 divides p2 |^ (p2 |-count m) by A3, NAT_3:6;
then p1 |-count (p1 |^ (p1 |-count m)) = 0 by A1, A4, NAT_3:27;
then p1 |-count m = 0 by A4, NAT_3:25;
hence contradiction by A5, NEWTON:9; :: thesis: verum