let a, b be non zero Nat; :: thesis: ( a,b are_coprime implies support (pfexp a) misses support (pfexp b) )
set f = pfexp a;
set g = pfexp b;
assume a,b are_coprime ; :: thesis: support (pfexp a) misses support (pfexp b)
then A1: a gcd b = 1 ;
assume support (pfexp a) meets support (pfexp b) ; :: thesis: contradiction
then consider x being object 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;
A4: (pfexp a) . x = x |-count a by Def8;
A5: (pfexp b) . x = x |-count b by Def8;
(pfexp b) . x <> 0 by A3, PRE_POLY:def 7;
then A6: x divides x |^ (x |-count b) by A5, Th3;
A7: x <> 1 by INT_2:def 4;
then x |^ (x |-count b) divides b by Def7;
then A8: x divides b by A6, NAT_D:4;
(pfexp a) . x <> 0 by A2, PRE_POLY:def 7;
then A9: x divides x |^ (x |-count a) by A4, Th3;
x |^ (x |-count a) divides a by A7, Def7;
then x divides a by A9, NAT_D:4;
then x divides 1 by A1, A8, NAT_D:def 5;
hence contradiction by A7, WSIERP_1:15; :: thesis: verum