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 Th19;
a gcd c divides a by NAT_D:def 5;
then (a gcd c) gcd b = 1 by A1, Th20, NEWTON:70;
then ((a gcd c) |^ d) gcd b = 1 by Th17;
then (a gcd c) |^ d divides a by A2, 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

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

A10: now

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

A14: now

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

end;

now

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

end;

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

end;

now

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

end;

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

end;

now

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

end;

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