let m, n be Element of NAT ; :: thesis: ( m * n is square & m,n are_coprime implies ( m is square & n is square ) )

defpred S_{1}[ 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

S_{1}[k] ) holds

S_{1}[mn]
_{1}[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

defpred S

( m is square & n is square );

A1: for mn being Nat st ( for k being Nat st k < mn holds

S

S

proof

for mn being Nat holds S
let mn be Nat; :: thesis: ( ( for k being Nat st k < mn holds

S_{1}[k] ) implies S_{1}[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: S_{1}[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 ;

end;S

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: S

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 A3, NAT_1:25;

end;

suppose A7:
m * n = 0
; :: thesis: ( m is square & n is square )

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;

end;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
end;

per cases
( p divides m or p divides n )
by A3, A10, NEWTON:80;

end;

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;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

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;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

hence ( m * n is square & m,n are_coprime implies ( m is square & n is square ) ) ; :: thesis: verum