let a, b, c, n be Nat; :: thesis: ( a,b are_coprime & a * b = c |^ n implies ex k being Nat st k |^ n = a )

assume A1: ( a,b are_coprime & a * b = c |^ n ) ; :: thesis: ex k being Nat st k |^ n = a

consider k being Nat such that

A3: k = a gcd c ;

assume A1: ( a,b are_coprime & a * b = c |^ n ) ; :: thesis: ex k being Nat st k |^ n = a

consider k being Nat such that

A3: k = a gcd c ;

per cases
( n = 0 or ( n > 0 & a = 0 ) or b = 0 or ( n > 0 & a > 0 & b > 0 ) )
;

end;

suppose B1:
n = 0
; :: thesis: ex k being Nat st k |^ n = a

then
a = 1 |^ 0
by A1, NAT_1:15, NEWTON:4;

hence ex k being Nat st k |^ n = a by B1; :: thesis: verum

end;hence ex k being Nat st k |^ n = a by B1; :: thesis: verum

suppose B1:
( n > 0 & a > 0 & b > 0 )
; :: thesis: ex k being Nat st k |^ n = a

then consider m being Nat such that

B2: n = 1 + m by NAT_1:10, NAT_1:14;

B3: a |^ m,b are_coprime by A1, WSIERP_1:10;

k |^ n = (a |^ n) gcd (c |^ n) by A3, Th7

.= ((a |^ m) * a) gcd (a * b) by A1, B2, NEWTON:6

.= a * 1 by B3, B1, EULER_1:15 ;

hence ex k being Nat st k |^ n = a ; :: thesis: verum

end;B2: n = 1 + m by NAT_1:10, NAT_1:14;

B3: a |^ m,b are_coprime by A1, WSIERP_1:10;

k |^ n = (a |^ n) gcd (c |^ n) by A3, Th7

.= ((a |^ m) * a) gcd (a * b) by A1, B2, NEWTON:6

.= a * 1 by B3, B1, EULER_1:15 ;

hence ex k being Nat st k |^ n = a ; :: thesis: verum