let x, y, z be Element of REAL ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A1: ( x in REAL+ \/ [:{0},REAL+:] & y in REAL+ \/ [:{0},REAL+:] ) by XBOOLE_0:def 5;
A2: z in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 5;
per cases ( ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in REAL+ & y in REAL+ & z in [:{0},REAL+:] ) or ( x in REAL+ & y in [:{0},REAL+:] & z in REAL+ ) or ( x in REAL+ & y in [:{0},REAL+:] & z in [:{0},REAL+:] ) or ( z in REAL+ & y in REAL+ & x in [:{0},REAL+:] ) or ( x in [:{0},REAL+:] & y in REAL+ & z in [:{0},REAL+:] ) or ( z in REAL+ & y in [:{0},REAL+:] & x in [:{0},REAL+:] ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & z in [:{0},REAL+:] ) ) by A1, A2, XBOOLE_0:def 3;
suppose that A3: x in REAL+ and
A4: y in REAL+ and
A5: z in REAL+ ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A6: ex x99, y99 being Element of REAL+ st
( x = x99 & y = y99 & + (x,y) = x99 + y99 ) by A3, A4, Def1;
then A7: ex xy99, z99 being Element of REAL+ st
( + (x,y) = xy99 & z = z99 & + ((+ (x,y)),z) = xy99 + z99 ) by A5, Def1;
A8: ex y9, z9 being Element of REAL+ st
( y = y9 & z = z9 & + (y,z) = y9 + z9 ) by A4, A5, Def1;
then ex x9, yz9 being Element of REAL+ st
( x = x9 & + (y,z) = yz9 & + (x,(+ (y,z))) = x9 + yz9 ) by A3, Def1;
hence + (x,(+ (y,z))) = + ((+ (x,y)),z) by A8, A6, A7, ARYTM_2:6; :: thesis: verum
end;
suppose that A9: x in REAL+ and
A10: y in REAL+ and
A11: z in [:{0},REAL+:] ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A12: ex x99, y99 being Element of REAL+ st
( x = x99 & y = y99 & + (x,y) = x99 + y99 ) by A9, A10, Def1;
then consider xy99, z99 being Element of REAL+ such that
A13: + (x,y) = xy99 and
A14: z = [0,z99] and
A15: + ((+ (x,y)),z) = xy99 - z99 by A11, Def1;
consider y9, z9 being Element of REAL+ such that
A16: y = y9 and
A17: z = [0,z9] and
A18: + (y,z) = y9 - z9 by A10, A11, Def1;
A19: z9 = z99 by A17, A14, XTUPLE_0:1;
now :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
per cases ( z9 <=' y9 or not z9 <=' y9 ) ;
suppose A20: z9 <=' y9 ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
then A21: + (y,z) = y9 -' z9 by A18, ARYTM_1:def 2;
then ex x9, yz9 being Element of REAL+ st
( x = x9 & + (y,z) = yz9 & + (x,(+ (y,z))) = x9 + yz9 ) by A9, Def1;
hence + (x,(+ (y,z))) = + ((+ (x,y)),z) by A16, A12, A13, A15, A19, A20, A21, ARYTM_1:20; :: thesis: verum
end;
suppose A22: not z9 <=' y9 ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
then A23: + (y,z) = [0,(z9 -' y9)] by A18, ARYTM_1:def 2;
then + (y,z) in [:{0},REAL+:] by Lm1;
then consider x9, yz9 being Element of REAL+ such that
A24: x = x9 and
A25: ( + (y,z) = [0,yz9] & + (x,(+ (y,z))) = x9 - yz9 ) by A9, Def1;
thus + (x,(+ (y,z))) = x9 - (z9 -' y9) by A23, A25, XTUPLE_0:1
.= + ((+ (x,y)),z) by A16, A12, A13, A15, A19, A22, A24, ARYTM_1:21 ; :: thesis: verum
end;
end;
end;
hence + (x,(+ (y,z))) = + ((+ (x,y)),z) ; :: thesis: verum
end;
suppose that A26: x in REAL+ and
A27: y in [:{0},REAL+:] and
A28: z in REAL+ ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
consider x99, y99 being Element of REAL+ such that
A29: x = x99 and
A30: y = [0,y99] and
A31: + (x,y) = x99 - y99 by A26, A27, Def1;
consider z9, y9 being Element of REAL+ such that
A32: z = z9 and
A33: y = [0,y9] and
A34: + (y,z) = z9 - y9 by A27, A28, Def1;
A35: y9 = y99 by A33, A30, XTUPLE_0:1;
now :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
per cases ( ( y9 <=' x99 & y9 <=' z9 ) or ( y9 <=' x99 & not y9 <=' z9 ) or ( not y9 <=' x99 & y9 <=' z9 ) or ( not y9 <=' x99 & not y9 <=' z9 ) ) ;
suppose that A36: y9 <=' x99 and
A37: y9 <=' z9 ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A38: + (y,z) = z9 -' y9 by A34, A37, ARYTM_1:def 2;
then consider x9, yz9 being Element of REAL+ such that
A39: x = x9 and
A40: ( + (y,z) = yz9 & + (x,(+ (y,z))) = x9 + yz9 ) by A26, Def1;
A41: + (x,y) = x9 -' y9 by A29, A31, A35, A36, A39, ARYTM_1:def 2;
then ex z99, xy99 being Element of REAL+ st
( z = z99 & + (x,y) = xy99 & + (z,(+ (x,y))) = z99 + xy99 ) by A28, Def1;
hence + (x,(+ (y,z))) = + ((+ (x,y)),z) by A32, A29, A36, A37, A38, A39, A40, A41, ARYTM_1:12; :: thesis: verum
end;
suppose that A42: y9 <=' x99 and
A43: not y9 <=' z9 ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A44: + (x,y) = x99 -' y9 by A31, A35, A42, ARYTM_1:def 2;
then A45: ex z99, xy99 being Element of REAL+ st
( z = z99 & + (x,y) = xy99 & + (z,(+ (x,y))) = z99 + xy99 ) by A28, Def1;
A46: + (y,z) = [0,(y9 -' z9)] by A34, A43, ARYTM_1:def 2;
then + (y,z) in [:{0},REAL+:] by Lm1;
then consider x9, yz9 being Element of REAL+ such that
A47: x = x9 and
A48: ( + (y,z) = [0,yz9] & + (x,(+ (y,z))) = x9 - yz9 ) by A26, Def1;
thus + (x,(+ (y,z))) = x9 - (y9 -' z9) by A46, A48, XTUPLE_0:1
.= + ((+ (x,y)),z) by A32, A29, A42, A43, A47, A44, A45, ARYTM_1:22 ; :: thesis: verum
end;
suppose that A49: not y9 <=' x99 and
A50: y9 <=' z9 ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A51: + (y,x) = [0,(y9 -' x99)] by A31, A35, A49, ARYTM_1:def 2;
then + (y,x) in [:{0},REAL+:] by Lm1;
then consider z99, yx99 being Element of REAL+ such that
A52: z = z99 and
A53: ( + (y,x) = [0,yx99] & + (z,(+ (y,x))) = z99 - yx99 ) by A28, Def1;
A54: + (z,y) = z9 -' y9 by A34, A50, ARYTM_1:def 2;
then ex x9, zy99 being Element of REAL+ st
( x = x9 & + (z,y) = zy99 & + (x,(+ (z,y))) = x9 + zy99 ) by A26, Def1;
hence + (x,(+ (y,z))) = z99 - (y9 -' x99) by A32, A29, A49, A50, A52, A54, ARYTM_1:22
.= + ((+ (x,y)),z) by A51, A53, XTUPLE_0:1 ;
:: thesis: verum
end;
suppose that A55: not y9 <=' x99 and
A56: not y9 <=' z9 ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A57: + (y,z) = [0,(y9 -' z9)] by A34, A56, ARYTM_1:def 2;
then + (y,z) in [:{0},REAL+:] by Lm1;
then consider x9, yz9 being Element of REAL+ such that
A58: x = x9 and
A59: ( + (y,z) = [0,yz9] & + (x,(+ (y,z))) = x9 - yz9 ) by A26, Def1;
A60: + (y,x) = [0,(y9 -' x99)] by A31, A35, A55, ARYTM_1:def 2;
then + (y,x) in [:{0},REAL+:] by Lm1;
then consider z99, yx99 being Element of REAL+ such that
A61: z = z99 and
A62: ( + (y,x) = [0,yx99] & + (z,(+ (y,x))) = z99 - yx99 ) by A28, Def1;
thus + (x,(+ (y,z))) = x9 - (y9 -' z9) by A57, A59, XTUPLE_0:1
.= z99 - (y9 -' x99) by A32, A29, A55, A56, A61, A58, ARYTM_1:23
.= + ((+ (x,y)),z) by A60, A62, XTUPLE_0:1 ; :: thesis: verum
end;
end;
end;
hence + (x,(+ (y,z))) = + ((+ (x,y)),z) ; :: thesis: verum
end;
suppose that A63: x in REAL+ and
A64: y in [:{0},REAL+:] and
A65: z in [:{0},REAL+:] ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
( ( not z in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not z in [:{0},REAL+:] ) ) by A64, A65, Th5, XBOOLE_0:3;
then consider y9, z9 being Element of REAL+ such that
A66: y = [0,y9] and
A67: z = [0,z9] and
A68: + (y,z) = [0,(y9 + z9)] by A64, Def1;
+ (y,z) in [:{0},REAL+:] by A68, Lm1;
then consider x9, yz9 being Element of REAL+ such that
A69: x = x9 and
A70: + (y,z) = [0,yz9] and
A71: + (x,(+ (y,z))) = x9 - yz9 by A63, Def1;
consider x99, y99 being Element of REAL+ such that
A72: x = x99 and
A73: y = [0,y99] and
A74: + (x,y) = x99 - y99 by A63, A64, Def1;
A75: y9 = y99 by A66, A73, XTUPLE_0:1;
now :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
per cases ( y99 <=' x99 or not y99 <=' x99 ) ;
suppose A76: y99 <=' x99 ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
then A77: + (x,y) = x99 -' y99 by A74, ARYTM_1:def 2;
then consider xy99, z99 being Element of REAL+ such that
A78: + (x,y) = xy99 and
A79: z = [0,z99] and
A80: + ((+ (x,y)),z) = xy99 - z99 by A65, Def1;
A81: z9 = z99 by A67, A79, XTUPLE_0:1;
thus + (x,(+ (y,z))) = x9 - (y9 + z9) by A68, A70, A71, XTUPLE_0:1
.= + ((+ (x,y)),z) by A72, A69, A75, A76, A77, A78, A80, A81, ARYTM_1:24 ; :: thesis: verum
end;
suppose A82: not y99 <=' x99 ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A83: ( not z in REAL+ or not + (x,y) in [:{0},REAL+:] ) by A65, Th5, XBOOLE_0:3;
A84: + (x,y) = [0,(y99 -' x99)] by A74, A82, ARYTM_1:def 2;
then + (x,y) in [:{0},REAL+:] by Lm1;
then ( not + (x,y) in REAL+ or not z in [:{0},REAL+:] ) by Th5, XBOOLE_0:3;
then consider xy99, z99 being Element of REAL+ such that
A85: + (x,y) = [0,xy99] and
A86: z = [0,z99] and
A87: + ((+ (x,y)),z) = [0,(xy99 + z99)] by A84, A83, Def1, Lm1;
A88: z9 = z99 by A67, A86, XTUPLE_0:1;
A89: yz9 = z9 + y9 by A68, A70, XTUPLE_0:1;
then y99 <=' yz9 by A75, ARYTM_2:19;
then not yz9 <=' x9 by A72, A69, A82, ARYTM_1:3;
hence + (x,(+ (y,z))) = [0,((z9 + y9) -' x9)] by A71, A89, ARYTM_1:def 2
.= [0,(z99 + (y99 -' x99))] by A72, A69, A75, A82, A88, ARYTM_1:13
.= + ((+ (x,y)),z) by A84, A85, A87, XTUPLE_0:1 ;
:: thesis: verum
end;
end;
end;
hence + (x,(+ (y,z))) = + ((+ (x,y)),z) ; :: thesis: verum
end;
suppose that A90: z in REAL+ and
A91: y in REAL+ and
A92: x in [:{0},REAL+:] ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A93: ex z99, y99 being Element of REAL+ st
( z = z99 & y = y99 & + (z,y) = z99 + y99 ) by A90, A91, Def1;
then consider zy99, x99 being Element of REAL+ such that
A94: + (z,y) = zy99 and
A95: x = [0,x99] and
A96: + ((+ (z,y)),x) = zy99 - x99 by A92, Def1;
consider y9, x9 being Element of REAL+ such that
A97: y = y9 and
A98: x = [0,x9] and
A99: + (y,x) = y9 - x9 by A91, A92, Def1;
A100: x9 = x99 by A98, A95, XTUPLE_0:1;
now :: thesis: + (z,(+ (y,x))) = + ((+ (z,y)),x)
per cases ( x9 <=' y9 or not x9 <=' y9 ) ;
suppose A101: x9 <=' y9 ; :: thesis: + (z,(+ (y,x))) = + ((+ (z,y)),x)
then A102: + (y,x) = y9 -' x9 by A99, ARYTM_1:def 2;
then ex z9, yx9 being Element of REAL+ st
( z = z9 & + (y,x) = yx9 & + (z,(+ (y,x))) = z9 + yx9 ) by A90, Def1;
hence + (z,(+ (y,x))) = + ((+ (z,y)),x) by A97, A93, A94, A96, A100, A101, A102, ARYTM_1:20; :: thesis: verum
end;
suppose A103: not x9 <=' y9 ; :: thesis: + (z,(+ (y,x))) = + ((+ (z,y)),x)
then A104: + (y,x) = [0,(x9 -' y9)] by A99, ARYTM_1:def 2;
then + (y,x) in [:{0},REAL+:] by Lm1;
then consider z9, yx9 being Element of REAL+ such that
A105: z = z9 and
A106: ( + (y,x) = [0,yx9] & + (z,(+ (y,x))) = z9 - yx9 ) by A90, Def1;
thus + (z,(+ (y,x))) = z9 - (x9 -' y9) by A104, A106, XTUPLE_0:1
.= + ((+ (z,y)),x) by A97, A93, A94, A96, A100, A103, A105, ARYTM_1:21 ; :: thesis: verum
end;
end;
end;
hence + (x,(+ (y,z))) = + ((+ (x,y)),z) ; :: thesis: verum
end;
suppose that A107: x in [:{0},REAL+:] and
A108: y in REAL+ and
A109: z in [:{0},REAL+:] ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
consider y9, z9 being Element of REAL+ such that
A110: y = y9 and
A111: z = [0,z9] and
A112: + (y,z) = y9 - z9 by A108, A109, Def1;
consider x99, y99 being Element of REAL+ such that
A113: x = [0,x99] and
A114: y = y99 and
A115: + (x,y) = y99 - x99 by A107, A108, Def1;
now :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
per cases ( ( x99 <=' y99 & z9 <=' y9 ) or ( not x99 <=' y99 & z9 <=' y9 ) or ( not z9 <=' y9 & x99 <=' y99 ) or ( not x99 <=' y99 & not z9 <=' y9 ) ) ;
suppose that A116: x99 <=' y99 and
A117: z9 <=' y9 ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A118: + (y,z) = y9 -' z9 by A112, A117, ARYTM_1:def 2;
then consider x9, yz9 being Element of REAL+ such that
A119: x = [0,x9] and
A120: ( + (y,z) = yz9 & + (x,(+ (y,z))) = yz9 - x9 ) by A107, Def1;
A121: x9 = x99 by A113, A119, XTUPLE_0:1;
then A122: + (x,y) = y9 -' x9 by A110, A114, A115, A116, ARYTM_1:def 2;
then consider z99, xy99 being Element of REAL+ such that
A123: z = [0,z99] and
A124: ( + (x,y) = xy99 & + (z,(+ (x,y))) = xy99 - z99 ) by A109, Def1;
z9 = z99 by A111, A123, XTUPLE_0:1;
hence + (x,(+ (y,z))) = + ((+ (x,y)),z) by A110, A114, A116, A117, A118, A120, A121, A122, A124, ARYTM_1:25; :: thesis: verum
end;
suppose that A125: not x99 <=' y99 and
A126: z9 <=' y9 ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A127: ( not z in REAL+ or not + (x,y) in [:{0},REAL+:] ) by A109, Th5, XBOOLE_0:3;
A128: + (y,x) = [0,(x99 -' y99)] by A115, A125, ARYTM_1:def 2;
then + (y,x) in [:{0},REAL+:] by Lm1;
then ( not + (x,y) in REAL+ or not z in [:{0},REAL+:] ) by Th5, XBOOLE_0:3;
then consider z99, yx9 being Element of REAL+ such that
A129: z = [0,z99] and
A130: ( + (y,x) = [0,yx9] & + (z,(+ (y,x))) = [0,(z99 + yx9)] ) by A128, A127, Def1, Lm1;
A131: z9 = z99 by A111, A129, XTUPLE_0:1;
A132: + (y,z) = y9 -' z9 by A112, A126, ARYTM_1:def 2;
then consider x9, yz9 being Element of REAL+ such that
A133: x = [0,x9] and
A134: + (y,z) = yz9 and
A135: + (x,(+ (y,z))) = yz9 - x9 by A107, Def1;
A136: x9 = x99 by A113, A133, XTUPLE_0:1;
yz9 <=' y9 by A132, A134, ARYTM_1:11;
then not x9 <=' yz9 by A110, A114, A125, A136, ARYTM_1:3;
hence + (x,(+ (y,z))) = [0,(x9 -' (y9 -' z9))] by A132, A134, A135, ARYTM_1:def 2
.= [0,((x99 -' y99) + z99)] by A110, A114, A125, A126, A136, A131, ARYTM_1:14
.= + ((+ (x,y)),z) by A128, A130, XTUPLE_0:1 ;
:: thesis: verum
end;
suppose that A137: not z9 <=' y9 and
A138: x99 <=' y99 ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A139: ( not x in REAL+ or not + (z,y) in [:{0},REAL+:] ) by A107, Th5, XBOOLE_0:3;
A140: + (y,z) = [0,(z9 -' y9)] by A112, A137, ARYTM_1:def 2;
then + (y,z) in [:{0},REAL+:] by Lm1;
then ( not + (z,y) in REAL+ or not x in [:{0},REAL+:] ) by Th5, XBOOLE_0:3;
then consider x9, yz99 being Element of REAL+ such that
A141: x = [0,x9] and
A142: ( + (y,z) = [0,yz99] & + (x,(+ (y,z))) = [0,(x9 + yz99)] ) by A140, A139, Def1, Lm1;
A143: x99 = x9 by A113, A141, XTUPLE_0:1;
A144: + (y,x) = y99 -' x99 by A115, A138, ARYTM_1:def 2;
then consider z99, yx99 being Element of REAL+ such that
A145: z = [0,z99] and
A146: + (y,x) = yx99 and
A147: + (z,(+ (y,x))) = yx99 - z99 by A109, Def1;
A148: z99 = z9 by A111, A145, XTUPLE_0:1;
yx99 <=' y99 by A144, A146, ARYTM_1:11;
then A149: not z99 <=' yx99 by A110, A114, A137, A148, ARYTM_1:3;
thus + (x,(+ (y,z))) = [0,((z9 -' y9) + x9)] by A140, A142, XTUPLE_0:1
.= [0,(z99 -' (y99 -' x99))] by A110, A114, A137, A138, A148, A143, ARYTM_1:14
.= + ((+ (x,y)),z) by A144, A146, A147, A149, ARYTM_1:def 2 ; :: thesis: verum
end;
suppose that A150: not x99 <=' y99 and
A151: not z9 <=' y9 ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A152: ( not x in REAL+ or not + (z,y) in [:{0},REAL+:] ) by A107, Th5, XBOOLE_0:3;
A153: ( not z in REAL+ or not + (x,y) in [:{0},REAL+:] ) by A109, Th5, XBOOLE_0:3;
A154: + (y,x) = [0,(x99 -' y99)] by A115, A150, ARYTM_1:def 2;
then + (y,x) in [:{0},REAL+:] by Lm1;
then ( not + (x,y) in REAL+ or not z in [:{0},REAL+:] ) by Th5, XBOOLE_0:3;
then consider z99, yx9 being Element of REAL+ such that
A155: z = [0,z99] and
A156: ( + (y,x) = [0,yx9] & + (z,(+ (y,x))) = [0,(z99 + yx9)] ) by A154, A153, Def1, Lm1;
A157: z9 = z99 by A111, A155, XTUPLE_0:1;
A158: + (y,z) = [0,(z9 -' y9)] by A112, A151, ARYTM_1:def 2;
then + (y,z) in [:{0},REAL+:] by Lm1;
then ( not + (z,y) in REAL+ or not x in [:{0},REAL+:] ) by Th5, XBOOLE_0:3;
then consider x9, yz99 being Element of REAL+ such that
A159: x = [0,x9] and
A160: ( + (y,z) = [0,yz99] & + (x,(+ (y,z))) = [0,(x9 + yz99)] ) by A158, A152, Def1, Lm1;
A161: x9 = x99 by A113, A159, XTUPLE_0:1;
thus + (x,(+ (y,z))) = [0,((z9 -' y9) + x9)] by A158, A160, XTUPLE_0:1
.= [0,((x99 -' y99) + z99)] by A110, A114, A150, A151, A157, A161, ARYTM_1:15
.= + ((+ (x,y)),z) by A154, A156, XTUPLE_0:1 ; :: thesis: verum
end;
end;
end;
hence + (x,(+ (y,z))) = + ((+ (x,y)),z) ; :: thesis: verum
end;
suppose that A162: z in REAL+ and
A163: y in [:{0},REAL+:] and
A164: x in [:{0},REAL+:] ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
( ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) ) by A163, A164, Th5, XBOOLE_0:3;
then consider y9, x9 being Element of REAL+ such that
A165: y = [0,y9] and
A166: x = [0,x9] and
A167: + (y,x) = [0,(y9 + x9)] by A163, Def1;
+ (y,x) in [:{0},REAL+:] by A167, Lm1;
then consider z9, yx9 being Element of REAL+ such that
A168: z = z9 and
A169: + (y,x) = [0,yx9] and
A170: + (z,(+ (y,x))) = z9 - yx9 by A162, Def1;
consider z99, y99 being Element of REAL+ such that
A171: z = z99 and
A172: y = [0,y99] and
A173: + (z,y) = z99 - y99 by A162, A163, Def1;
A174: y9 = y99 by A165, A172, XTUPLE_0:1;
now :: thesis: + (z,(+ (y,x))) = + ((+ (z,y)),x)
per cases ( y99 <=' z99 or not y99 <=' z99 ) ;
suppose A175: y99 <=' z99 ; :: thesis: + (z,(+ (y,x))) = + ((+ (z,y)),x)
then A176: + (z,y) = z99 -' y99 by A173, ARYTM_1:def 2;
then consider zy99, x99 being Element of REAL+ such that
A177: + (z,y) = zy99 and
A178: x = [0,x99] and
A179: + ((+ (z,y)),x) = zy99 - x99 by A164, Def1;
A180: x9 = x99 by A166, A178, XTUPLE_0:1;
thus + (z,(+ (y,x))) = z9 - (y9 + x9) by A167, A169, A170, XTUPLE_0:1
.= + ((+ (z,y)),x) by A171, A168, A174, A175, A176, A177, A179, A180, ARYTM_1:24 ; :: thesis: verum
end;
suppose A181: not y99 <=' z99 ; :: thesis: + (z,(+ (y,x))) = + ((+ (z,y)),x)
A182: ( not x in REAL+ or not + (z,y) in [:{0},REAL+:] ) by A164, Th5, XBOOLE_0:3;
A183: + (z,y) = [0,(y99 -' z99)] by A173, A181, ARYTM_1:def 2;
then + (z,y) in [:{0},REAL+:] by Lm1;
then ( not + (z,y) in REAL+ or not x in [:{0},REAL+:] ) by Th5, XBOOLE_0:3;
then consider zy99, x99 being Element of REAL+ such that
A184: + (z,y) = [0,zy99] and
A185: x = [0,x99] and
A186: + ((+ (z,y)),x) = [0,(zy99 + x99)] by A183, A182, Def1, Lm1;
A187: x9 = x99 by A166, A185, XTUPLE_0:1;
A188: yx9 = x9 + y9 by A167, A169, XTUPLE_0:1;
then y99 <=' yx9 by A174, ARYTM_2:19;
then not yx9 <=' z9 by A171, A168, A181, ARYTM_1:3;
hence + (z,(+ (y,x))) = [0,((x9 + y9) -' z9)] by A170, A188, ARYTM_1:def 2
.= [0,(x99 + (y99 -' z99))] by A171, A168, A174, A181, A187, ARYTM_1:13
.= + ((+ (z,y)),x) by A183, A184, A186, XTUPLE_0:1 ;
:: thesis: verum
end;
end;
end;
hence + (x,(+ (y,z))) = + ((+ (x,y)),z) ; :: thesis: verum
end;
suppose that A189: x in [:{0},REAL+:] and
A190: y in [:{0},REAL+:] and
A191: z in [:{0},REAL+:] ; :: thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A192: ( not x in REAL+ or not + (z,y) in [:{0},REAL+:] ) by A189, Th5, XBOOLE_0:3;
( ( not z in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not z in [:{0},REAL+:] ) ) by A190, A191, Th5, XBOOLE_0:3;
then consider y9, z9 being Element of REAL+ such that
A193: y = [0,y9] and
A194: z = [0,z9] and
A195: + (y,z) = [0,(y9 + z9)] by A190, Def1;
+ (z,y) in [:{0},REAL+:] by A195, Lm1;
then ( not + (z,y) in REAL+ or not x in [:{0},REAL+:] ) by Th5, XBOOLE_0:3;
then consider x9, yz9 being Element of REAL+ such that
A196: x = [0,x9] and
A197: ( + (y,z) = [0,yz9] & + (x,(+ (y,z))) = [0,(x9 + yz9)] ) by A195, A192, Def1, Lm1;
A198: ( not z in REAL+ or not + (x,y) in [:{0},REAL+:] ) by A191, Th5, XBOOLE_0:3;
( ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) ) by A189, A190, Th5, XBOOLE_0:3;
then consider x99, y99 being Element of REAL+ such that
A199: x = [0,x99] and
A200: y = [0,y99] and
A201: + (x,y) = [0,(x99 + y99)] by A189, Def1;
A202: x9 = x99 by A199, A196, XTUPLE_0:1;
+ (x,y) in [:{0},REAL+:] by A201, Lm1;
then ( not + (x,y) in REAL+ or not z in [:{0},REAL+:] ) by Th5, XBOOLE_0:3;
then consider xy99, z99 being Element of REAL+ such that
A203: + (x,y) = [0,xy99] and
A204: z = [0,z99] and
A205: + ((+ (x,y)),z) = [0,(xy99 + z99)] by A201, A198, Def1, Lm1;
A206: z9 = z99 by A194, A204, XTUPLE_0:1;
A207: y9 = y99 by A193, A200, XTUPLE_0:1;
thus + (x,(+ (y,z))) = [0,((z9 + y9) + x9)] by A195, A197, XTUPLE_0:1
.= [0,(z99 + (y99 + x99))] by A206, A202, A207, ARYTM_2:6
.= + ((+ (x,y)),z) by A201, A203, A205, XTUPLE_0:1 ; :: thesis: verum
end;
end;