let r, t be Element of RAT+ ; :: thesis: ( t <> {} implies ex s being Element of RAT+ st
( s in omega & r <=' s *' t ) )
set y = ((numerator r) *^ (((numerator t) *^ (denominator r)) -^ 1)) / (denominator r);
A1: denominator r <> {} by Th35;
(denominator t) *^ (numerator r) in omega by ORDINAL1:def 12;
then reconsider s = (denominator t) *^ (numerator r) as ordinal Element of RAT+ by Lm6;
assume t <> {} ; :: thesis: ex s being Element of RAT+ st
( s in omega & r <=' s *' t )
then numerator t <> {} by Th37;
then {} in (numerator t) *^ (denominator r) by A1, ORDINAL3:8, ORDINAL3:31;
then one c= (numerator t) *^ (denominator r) by Lm3, ORDINAL1:21;
then (numerator t) *^ (denominator r) = 1 +^ (((numerator t) *^ (denominator r)) -^ 1) by ORDINAL3:def 5;
then s *^ ((numerator t) *^ (denominator r)) = (denominator t) *^ ((numerator r) *^ (1 +^ (((numerator t) *^ (denominator r)) -^ 1))) by ORDINAL3:50
.= (denominator t) *^ (((numerator r) *^ 1) +^ ((numerator r) *^ (((numerator t) *^ (denominator r)) -^ 1))) by ORDINAL3:46 ;
then A2: (s *^ (numerator t)) *^ (denominator r) = (denominator t) *^ (((numerator r) *^ 1) +^ ((numerator r) *^ (((numerator t) *^ (denominator r)) -^ 1))) by ORDINAL3:50;
take s ; :: thesis: ( s in omega & r <=' s *' t )
thus s in omega by ORDINAL1:def 12; :: thesis: r <=' s *' t
take ((numerator r) *^ (((numerator t) *^ (denominator r)) -^ 1)) / (denominator r) ; :: according to ARYTM_3:def 13 :: thesis: s *' t = r + (((numerator r) *^ (((numerator t) *^ (denominator r)) -^ 1)) / (denominator r))
denominator t <> {} by Th35;
then (s *^ (numerator t)) / (denominator t) = (((numerator r) *^ 1) +^ ((numerator r) *^ (((numerator t) *^ (denominator r)) -^ 1))) / (denominator r) by A1, A2, Th45
.= (((numerator r) *^ 1) / (denominator r)) + (((numerator r) *^ (((numerator t) *^ (denominator r)) -^ 1)) / (denominator r)) by Th35, Th47
.= ((numerator r) / (denominator r)) + (((numerator r) *^ (((numerator t) *^ (denominator r)) -^ 1)) / (denominator r)) by ORDINAL2:39
.= r + (((numerator r) *^ (((numerator t) *^ (denominator r)) -^ 1)) / (denominator r)) by Th39 ;
then r + (((numerator r) *^ (((numerator t) *^ (denominator r)) -^ 1)) / (denominator r)) = (s *^ (numerator t)) / (1 *^ (denominator t)) by ORDINAL2:39
.= (s / 1) *' ((numerator t) / (denominator t)) by Th49
.= s *' ((numerator t) / (denominator t)) by Th40 ;
hence s *' t = r + (((numerator r) *^ (((numerator t) *^ (denominator r)) -^ 1)) / (denominator r)) by Th39; :: thesis: verum