let x, y, z be Element of RAT+ ; (x + y) + z = x + (y + 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 y <> {}
by Th35;
A2:
denominator z <> {}
by Th35;
then A3:
(denominator y) *^ (denominator z) <> {}
by A1, ORDINAL3:31;
A4:
denominator x <> {}
by Th35;
then A5:
(denominator x) *^ (denominator y) <> {}
by A1, ORDINAL3:31;
thus (x + y) + z =
((((numerator x) *^ (denominator y)) +^ ((denominator x) *^ (numerator y))) / ((denominator x) *^ (denominator y))) + ((numerator z) / (denominator z))
by Th39
.=
(((((numerator x) *^ (denominator y)) +^ ((denominator x) *^ (numerator y))) *^ (denominator z)) +^ (((denominator x) *^ (denominator y)) *^ (numerator z))) / (((denominator x) *^ (denominator y)) *^ (denominator z))
by A2, A5, Th46
.=
(((((numerator x) *^ (denominator y)) *^ (denominator z)) +^ (((denominator x) *^ (numerator y)) *^ (denominator z))) +^ (((denominator x) *^ (denominator y)) *^ (numerator z))) / (((denominator x) *^ (denominator y)) *^ (denominator z))
by ORDINAL3:46
.=
((((numerator x) *^ ((denominator y) *^ (denominator z))) +^ (((denominator x) *^ (numerator y)) *^ (denominator z))) +^ (((denominator x) *^ (denominator y)) *^ (numerator z))) / (((denominator x) *^ (denominator y)) *^ (denominator z))
by ORDINAL3:50
.=
((((numerator x) *^ ((denominator y) *^ (denominator z))) +^ ((denominator x) *^ ((numerator y) *^ (denominator z)))) +^ (((denominator x) *^ (denominator y)) *^ (numerator z))) / (((denominator x) *^ (denominator y)) *^ (denominator z))
by ORDINAL3:50
.=
((((numerator x) *^ ((denominator y) *^ (denominator z))) +^ ((denominator x) *^ ((numerator y) *^ (denominator z)))) +^ ((denominator x) *^ ((denominator y) *^ (numerator z)))) / (((denominator x) *^ (denominator y)) *^ (denominator z))
by ORDINAL3:50
.=
(((numerator x) *^ ((denominator y) *^ (denominator z))) +^ (((denominator x) *^ ((numerator y) *^ (denominator z))) +^ ((denominator x) *^ ((denominator y) *^ (numerator z))))) / (((denominator x) *^ (denominator y)) *^ (denominator z))
by ORDINAL3:30
.=
(((numerator x) *^ ((denominator y) *^ (denominator z))) +^ ((denominator x) *^ (((numerator y) *^ (denominator z)) +^ ((denominator y) *^ (numerator z))))) / (((denominator x) *^ (denominator y)) *^ (denominator z))
by ORDINAL3:46
.=
(((numerator x) *^ ((denominator y) *^ (denominator z))) +^ ((denominator x) *^ (((numerator y) *^ (denominator z)) +^ ((denominator y) *^ (numerator z))))) / ((denominator x) *^ ((denominator y) *^ (denominator z)))
by ORDINAL3:50
.=
((((numerator y) *^ (denominator z)) +^ ((denominator y) *^ (numerator z))) / ((denominator y) *^ (denominator z))) + ((numerator x) / (denominator x))
by A4, A3, Th46
.=
x + (y + z)
by Th39
; verum