let m, n be Element of NAT ; :: thesis: ( m * n is square & m,n are_relative_prime 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_relative_prime 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_relative_prime 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_relative_prime implies ( m is square & n is square ) )
assume A3: m * n = mn ; :: thesis: ( not m * n is square or not m,n are_relative_prime or ( m is square & n is square ) )
assume m * n is square ; :: thesis: ( not m,n are_relative_prime or ( m is square & n is square ) )
then consider mn' being Nat such that
A4: mn = mn' ^2 by A3, Def3;
assume A5: m,n are_relative_prime ; :: thesis: ( m is square & n is square )
then A6: m gcd n = 1 ^2 by INT_2:def 4;
per cases ( m * n = 0 or m * n = 1 ^2 or mn > 1 ) by A3, NAT_1:26;
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 p' being Element of NAT such that
A9: p' is prime and
A10: p' divides mn by INT_2:48;
reconsider p = p' as prime Element of NAT by A9;
p divides mn' by A4, A10, NEWTON:98;
then consider mn'' being Nat such that
A11: mn' = p * mn'' by NAT_D:def 3;
A12: p > 1 by INT_2:def 5;
then p * p > p by XREAL_1:157;
then A13: p * p > 1 by A12, XXREAL_0:2;
A14: n > 0 by A3, A8;
A15: p <> 0 by INT_2:def 5;
A16: m > 0 by A3, A8;
hereby :: thesis: verum
per cases ( p divides m or p divides n ) by A3, A10, NEWTON:98;
suppose A17: p divides m ; :: thesis: ( m is square & n is square )
then A18: not p divides n by A5, Def2;
consider m' being Nat such that
A19: m = p * m' by A17, NAT_D:def 3;
p * (m' * n) = p * (p * (mn'' * mn'')) by A3, A4, A11, A19;
then m' * n = p * (mn'' * mn'') by A15, XCMPLX_1:5;
then p divides m' * n by NAT_D:def 3;
then p divides m' by A18, NEWTON:98;
then consider m'' being Nat such that
A20: m' = p * m'' by NAT_D:def 3;
reconsider m'' = m'' as Element of NAT by ORDINAL1:def 13;
A21: m'' <> 0 by A3, A8, A19, A20;
p * (p * (m'' * n)) = p * (p * (mn'' * mn'')) by A3, A4, A11, A19, A20;
then p * (m'' * n) = p * (mn'' * mn'') by A15, XCMPLX_1:5;
then A22: m'' * n = mn'' ^2 by A15, XCMPLX_1:5;
m = (p * p) * m'' by A19, A20;
then m'' divides m by NAT_D:def 3;
then m'' gcd n = 1 by A6, WSIERP_1:21;
then A23: m'',n are_relative_prime by INT_2:def 4;
m = (p * p) * m'' by A19, A20;
then 1 * m'' < m by A13, A21, XREAL_1:100;
then A24: m'' * n < mn by A3, A14, A21, XREAL_1:100;
then m'' is square by A2, A22, A23;
then consider m''' being Nat such that
A25: m'' = m''' ^2 by Def3;
m = (p * m''') ^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, Def2;
consider n' being Nat such that
A28: n = p * n' by A26, NAT_D:def 3;
p * (m * n') = p * (p * (mn'' * mn'')) by A3, A4, A11, A28;
then m * n' = p * (mn'' * mn'') by A15, XCMPLX_1:5;
then p divides m * n' by NAT_D:def 3;
then p divides n' by A27, NEWTON:98;
then consider n'' being Nat such that
A29: n' = p * n'' by NAT_D:def 3;
reconsider n'' = n'' as Element of NAT by ORDINAL1:def 13;
A30: n'' <> 0 by A3, A8, A28, A29;
p * (p * (m * n'')) = p * (p * (mn'' * mn'')) by A3, A4, A11, A28, A29;
then p * (m * n'') = p * (mn'' * mn'') by A15, XCMPLX_1:5;
then A31: m * n'' = mn'' ^2 by A15, XCMPLX_1:5;
n = (p * p) * n'' by A28, A29;
then n'' divides n by NAT_D:def 3;
then m gcd n'' = 1 by A6, WSIERP_1:21;
then A32: m,n'' are_relative_prime by INT_2:def 4;
n = (p * p) * n'' by A28, A29;
then 1 * n'' < n by A13, A30, XREAL_1:100;
then A33: m * n'' < mn by A3, A16, A30, XREAL_1:100;
then n'' is square by A2, A31, A32;
then consider n''' being Nat such that
A34: n'' = n''' ^2 by Def3;
n = (p * n''') ^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_relative_prime implies ( m is square & n is square ) ) ; :: thesis: verum