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 A1: ( a gcd b = 1 & a * b = c |^ d ) ; :: thesis: ex e, f being Nat st
( a = e |^ d & b = f |^ d )
set e = a gcd c;
A2: ( a gcd c divides c & a gcd c divides a ) by NAT_D:def 5;
then A3: (a gcd c) |^ d divides c |^ d by Th19;
(a gcd c) gcd b = 1 by A1, A2, Th20, NEWTON:70;
then ((a gcd c) |^ d) gcd b = 1 by Th17;
then (a gcd c) |^ d divides a by A1, A3, Th36;
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 13;

A5: now

assume A6: d = 0 ; :: thesis: ex e, f being Nat st
( a = e |^ d & b = f |^ d )
then a * b = 1 by A1, NEWTON:9;
then ( a divides 1 & b divides 1 ) by NAT_D:def 3;
then ( a = 1 & b = 1 ) by Th20;
then ( a = 1 |^ 0 & b = 1 |^ 0 ) by NEWTON:9;
hence ex e, f being Nat st
( a = e |^ d & b = f |^ d ) by A6; :: thesis: verum

end;

now

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

A10: now

assume a gcd c = 0 ; :: thesis: ex e, f being Nat st
( a = e |^ d & b = f |^ d )
then A11: ( a = 0 & 0 = c ) by INT_2:5;
then b = 1 by A1, NEWTON:65;
then A12: b = 1 |^ d by NEWTON:15;
a = 0 |^ d by A7, A11, NAT_1:14, NEWTON:16;
hence ex e, f being Nat st
( a = e |^ d & b = f |^ d ) by A12; :: thesis: verum

end;

X: c in REAL by XREAL_0:def 1;

now

assume A13: a gcd c <> 0 ; :: thesis: ex e, f being Nat st
( a = e |^ d & b = f |^ d )
then A14: ( a <> 0 or c <> 0 ) by INT_2:5;
then A15: a <> 0 by A1, X, CARD_4:51;

A16: now

assume 0 = c ; :: thesis: ex e, f being Nat st
( a = e |^ d & b = f |^ d )
then A17: b = 0 by A1, A8, A14, NEWTON:16, XCMPLX_1:6;
then a = 1 by A1, NEWTON:65;
then A18: a = 1 |^ d by NEWTON:15;
b = 0 |^ d by A7, A17, NAT_1:14, NEWTON:16;
hence ex e, f being Nat st
( a = e |^ d & b = f |^ d ) by A18; :: thesis: verum

end;

now

assume A19: c <> 0 ; :: thesis: ex e, f being Nat st
( a = e |^ d & b = f |^ d )
reconsider e1 = a gcd c as Real by XREAL_0:def 1;
A20: e1 |^ d <> 0 by A13, CARD_4:51;
consider a1, c1 being Integer such that
A21: ( a = (a gcd c) * a1 & (a gcd c) * c1 = c & a1,c1 are_relative_prime ) by A19, INT_2:38;
reconsider a1 = a1, c1 = c1 as Element of NAT by A15, A19, A21, Lm6;
A22: ( a1 = a / (a gcd c) & c1 = c / (a gcd c) ) by A13, A21, XCMPLX_1:90;
A23: a1 gcd c1 = 1 by A21, INT_2:def 4;
a1 = (((a gcd c) |^ (d1 + 1)) * g) / (a gcd c) by A4, A9, A13, A21, XCMPLX_1:90
.= (((a gcd c) * ((a gcd c) |^ d1)) * g) / (a gcd c) by NEWTON:11
.= ((a gcd c) * (((a gcd c) |^ d1) * g)) / (a gcd c)
.= ((a gcd c) |^ d1) * g by A13, XCMPLX_1:90 ;
then g divides a1 by NAT_D:def 3;
then g gcd c1 = 1 by A23, Th20, NEWTON:70;
then A24: g gcd (c1 |^ d) = 1 by Th17;
A25: c1 |^ d = (((a gcd c) |^ d) * (g * b)) / ((a gcd c) |^ d) by A1, A4, A22, PREPOWER:15
.= g * b by A20, XCMPLX_1:90 ;
then g divides c1 |^ d by NAT_D:def 3;
then g = 1 by A24, NEWTON:62;
hence ex e, f being Nat st
( a = e |^ d & b = f |^ d ) by A4, A25; :: thesis: verum

end;

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

end;

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

end;

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