let m, n be Element of NAT ; :: thesis: ( m divides n iff m ^2 divides n ^2 )
defpred S₁[ 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₁[k] ) holds
S₁[m]

proof

let m be Nat; :: thesis: ( ( for k being Nat st k < m holds
S₁[k] ) implies S₁[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₁[m]
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 m divides n ; :: thesis: m ^2 divides n ^2
then consider k' being Nat such that
A3: n = m * k' by NAT_D:def 3;
n ^2 = (m ^2 ) * (k' ^2 ) by A3;
hence m ^2 divides n ^2 by NAT_D:def 3; :: thesis: verum

end;

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

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

suppose m = 0 ; :: thesis: m divides n

then n ^2 = 0 by A4, INT_2:3;
then n = 0 by XCMPLX_1:6;
hence m divides n by NAT_D:6; :: thesis: verum

end;

suppose m = 1 ; :: thesis: m divides n

hence m divides n by NAT_D:6; :: thesis: verum

end;

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

consider k' being Nat such that
A6: n ^2 = (m ^2 ) * k' by A4, NAT_D:def 3;
m >= 1 + 1 by A5, NAT_1:13;
then consider p' being Element of NAT such that
A7: p' is prime and
A8: p' divides m by INT_2:48;
reconsider p = p' as prime Element of NAT by A7;
consider m' being Nat such that
A9: m = p * m' by A8, NAT_D:def 3;
reconsider m' = m' as Element of NAT by ORDINAL1:def 13;
m ^2 = (m * m') * p by A9;
then p divides m ^2 by NAT_D:def 3;
then p divides n ^2 by A4, NAT_D:4;
then p divides n by NEWTON:98;
then consider n' being Nat such that
A10: n = p * n' by NAT_D:def 3;
A11: p > 1 by INT_2:def 5;
then A12: p ^2 > 0 by SQUARE_1:74;
reconsider n' = n' as Element of NAT by ORDINAL1:def 13;
(p ^2 ) * (n' ^2 ) = (p ^2 ) * ((m' ^2 ) * k') by A9, A10, A6;
then n' ^2 = (m' ^2 ) * k' by A12, XCMPLX_1:5;
then A13: m' ^2 divides n' ^2 by NAT_D:def 3;
p * m' > 1 * m' by A5, A9, A11, XREAL_1:100;
then m' divides n' by A2, A9, A13;
then consider k being Nat such that
A14: n' = m' * k by NAT_D:def 3;
n = m * k by A9, A10, A14;
hence m divides n by NAT_D:def 3; :: thesis: verum

end;

end;

end;

for m being Nat holds S₁[m] from NAT_1:sch 4(A1);
hence ( m divides n iff m ^2 divides n ^2 ) ; :: thesis: verum