let m, n be 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 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 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 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 A3, NAT_1:25;
suppose A7: m * n = 0 ; :: thesis: ( m is square & n is square )
hereby :: thesis: verum
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 A4, A10, NEWTON:80;
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 A12, XXREAL_0:2;
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 A3, A10, NEWTON:80;
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 A17, NAT_D:def 3;
p * (m9 * n) = p * (p * (mn99 * mn99)) by A3, A4, A11, A19;
then m9 * n = p * (mn99 * mn99) by A15, XCMPLX_1:5;
then p divides m9 * n ;
then p divides m9 by A18, NEWTON:80;
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 A15, XCMPLX_1:5;
then A22: m99 * n = mn99 ^2 by A15, XCMPLX_1:5;
m = (p * p) * m99 by A19, A20;
then m99 divides m ;
then m99 gcd n = 1 by A6, WSIERP_1:16;
then A23: m99,n are_coprime ;
m = (p * p) * m99 by A19, A20;
then 1 * m99 < m by A13, A21, XREAL_1:98;
then A24: m99 * n < mn by A3, A14, A21, XREAL_1:98;
then m99 is square by A2, A22, A23;
then consider m999 being Nat such that
A25: m99 = m999 ^2 ;
m = (p * m999) ^2 by A19, A20, A25;
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 A26, NAT_D:def 3;
p * (m * n9) = p * (p * (mn99 * mn99)) by A3, A4, A11, A28;
then m * n9 = p * (mn99 * mn99) by A15, XCMPLX_1:5;
then p divides m * n9 ;
then p divides n9 by A27, NEWTON:80;
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 A15, XCMPLX_1:5;
then A31: m * n99 = mn99 ^2 by A15, XCMPLX_1:5;
n = (p * p) * n99 by A28, A29;
then n99 divides n ;
then m gcd n99 = 1 by A6, WSIERP_1:16;
then A32: m,n99 are_coprime ;
n = (p * p) * n99 by A28, A29;
then 1 * n99 < n by A13, A30, XREAL_1:98;
then A33: m * n99 < mn by A3, A16, A30, XREAL_1:98;
then n99 is square by A2, A31, A32;
then consider n999 being Nat such that
A34: n99 = n999 ^2 ;
n = (p * n999) ^2 by A28, A29, A34;
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 NAT_1:sch 4(A1);
 hence ( m * n is square & m,n are_coprime implies ( m is square & n is square ) ) ; :: thesis: verum