let a, b, c, d be Nat; :: thesis: ( a gcd b = 1 & a * b = c |^ d implies ex e, f being Nat st
( a = e |^ d & b = f |^ d ) )
assume that
A1: a gcd b = 1 and
A2: a * b = c |^ d ; :: thesis: ex e, f being Nat st
( a = e |^ d & b = f |^ d )
set e = a gcd c;
a gcd c divides c by NAT_D:def 5;
then A3: (a gcd c) |^ d divides c |^ d by Th14;
a gcd c divides a by NAT_D:def 5;
then (a gcd c) gcd b = 1 by A1, Th15, NEWTON:57;
then ((a gcd c) |^ d) gcd b = 1 by Th12;
then (a gcd c) |^ d divides a by A2, A3, Th29;
then consider g being Nat such that
A4: ((a gcd c) |^ d) * g = a by NAT_D:def 3;
reconsider g = g as Element of NAT by ORDINAL1:def 12;

A5: now :: thesis: ( d <> 0 implies ex e, f being Nat st
( a = e |^ d & b = f |^ d ) )

assume A6: d <> 0 ; :: thesis: ex e, f being Nat st
( a = e |^ d & b = f |^ d )
then consider d1 being Nat such that
A7: d = 1 + d1 by NAT_1:10, NAT_1:14;
reconsider d1 = d1 as Element of NAT by ORDINAL1:def 12;
A8: d >= 1 by A6, NAT_1:14;

A9: now :: thesis: ( a gcd c <> 0 implies ex e, f being Nat st
( a = e |^ d & b = f |^ d ) )

assume A10: a gcd c <> 0 ; :: thesis: ex e, f being Nat st
( a = e |^ d & b = f |^ d )
then A11: ( a <> 0 or c <> 0 ) by INT_2:5;
then A12: a <> 0 by A2, CARD_4:3;

A13: now :: thesis: ( c <> 0 implies ex e, f being Nat st
( a = e |^ d & b = f |^ d ) )

reconsider e1 = a gcd c as Real ;
assume A14: c <> 0 ; :: thesis: ex e, f being Nat st
( a = e |^ d & b = f |^ d )
then consider a1, c1 being Integer such that
A15: a = (a gcd c) * a1 and
A16: (a gcd c) * c1 = c and
A17: a1,c1 are_coprime by INT_2:23;
reconsider a1 = a1, c1 = c1 as Element of NAT by A12, A14, A15, A16, Lm6;
a1 = (((a gcd c) |^ (d1 + 1)) * g) / (a gcd c) by A4, A7, A10, A15, XCMPLX_1:89
.= (((a gcd c) * ((a gcd c) |^ d1)) * g) / (a gcd c) by NEWTON:6
.= ((a gcd c) * (((a gcd c) |^ d1) * g)) / (a gcd c)
.= ((a gcd c) |^ d1) * g by A10, XCMPLX_1:89 ;
then A18: g divides a1 ;
a1 gcd c1 = 1 by A17, INT_2:def 3;
then g gcd c1 = 1 by A18, Th15, NEWTON:57;
then A19: g gcd (c1 |^ d) = 1 by Th12;
A20: e1 |^ d <> 0 by A10, CARD_4:3;
c1 = c / (a gcd c) by A10, A16, XCMPLX_1:89;
then A21: c1 |^ d = (((a gcd c) |^ d) * (g * b)) / ((a gcd c) |^ d) by A2, A4, PREPOWER:8
.= g * b by A20, XCMPLX_1:89 ;
then g divides c1 |^ d ;
then g = 1 by A19, NEWTON:49;
hence ex e, f being Nat st
( a = e |^ d & b = f |^ d ) by A4, A21; :: thesis: verum

end;

now :: thesis: ( 0 = c implies ex e, f being Nat st
( a = e |^ d & b = f |^ d ) )

assume 0 = c ; :: thesis: ex e, f being Nat st
( a = e |^ d & b = f |^ d )
then A22: b = 0 by A2, A8, A11, NEWTON:11, XCMPLX_1:6;
then a = 1 by A1, NEWTON:52;
then A23: a = 1 |^ d ;
b = 0 |^ d by A6, A22, NAT_1:14, NEWTON:11;
hence ex e, f being Nat st
( a = e |^ d & b = f |^ d ) by A23; :: thesis: verum

end;

hence ex e, f being Nat st
( a = e |^ d & b = f |^ d ) by A13; :: thesis: verum

end;

now :: thesis: ( a gcd c = 0 implies ex e, f being Nat st
( a = e |^ d & b = f |^ d ) )

assume a gcd c = 0 ; :: thesis: ex e, f being Nat st
( a = e |^ d & b = f |^ d )
then A24: a = 0 by INT_2:5;
then b = 1 by A1, NEWTON:52;
then A25: b = 1 |^ d ;
a = 0 |^ d by A6, A24, NAT_1:14, NEWTON:11;
hence ex e, f being Nat st
( a = e |^ d & b = f |^ d ) by A25; :: thesis: verum

end;

hence ex e, f being Nat st
( a = e |^ d & b = f |^ d ) by A9; :: thesis: verum

end;

now :: thesis: ( d = 0 implies ex e, f being Nat st
( a = e |^ d & b = f |^ d ) )

assume A26: d = 0 ; :: thesis: ex e, f being Nat st
( a = e |^ d & b = f |^ d )
then A27: a * b = 1 by A2, NEWTON:4;
then b divides 1 ;
then b = 1 by Th15;
then A28: b = 1 |^ 0 ;
a divides 1 by A27;
then a = 1 by Th15;
then a = 1 |^ 0 ;
hence ex e, f being Nat st
( a = e |^ d & b = f |^ d ) by A26, A28; :: thesis: verum

end;

hence ex e, f being Nat st
( a = e |^ d & b = f |^ d ) by A5; :: thesis: verum