let p be Rational; :: thesis: ex m being Integer ex k being Element of NAT st
( k <> 0 & p = m / k & ( for n being Integer
for l being Element of NAT st l <> 0 & p = n / l holds
k <= l ) )
defpred S₁[ Nat] means ( $1 <> 0 & ex m1 being Integer st p = m1 / $1 );
consider m being Integer, k being Element of NAT such that
A1: ( k <> 0 & p = m / k ) by Th24;
A2: ex l being Nat st S₁[l] by A1;
ex k1 being Nat st
( S₁[k1] & ( for l1 being Nat st S₁[l1] holds
k1 <= l1 ) ) from NAT_1:sch 5(A2);
then consider k1 being Nat such that
A3: ( k1 <> 0 & ex m1 being Integer st p = m1 / k1 & ( for l1 being Nat st l1 <> 0 & ex n1 being Integer st p = n1 / l1 holds
k1 <= l1 ) ) ;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 13;
consider m1 being Integer such that
A4: ( p = m1 / k1 & ( for l1 being Nat st l1 <> 0 & ex n1 being Integer st p = n1 / l1 holds
k1 <= l1 ) ) by A3;
take m1 ; :: thesis: ex k being Element of NAT st
( k <> 0 & p = m1 / k & ( for n being Integer
for l being Element of NAT st l <> 0 & p = n / l holds
k <= l ) )
take k1 ; :: thesis: ( k1 <> 0 & p = m1 / k1 & ( for n being Integer
for l being Element of NAT st l <> 0 & p = n / l holds
k1 <= l ) )
thus k1 <> 0 by A3; :: thesis: ( p = m1 / k1 & ( for n being Integer
for l being Element of NAT st l <> 0 & p = n / l holds
k1 <= l ) )
thus m1 / k1 = p by A4; :: thesis: for n being Integer
for l being Element of NAT st l <> 0 & p = n / l holds
k1 <= l
thus for n being Integer
for l being Element of NAT st l <> 0 & p = n / l holds
k1 <= l by A4; :: thesis: verum
thus verum ; :: thesis: verum