let x, y be Element of RAT+ ; ( x in omega & x + y in omega implies y in omega )
assume that
A1:
x in omega
and
A2:
x + y in omega
; y in omega
A3:
denominator (x + y) = 1
by A2, Def9;
set nx = numerator x;
set dx = denominator x;
A4:
denominator x = 1
by A1, Def9;
set ny = numerator y;
set dy = denominator y;
A5:
( x + y = (numerator (x + y)) / (denominator (x + y)) & (((numerator x) *^ (denominator y)) +^ ((numerator y) *^ (denominator x))) *^ 1 = ((numerator x) *^ (denominator y)) +^ ((numerator y) *^ (denominator x)) )
by Th39, ORDINAL2:39;
denominator y <> {}
by Th35;
then
(denominator x) *^ (denominator y) <> {}
by A4, ORDINAL3:31, Lm4;
then ((numerator x) *^ (denominator y)) +^ ((numerator y) *^ (denominator x)) =
((denominator x) *^ (denominator y)) *^ (numerator (x + y))
by A3, A5, Th45, Lm4
.=
(denominator y) *^ (numerator (x + y))
by A4, ORDINAL2:39
;
then
((numerator x) *^ (denominator y)) +^ (numerator y) = (denominator y) *^ (numerator (x + y))
by A4, ORDINAL2:39;
then
numerator y = ((denominator y) *^ (numerator (x + y))) -^ ((numerator x) *^ (denominator y))
by ORDINAL3:52;
then
numerator y = (denominator y) *^ ((numerator (x + y)) -^ (numerator x))
by ORDINAL3:63;
then A6:
denominator y divides numerator y
;
A7:
numerator y, denominator y are_coprime
by Th34;
for m being natural Ordinal st m divides denominator y & m divides numerator y holds
m divides denominator y
;
then
(denominator y) hcf (numerator y) = denominator y
by A6, Def5;
then A8:
denominator y = 1
by A7, Th20;
y = (numerator y) / (denominator y)
by Th39;
then
y = numerator y
by A8, Th40;
hence
y in omega
; verum