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

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

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

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

then n ^2 = 0 by A4;
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 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;

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