let m, n be Element of NAT ; :: thesis: ( m * n is square & m,n are_coprime implies ( m is square & n is square ) )
defpred S1[ Nat] means for m, n being Element of NAT st m * n = \$1 & m * n is square & m,n are_coprime holds
( m is square & n is square );
A1: for mn being Nat st ( for k being Nat st k < mn holds
S1[k] ) holds
S1[mn]
proof
let mn be Nat; :: thesis: ( ( for k being Nat st k < mn holds
S1[k] ) implies S1[mn] )

assume A2: for k being Nat st k < mn holds
for m, n being Element of NAT st m * n = k & m * n is square & m,n are_coprime holds
( m is square & n is square ) ; :: thesis: S1[mn]
let m, n be Element of NAT ; :: thesis: ( m * n = mn & m * n is square & m,n are_coprime implies ( m is square & n is square ) )
assume A3: m * n = mn ; :: thesis: ( not m * n is square or not m,n are_coprime or ( m is square & n is square ) )
assume m * n is square ; :: thesis: ( not m,n are_coprime or ( m is square & n is square ) )
then consider mn9 being Nat such that
A4: mn = mn9 ^2 by A3;
assume A5: m,n are_coprime ; :: thesis: ( m is square & n is square )
then A6: m gcd n = 1 ^2 ;
per cases ( m * n = 0 or m * n = 1 ^2 or mn > 1 ) by ;
suppose A7: m * n = 0 ; :: thesis: ( m is square & n is square )
hereby :: thesis: verum
per cases ( m = 0 ^2 or n = 0 ^2 ) by ;
suppose m = 0 ^2 ; :: thesis: ( m is square & n is square )
hence ( m is square & n is square ) by ; :: thesis: verum
end;
suppose n = 0 ^2 ; :: thesis: ( m is square & n is square )
hence ( m is square & n is square ) by ; :: thesis: verum
end;
end;
end;
end;
suppose m * n = 1 ^2 ; :: thesis: ( m is square & n is square )
hence ( m is square & n is square ) by NAT_1:15; :: thesis: verum
end;
suppose A8: mn > 1 ; :: thesis: ( m is square & n is square )
then mn >= 1 + 1 by NAT_1:13;
then consider p9 being Element of NAT such that
A9: p9 is prime and
A10: p9 divides mn by INT_2:31;
reconsider p = p9 as prime Element of NAT by A9;
p divides mn9 by ;
then consider mn99 being Nat such that
A11: mn9 = p * mn99 by NAT_D:def 3;
A12: p > 1 by INT_2:def 4;
then p * p > p by XREAL_1:155;
then A13: p * p > 1 by ;
A14: n > 0 by A3, A8;
A15: p <> 0 by INT_2:def 4;
A16: m > 0 by A3, A8;
hereby :: thesis: verum
per cases ( p divides m or p divides n ) by ;
suppose A17: p divides m ; :: thesis: ( m is square & n is square )
then A18: not p divides n by A5;
consider m9 being Nat such that
A19: m = p * m9 by ;
p * (m9 * n) = p * (p * (mn99 * mn99)) by A3, A4, A11, A19;
then m9 * n = p * (mn99 * mn99) by ;
then p divides m9 * n ;
then p divides m9 by ;
then consider m99 being Nat such that
A20: m9 = p * m99 by NAT_D:def 3;
reconsider m99 = m99 as Element of NAT by ORDINAL1:def 12;
A21: m99 <> 0 by A3, A8, A19, A20;
p * (p * (m99 * n)) = p * (p * (mn99 * mn99)) by A3, A4, A11, A19, A20;
then p * (m99 * n) = p * (mn99 * mn99) by ;
then A22: m99 * n = mn99 ^2 by ;
m = (p * p) * m99 by ;
then m99 divides m ;
then m99 gcd n = 1 by ;
then A23: m99,n are_coprime ;
m = (p * p) * m99 by ;
then 1 * m99 < m by ;
then A24: m99 * n < mn by ;
then m99 is square by A2, A22, A23;
then consider m999 being Nat such that
A25: m99 = m999 ^2 ;
m = (p * m999) ^2 by ;
hence ( m is square & n is square ) by A2, A24, A22, A23; :: thesis: verum
end;
suppose A26: p divides n ; :: thesis: ( m is square & n is square )
then A27: not p divides m by A5;
consider n9 being Nat such that
A28: n = p * n9 by ;
p * (m * n9) = p * (p * (mn99 * mn99)) by A3, A4, A11, A28;
then m * n9 = p * (mn99 * mn99) by ;
then p divides m * n9 ;
then p divides n9 by ;
then consider n99 being Nat such that
A29: n9 = p * n99 by NAT_D:def 3;
reconsider n99 = n99 as Element of NAT by ORDINAL1:def 12;
A30: n99 <> 0 by A3, A8, A28, A29;
p * (p * (m * n99)) = p * (p * (mn99 * mn99)) by A3, A4, A11, A28, A29;
then p * (m * n99) = p * (mn99 * mn99) by ;
then A31: m * n99 = mn99 ^2 by ;
n = (p * p) * n99 by ;
then n99 divides n ;
then m gcd n99 = 1 by ;
then A32: m,n99 are_coprime ;
n = (p * p) * n99 by ;
then 1 * n99 < n by ;
then A33: m * n99 < mn by ;
then n99 is square by A2, A31, A32;
then consider n999 being Nat such that
A34: n99 = n999 ^2 ;
n = (p * n999) ^2 by ;
hence ( m is square & n is square ) by A2, A33, A31, A32; :: thesis: verum
end;
end;
end;
end;
end;
end;
for mn being Nat holds S1[mn] from hence ( m * n is square & m,n are_coprime implies ( m is square & n is square ) ) ; :: thesis: verum