let m, n be Element of NAT ; :: thesis: ( m divides n iff m ^2 divides n ^2 )
defpred S1[ 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
S1[k] ) holds
S1[m]
proof
let m be Nat; :: thesis: ( ( for k being Nat st k < m holds
S1[k] ) implies S1[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: S1[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:
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 A5: m > 1 ; :: thesis: m divides n
consider k9 being Nat such that
A6: n ^2 = (m ^2) * k9 by ;
m >= 1 + 1 by ;
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 ;
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 ;
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 ;
then A13: m9 ^2 divides n9 ^2 ;
p * m9 > 1 * m9 by ;
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 S1[m] from hence ( m divides n iff m ^2 divides n ^2 ) ; :: thesis: verum