let a, b be non empty Nat; :: thesis: ( a,b are_relative_prime implies support (pfexp a) misses support (pfexp b) )
assume a,b are_relative_prime ; :: thesis: support (pfexp a) misses support (pfexp b)
then A1: a gcd b = 1 by INT_2:def 4;
set f = pfexp a;
set g = pfexp b;
assume support (pfexp a) meets support (pfexp b) ; :: thesis: contradiction
then consider x being set such that
A2: x in support (pfexp a) and
A3: x in support (pfexp b) by XBOOLE_0:3;
reconsider x = x as Prime by A2, Th34;
A5: (pfexp a) . x <> 0 by A2, POLYNOM1:def 7;
A6: (pfexp a) . x = x |-count a by Def8;
A7: x <> 1 by INT_2:def 5;
then A8: x |^ (x |-count a) divides a by Def7;
x divides x |^ (x |-count a) by A5, A6, Th3;
then A9: x divides a by A8, NAT_D:4;
A10: (pfexp b) . x <> 0 by A3, POLYNOM1:def 7;
A11: (pfexp b) . x = x |-count b by Def8;
A12: x |^ (x |-count b) divides b by A7, Def7;
x divides x |^ (x |-count b) by A10, A11, Th3;
then x divides b by A12, NAT_D:4;
then x divides 1 by A1, A9, NAT_D:def 5;
hence contradiction by A7, WSIERP_1:20; :: thesis: verum