let p be Nat; ( ex n being Element of NAT st
( n divides p & 1 < n & n < p ) implies ex n being Element of NAT st
( n divides p & 1 < n & n * n <= p ) )
given n being Element of NAT such that A1:
n divides p
and
A2:
1 < n
and
A3:
n < p
; ex n being Element of NAT st
( n divides p & 1 < n & n * n <= p )
per cases
( n * n <= p or n * n > p )
;
suppose A5:
n * n > p
;
ex n being Element of NAT st
( n divides p & 1 < n & n * n <= p )consider k being
Nat such that A6:
p = n * k
by A1, NAT_D:def 3;
A7:
k * k <= p
take
k
;
( k is Element of NAT & k divides p & 1 < k & k * k <= p )
n / n < (n * k) / n
by A2, A3, A6, XREAL_1:74;
then
1
< (k * n) / n
by A2, XCMPLX_1:60;
hence
(
k is
Element of
NAT &
k divides p & 1
< k &
k * k <= p )
by A2, A6, A7, NAT_D:def 3, ORDINAL1:def 12, XCMPLX_1:89;
verum end; end;