let x, y, z be Element of RAT+ ; x *' (y + z) = (x *' y) + (x *' z)
set nx = numerator x;
set ny = numerator y;
set nz = numerator z;
set dx = denominator x;
set dy = denominator y;
set dz = denominator z;
A1:
denominator x <> {}
by Th35;
denominator z <> {}
by Th35;
then A2:
(denominator x) *^ (denominator z) <> {}
by A1, ORDINAL3:31;
denominator y <> {}
by Th35;
then A3:
(denominator x) *^ (denominator y) <> {}
by A1, ORDINAL3:31;
x = (numerator x) / (denominator x)
by Th39;
hence x *' (y + z) =
((numerator x) *^ (((numerator y) *^ (denominator z)) +^ ((denominator y) *^ (numerator z)))) / ((denominator x) *^ ((denominator y) *^ (denominator z)))
by Th49
.=
(((numerator x) *^ ((numerator y) *^ (denominator z))) +^ ((numerator x) *^ ((denominator y) *^ (numerator z)))) / ((denominator x) *^ ((denominator y) *^ (denominator z)))
by ORDINAL3:46
.=
((((numerator x) *^ (numerator y)) *^ (denominator z)) +^ ((numerator x) *^ ((denominator y) *^ (numerator z)))) / ((denominator x) *^ ((denominator y) *^ (denominator z)))
by ORDINAL3:50
.=
((((numerator x) *^ (numerator y)) *^ (denominator z)) +^ ((denominator y) *^ ((numerator x) *^ (numerator z)))) / ((denominator x) *^ ((denominator y) *^ (denominator z)))
by ORDINAL3:50
.=
((((numerator x) *^ (numerator y)) *^ (denominator z)) +^ ((denominator y) *^ ((numerator x) *^ (numerator z)))) / ((denominator y) *^ ((denominator x) *^ (denominator z)))
by ORDINAL3:50
.=
((denominator x) *^ ((((numerator x) *^ (numerator y)) *^ (denominator z)) +^ ((denominator y) *^ ((numerator x) *^ (numerator z))))) / ((denominator x) *^ ((denominator y) *^ ((denominator x) *^ (denominator z))))
by Th35, Th44
.=
(((denominator x) *^ (((numerator x) *^ (numerator y)) *^ (denominator z))) +^ ((denominator x) *^ ((denominator y) *^ ((numerator x) *^ (numerator z))))) / ((denominator x) *^ ((denominator y) *^ ((denominator x) *^ (denominator z))))
by ORDINAL3:46
.=
(((denominator x) *^ (((numerator x) *^ (numerator y)) *^ (denominator z))) +^ (((denominator x) *^ (denominator y)) *^ ((numerator x) *^ (numerator z)))) / ((denominator x) *^ ((denominator y) *^ ((denominator x) *^ (denominator z))))
by ORDINAL3:50
.=
((((numerator x) *^ (numerator y)) *^ ((denominator x) *^ (denominator z))) +^ (((denominator x) *^ (denominator y)) *^ ((numerator x) *^ (numerator z)))) / ((denominator x) *^ ((denominator y) *^ ((denominator x) *^ (denominator z))))
by ORDINAL3:50
.=
((((numerator x) *^ (numerator y)) *^ ((denominator x) *^ (denominator z))) +^ (((denominator x) *^ (denominator y)) *^ ((numerator x) *^ (numerator z)))) / (((denominator x) *^ (denominator y)) *^ ((denominator x) *^ (denominator z)))
by ORDINAL3:50
.=
(x *' y) + (x *' z)
by A2, A3, Th46
;
verum