let m, n be Element of NAT ; :: thesis: ( m divides n iff m ^2 divides n ^2 )

defpred S_{1}[ Nat] means for n being Element of NAT holds

( $1 divides n iff $1 ^2 divides n ^2 );

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

S_{1}[k] ) holds

S_{1}[m]
_{1}[m]
from NAT_1:sch 4(A1);

hence ( m divides n iff m ^2 divides n ^2 ) ; :: thesis: verum

defpred S

( $1 divides n iff $1 ^2 divides n ^2 );

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

S

S

proof

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

S_{1}[k] ) implies S_{1}[m] )

assume A2: for k being Nat st k < m holds

for n being Element of NAT holds

( k divides n iff k ^2 divides n ^2 ) ; :: thesis: S_{1}[m]

let n be Element of NAT ; :: thesis: ( m divides n iff m ^2 divides n ^2 )

end;S

assume A2: for k being Nat st k < m holds

for n being Element of NAT holds

( k divides n iff k ^2 divides n ^2 ) ; :: thesis: S

let n be Element of NAT ; :: thesis: ( m divides n iff m ^2 divides n ^2 )

hereby :: thesis: ( m ^2 divides n ^2 implies m divides n )

assume A4:
m ^2 divides n ^2
; :: thesis: m divides nassume
m divides n
; :: thesis: m ^2 divides n ^2

then consider k9 being Nat such that

A3: n = m * k9 by NAT_D:def 3;

n ^2 = (m ^2) * (k9 ^2) by A3;

hence m ^2 divides n ^2 ; :: thesis: verum

end;then consider k9 being Nat such that

A3: n = m * k9 by NAT_D:def 3;

n ^2 = (m ^2) * (k9 ^2) by A3;

hence m ^2 divides n ^2 ; :: thesis: verum

per cases
( m = 0 or m = 1 or m > 1 )
by NAT_1:25;

end;

suppose A5:
m > 1
; :: thesis: m divides n

consider k9 being Nat such that

A6: n ^2 = (m ^2) * k9 by A4, NAT_D:def 3;

m >= 1 + 1 by A5, NAT_1:13;

then consider p9 being Element of NAT such that

A7: p9 is prime and

A8: p9 divides m by INT_2:31;

reconsider p = p9 as prime Element of NAT by A7;

consider m9 being Nat such that

A9: m = p * m9 by A8, NAT_D:def 3;

reconsider m9 = m9 as Element of NAT by ORDINAL1:def 12;

m ^2 = (m * m9) * p by A9;

then p divides m ^2 ;

then p divides n ^2 by A4, NAT_D:4;

then p divides n by NEWTON:80;

then consider n9 being Nat such that

A10: n = p * n9 by NAT_D:def 3;

A11: p > 1 by INT_2:def 4;

then A12: p ^2 > 0 by SQUARE_1:12;

reconsider n9 = n9 as Element of NAT by ORDINAL1:def 12;

(p ^2) * (n9 ^2) = (p ^2) * ((m9 ^2) * k9) by A9, A10, A6;

then n9 ^2 = (m9 ^2) * k9 by A12, XCMPLX_1:5;

then A13: m9 ^2 divides n9 ^2 ;

p * m9 > 1 * m9 by A5, A9, A11, XREAL_1:98;

then m9 divides n9 by A2, A9, A13;

then consider k being Nat such that

A14: n9 = m9 * k by NAT_D:def 3;

n = m * k by A9, A10, A14;

hence m divides n ; :: thesis: verum

end;A6: n ^2 = (m ^2) * k9 by A4, NAT_D:def 3;

m >= 1 + 1 by A5, NAT_1:13;

then consider p9 being Element of NAT such that

A7: p9 is prime and

A8: p9 divides m by INT_2:31;

reconsider p = p9 as prime Element of NAT by A7;

consider m9 being Nat such that

A9: m = p * m9 by A8, NAT_D:def 3;

reconsider m9 = m9 as Element of NAT by ORDINAL1:def 12;

m ^2 = (m * m9) * p by A9;

then p divides m ^2 ;

then p divides n ^2 by A4, NAT_D:4;

then p divides n by NEWTON:80;

then consider n9 being Nat such that

A10: n = p * n9 by NAT_D:def 3;

A11: p > 1 by INT_2:def 4;

then A12: p ^2 > 0 by SQUARE_1:12;

reconsider n9 = n9 as Element of NAT by ORDINAL1:def 12;

(p ^2) * (n9 ^2) = (p ^2) * ((m9 ^2) * k9) by A9, A10, A6;

then n9 ^2 = (m9 ^2) * k9 by A12, XCMPLX_1:5;

then A13: m9 ^2 divides n9 ^2 ;

p * m9 > 1 * m9 by A5, A9, A11, XREAL_1:98;

then m9 divides n9 by A2, A9, A13;

then consider k being Nat such that

A14: n9 = m9 * k by NAT_D:def 3;

n = m * k by A9, A10, A14;

hence m divides n ; :: thesis: verum

hence ( m divides n iff m ^2 divides n ^2 ) ; :: thesis: verum