:: ARYTM_1 semantic presentation begin theorem Th1: :: ARYTM_1:1 for x, y being Element of REAL+ st x + y = y holds x = {} proof let x, y be Element of REAL+ ; ::_thesis: ( x + y = y implies x = {} ) reconsider o = {} as Element of REAL+ by ARYTM_2:20; assume x + y = y ; ::_thesis: x = {} then x + y = y + o by ARYTM_2:def_8; hence x = {} by ARYTM_2:11; ::_thesis: verum end; reconsider u = one as Element of REAL+ by ARYTM_2:20; Lm1: for x, y, z being Element of REAL+ st x *' y = x *' z & x <> {} holds y = z proof let x, y, z be Element of REAL+ ; ::_thesis: ( x *' y = x *' z & x <> {} implies y = z ) assume A1: x *' y = x *' z ; ::_thesis: ( not x <> {} or y = z ) assume x <> {} ; ::_thesis: y = z then consider x1 being Element of REAL+ such that A2: x *' x1 = one by ARYTM_2:14; thus y = (x *' x1) *' y by A2, ARYTM_2:15 .= x1 *' (x *' z) by A1, ARYTM_2:12 .= (x *' x1) *' z by ARYTM_2:12 .= z by A2, ARYTM_2:15 ; ::_thesis: verum end; theorem :: ARYTM_1:2 for x, y being Element of REAL+ holds ( not x *' y = {} or x = {} or y = {} ) proof let x, y be Element of REAL+ ; ::_thesis: ( not x *' y = {} or x = {} or y = {} ) assume A1: x *' y = {} ; ::_thesis: ( x = {} or y = {} ) assume x <> {} ; ::_thesis: y = {} then consider x1 being Element of REAL+ such that A2: x *' x1 = one by ARYTM_2:14; thus y = (x *' x1) *' y by A2, ARYTM_2:15 .= (x *' y) *' x1 by ARYTM_2:12 .= {} by A1, ARYTM_2:4 ; ::_thesis: verum end; theorem Th3: :: ARYTM_1:3 for x, y, z being Element of REAL+ st x <=' y & y <=' z holds x <=' z proof let x, y, z be Element of REAL+ ; ::_thesis: ( x <=' y & y <=' z implies x <=' z ) assume x <=' y ; ::_thesis: ( not y <=' z or x <=' z ) then consider z1 being Element of REAL+ such that A1: x + z1 = y by ARYTM_2:9; assume y <=' z ; ::_thesis: x <=' z then consider z2 being Element of REAL+ such that A2: y + z2 = z by ARYTM_2:9; z = x + (z1 + z2) by A1, A2, ARYTM_2:6; hence x <=' z by ARYTM_2:19; ::_thesis: verum end; theorem Th4: :: ARYTM_1:4 for x, y being Element of REAL+ st x <=' y & y <=' x holds x = y proof let x, y be Element of REAL+ ; ::_thesis: ( x <=' y & y <=' x implies x = y ) assume x <=' y ; ::_thesis: ( not y <=' x or x = y ) then consider z1 being Element of REAL+ such that A1: x + z1 = y by ARYTM_2:9; assume y <=' x ; ::_thesis: x = y then consider z2 being Element of REAL+ such that A2: y + z2 = x by ARYTM_2:9; x = x + (z1 + z2) by A1, A2, ARYTM_2:6; then z1 = {} by Th1, ARYTM_2:5; hence x = y by A1, ARYTM_2:def_8; ::_thesis: verum end; theorem Th5: :: ARYTM_1:5 for x, y being Element of REAL+ st x <=' y & y = {} holds x = {} proof let x, y be Element of REAL+ ; ::_thesis: ( x <=' y & y = {} implies x = {} ) assume x <=' y ; ::_thesis: ( not y = {} or x = {} ) then ex z being Element of REAL+ st x + z = y by ARYTM_2:9; hence ( not y = {} or x = {} ) by ARYTM_2:5; ::_thesis: verum end; theorem Th6: :: ARYTM_1:6 for x, y being Element of REAL+ st x = {} holds x <=' y proof let x, y be Element of REAL+ ; ::_thesis: ( x = {} implies x <=' y ) assume x = {} ; ::_thesis: x <=' y then x + y = y by ARYTM_2:def_8; hence x <=' y by ARYTM_2:19; ::_thesis: verum end; theorem Th7: :: ARYTM_1:7 for x, y, z being Element of REAL+ holds ( x <=' y iff x + z <=' y + z ) proof let x, y, z be Element of REAL+ ; ::_thesis: ( x <=' y iff x + z <=' y + z ) thus ( x <=' y implies x + z <=' y + z ) ::_thesis: ( x + z <=' y + z implies x <=' y ) proof assume x <=' y ; ::_thesis: x + z <=' y + z then consider z0 being Element of REAL+ such that A1: x + z0 = y by ARYTM_2:9; (x + z) + z0 = y + z by A1, ARYTM_2:6; hence x + z <=' y + z by ARYTM_2:19; ::_thesis: verum end; assume x + z <=' y + z ; ::_thesis: x <=' y then consider z0 being Element of REAL+ such that A2: (x + z) + z0 = y + z by ARYTM_2:9; y + z = (x + z0) + z by A2, ARYTM_2:6; hence x <=' y by ARYTM_2:11, ARYTM_2:19; ::_thesis: verum end; theorem Th8: :: ARYTM_1:8 for x, y, z being Element of REAL+ st x <=' y holds x *' z <=' y *' z proof let x, y, z be Element of REAL+ ; ::_thesis: ( x <=' y implies x *' z <=' y *' z ) assume x <=' y ; ::_thesis: x *' z <=' y *' z then consider z0 being Element of REAL+ such that A1: x + z0 = y by ARYTM_2:9; y *' z = (x *' z) + (z0 *' z) by A1, ARYTM_2:13; hence x *' z <=' y *' z by ARYTM_2:19; ::_thesis: verum end; Lm2: for x, y, z being Element of REAL+ st x *' y <=' x *' z & x <> {} holds y <=' z proof let x, y, z be Element of REAL+ ; ::_thesis: ( x *' y <=' x *' z & x <> {} implies y <=' z ) assume x *' y <=' x *' z ; ::_thesis: ( not x <> {} or y <=' z ) then consider z0 being Element of REAL+ such that A1: (x *' y) + z0 = x *' z by ARYTM_2:9; assume A2: x <> {} ; ::_thesis: y <=' z then consider x1 being Element of REAL+ such that A3: x *' x1 = one by ARYTM_2:14; x *' z = (x *' y) + (u *' z0) by A1, ARYTM_2:15 .= (x *' y) + (x *' (x1 *' z0)) by A3, ARYTM_2:12 .= x *' (y + (x1 *' z0)) by ARYTM_2:13 ; hence y <=' z by A2, Lm1, ARYTM_2:19; ::_thesis: verum end; definition let x, y be Element of REAL+ ; funcx -' y -> Element of REAL+ means :Def1: :: ARYTM_1:def 1 it + y = x if y <=' x otherwise it = {} ; existence ( ( y <=' x implies ex b1 being Element of REAL+ st b1 + y = x ) & ( not y <=' x implies ex b1 being Element of REAL+ st b1 = {} ) ) proof hereby ::_thesis: ( not y <=' x implies ex b1 being Element of REAL+ st b1 = {} ) assume y <=' x ; ::_thesis: ex IT being Element of REAL+ st IT + y = x then ex IT being Element of REAL+ st y + IT = x by ARYTM_2:9; hence ex IT being Element of REAL+ st IT + y = x ; ::_thesis: verum end; thus ( not y <=' x implies ex b1 being Element of REAL+ st b1 = {} ) by ARYTM_2:20; ::_thesis: verum end; correctness consistency for b1 being Element of REAL+ holds verum; uniqueness for b1, b2 being Element of REAL+ holds ( ( y <=' x & b1 + y = x & b2 + y = x implies b1 = b2 ) & ( not y <=' x & b1 = {} & b2 = {} implies b1 = b2 ) ); by ARYTM_2:11; end; :: deftheorem Def1 defines -' ARYTM_1:def_1_:_ for x, y, b3 being Element of REAL+ holds ( ( y <=' x implies ( b3 = x -' y iff b3 + y = x ) ) & ( not y <=' x implies ( b3 = x -' y iff b3 = {} ) ) ); Lm3: for x being Element of REAL+ holds x -' x = {} proof let x be Element of REAL+ ; ::_thesis: x -' x = {} x <=' x ; then (x -' x) + x = x by Def1; hence x -' x = {} by Th1; ::_thesis: verum end; theorem Th9: :: ARYTM_1:9 for x, y being Element of REAL+ holds ( x <=' y or x -' y <> {} ) proof let x, y be Element of REAL+ ; ::_thesis: ( x <=' y or x -' y <> {} ) assume A1: not x <=' y ; ::_thesis: x -' y <> {} assume A2: x -' y = {} ; ::_thesis: contradiction (x -' y) + y = x by A1, Def1; then x = y by A2, ARYTM_2:def_8; hence contradiction by A1; ::_thesis: verum end; theorem :: ARYTM_1:10 for x, y being Element of REAL+ st x <=' y & y -' x = {} holds x = y proof let x, y be Element of REAL+ ; ::_thesis: ( x <=' y & y -' x = {} implies x = y ) assume A1: x <=' y ; ::_thesis: ( not y -' x = {} or x = y ) assume y -' x = {} ; ::_thesis: x = y then y <=' x by Th9; hence x = y by A1, Th4; ::_thesis: verum end; theorem Th11: :: ARYTM_1:11 for x, y being Element of REAL+ holds x -' y <=' x proof let x, y be Element of REAL+ ; ::_thesis: x -' y <=' x percases ( y <=' x or not y <=' x ) ; suppose y <=' x ; ::_thesis: x -' y <=' x then (x -' y) + y = x by Def1; hence x -' y <=' x by ARYTM_2:19; ::_thesis: verum end; suppose not y <=' x ; ::_thesis: x -' y <=' x then x -' y = {} by Def1; hence x -' y <=' x by Th6; ::_thesis: verum end; end; end; Lm4: for x, y being Element of REAL+ st x = {} holds y -' x = y proof let x, y be Element of REAL+ ; ::_thesis: ( x = {} implies y -' x = y ) assume A1: x = {} ; ::_thesis: y -' x = y then A2: x <=' y by Th6; thus y -' x = (y -' x) + x by A1, ARYTM_2:def_8 .= y by A2, Def1 ; ::_thesis: verum end; Lm5: for x, y being Element of REAL+ holds (x + y) -' y = x proof let x, y be Element of REAL+ ; ::_thesis: (x + y) -' y = x y <=' x + y by ARYTM_2:19; hence (x + y) -' y = x by Def1; ::_thesis: verum end; Lm6: for x, y being Element of REAL+ st x <=' y holds y -' (y -' x) = x proof let x, y be Element of REAL+ ; ::_thesis: ( x <=' y implies y -' (y -' x) = x ) assume A1: x <=' y ; ::_thesis: y -' (y -' x) = x y -' x <=' y by Th11; then (y -' (y -' x)) + (y -' x) = y by Def1 .= (y -' x) + x by A1, Def1 ; hence y -' (y -' x) = x by ARYTM_2:11; ::_thesis: verum end; Lm7: for z, y, x being Element of REAL+ holds ( z -' y <=' x iff z <=' x + y ) proof let z, y, x be Element of REAL+ ; ::_thesis: ( z -' y <=' x iff z <=' x + y ) percases ( y <=' z or not y <=' z ) ; suppose y <=' z ; ::_thesis: ( z -' y <=' x iff z <=' x + y ) then (z -' y) + y = z by Def1; hence ( z -' y <=' x iff z <=' x + y ) by Th7; ::_thesis: verum end; supposeA1: not y <=' z ; ::_thesis: ( z -' y <=' x iff z <=' x + y ) A2: y <=' x + y by ARYTM_2:19; z -' y = {} by A1, Def1; hence ( z -' y <=' x iff z <=' x + y ) by A1, A2, Th3, Th6; ::_thesis: verum end; end; end; Lm8: for y, x, z being Element of REAL+ st y <=' x holds ( z + y <=' x iff z <=' x -' y ) proof let y, x, z be Element of REAL+ ; ::_thesis: ( y <=' x implies ( z + y <=' x iff z <=' x -' y ) ) assume y <=' x ; ::_thesis: ( z + y <=' x iff z <=' x -' y ) then (x -' y) + y = x by Def1; hence ( z + y <=' x iff z <=' x -' y ) by Th7; ::_thesis: verum end; Lm9: for z, y, x being Element of REAL+ holds (z -' y) -' x = z -' (x + y) proof let z, y, x be Element of REAL+ ; ::_thesis: (z -' y) -' x = z -' (x + y) percases ( x + y <=' z or x = {} or ( not y <=' z & x <> {} ) or ( not x + y <=' z & y <=' z ) ) ; supposeA1: x + y <=' z ; ::_thesis: (z -' y) -' x = z -' (x + y) y <=' x + y by ARYTM_2:19; then A2: y <=' z by A1, Th3; then A3: x <=' z -' y by A1, Lm8; ((z -' y) -' x) + (x + y) = (((z -' y) -' x) + x) + y by ARYTM_2:6 .= (z -' y) + y by A3, Def1 .= z by A2, Def1 ; hence (z -' y) -' x = z -' (x + y) by A1, Def1; ::_thesis: verum end; supposeA4: x = {} ; ::_thesis: (z -' y) -' x = z -' (x + y) hence (z -' y) -' x = z -' y by Lm4 .= z -' (x + y) by A4, ARYTM_2:def_8 ; ::_thesis: verum end; supposethat A5: not y <=' z and A6: x <> {} ; ::_thesis: (z -' y) -' x = z -' (x + y) y <=' y + x by ARYTM_2:19; then A7: not x + y <=' z by A5, Th3; now__::_thesis:_not_x_<='_z_-'_y assume A8: x <=' z -' y ; ::_thesis: contradiction z -' y = {} by A5, Def1; hence contradiction by A6, A8, Th5; ::_thesis: verum end; hence (z -' y) -' x = {} by Def1 .= z -' (x + y) by A7, Def1 ; ::_thesis: verum end; supposethat A9: not x + y <=' z and A10: y <=' z ; ::_thesis: (z -' y) -' x = z -' (x + y) not x <=' z -' y by A9, A10, Lm8; hence (z -' y) -' x = {} by Def1 .= z -' (x + y) by A9, Def1 ; ::_thesis: verum end; end; end; Lm10: for y, z, x being Element of REAL+ holds (y -' z) -' x = (y -' x) -' z proof let y, z, x be Element of REAL+ ; ::_thesis: (y -' z) -' x = (y -' x) -' z thus (y -' z) -' x = y -' (x + z) by Lm9 .= (y -' x) -' z by Lm9 ; ::_thesis: verum end; theorem :: ARYTM_1:12 for y, x, z being Element of REAL+ st y <=' x & y <=' z holds x + (z -' y) = (x -' y) + z proof let y, x, z be Element of REAL+ ; ::_thesis: ( y <=' x & y <=' z implies x + (z -' y) = (x -' y) + z ) assume that A1: y <=' x and A2: y <=' z ; ::_thesis: x + (z -' y) = (x -' y) + z (x + (z -' y)) + y = x + ((z -' y) + y) by ARYTM_2:6 .= x + z by A2, Def1 .= ((x -' y) + y) + z by A1, Def1 .= ((x -' y) + z) + y by ARYTM_2:6 ; hence x + (z -' y) = (x -' y) + z by ARYTM_2:11; ::_thesis: verum end; theorem Th13: :: ARYTM_1:13 for z, y, x being Element of REAL+ st z <=' y holds x + (y -' z) = (x + y) -' z proof let z, y, x be Element of REAL+ ; ::_thesis: ( z <=' y implies x + (y -' z) = (x + y) -' z ) assume A1: z <=' y ; ::_thesis: x + (y -' z) = (x + y) -' z y <=' x + y by ARYTM_2:19; then A2: z <=' x + y by A1, Th3; (x + (y -' z)) + z = x + ((y -' z) + z) by ARYTM_2:6 .= x + y by A1, Def1 .= ((x + y) -' z) + z by A2, Def1 ; hence x + (y -' z) = (x + y) -' z by ARYTM_2:11; ::_thesis: verum end; Lm11: for y, z, x being Element of REAL+ st y <=' z holds x -' (z -' y) = (x + y) -' z proof let y, z, x be Element of REAL+ ; ::_thesis: ( y <=' z implies x -' (z -' y) = (x + y) -' z ) assume A1: y <=' z ; ::_thesis: x -' (z -' y) = (x + y) -' z percases ( z -' y <=' x or not z -' y <=' x ) ; supposeA2: z -' y <=' x ; ::_thesis: x -' (z -' y) = (x + y) -' z then A3: z <=' x + y by Lm7; (x -' (z -' y)) + (z -' y) = x by A2, Def1 .= (x + z) -' z by Lm5 .= (x + (y + (z -' y))) -' z by A1, Def1 .= ((x + y) + (z -' y)) -' z by ARYTM_2:6 .= ((x + y) -' z) + (z -' y) by A3, Th13 ; hence x -' (z -' y) = (x + y) -' z by ARYTM_2:11; ::_thesis: verum end; supposeA4: not z -' y <=' x ; ::_thesis: x -' (z -' y) = (x + y) -' z then A5: not z <=' x + y by Lm7; thus x -' (z -' y) = {} by A4, Def1 .= (x + y) -' z by A5, Def1 ; ::_thesis: verum end; end; end; Lm12: for z, x, y being Element of REAL+ st z <=' x & y <=' z holds x -' (z -' y) = (x -' z) + y proof let z, x, y be Element of REAL+ ; ::_thesis: ( z <=' x & y <=' z implies x -' (z -' y) = (x -' z) + y ) assume that A1: z <=' x and A2: y <=' z ; ::_thesis: x -' (z -' y) = (x -' z) + y thus x -' (z -' y) = (x + y) -' z by A2, Lm11 .= (x -' z) + y by A1, Th13 ; ::_thesis: verum end; Lm13: for x, z, y being Element of REAL+ st x <=' z & y <=' z holds x -' (z -' y) = y -' (z -' x) proof let x, z, y be Element of REAL+ ; ::_thesis: ( x <=' z & y <=' z implies x -' (z -' y) = y -' (z -' x) ) assume that A1: x <=' z and A2: y <=' z ; ::_thesis: x -' (z -' y) = y -' (z -' x) thus x -' (z -' y) = (x + y) -' z by A2, Lm11 .= y -' (z -' x) by A1, Lm11 ; ::_thesis: verum end; theorem :: ARYTM_1:14 for z, x, y being Element of REAL+ st z <=' x & y <=' z holds (x -' z) + y = x -' (z -' y) proof let z, x, y be Element of REAL+ ; ::_thesis: ( z <=' x & y <=' z implies (x -' z) + y = x -' (z -' y) ) assume that A1: z <=' x and A2: y <=' z ; ::_thesis: (x -' z) + y = x -' (z -' y) thus x -' (z -' y) = (x + y) -' z by A2, Lm11 .= (x -' z) + y by A1, Th13 ; ::_thesis: verum end; theorem :: ARYTM_1:15 for y, x, z being Element of REAL+ st y <=' x & y <=' z holds (z -' y) + x = (x -' y) + z proof let y, x, z be Element of REAL+ ; ::_thesis: ( y <=' x & y <=' z implies (z -' y) + x = (x -' y) + z ) assume that A1: y <=' x and A2: y <=' z ; ::_thesis: (z -' y) + x = (x -' y) + z ((z -' y) + x) + y = ((z -' y) + y) + x by ARYTM_2:6 .= z + x by A2, Def1 .= ((x -' y) + y) + z by A1, Def1 .= ((x -' y) + z) + y by ARYTM_2:6 ; hence (z -' y) + x = (x -' y) + z by ARYTM_2:11; ::_thesis: verum end; theorem :: ARYTM_1:16 for x, y, z being Element of REAL+ st x <=' y holds z -' y <=' z -' x proof let x, y, z be Element of REAL+ ; ::_thesis: ( x <=' y implies z -' y <=' z -' x ) assume A1: x <=' y ; ::_thesis: z -' y <=' z -' x percases ( y <=' z or not y <=' z ) ; supposeA2: y <=' z ; ::_thesis: z -' y <=' z -' x (z -' y) + x <=' (z -' y) + y by A1, Th7; then A3: (z -' y) + x <=' z by A2, Def1; x <=' z by A1, A2, Th3; then (z -' y) + x <=' (z -' x) + x by A3, Def1; hence z -' y <=' z -' x by Th7; ::_thesis: verum end; suppose not y <=' z ; ::_thesis: z -' y <=' z -' x then z -' y = {} by Def1; hence z -' y <=' z -' x by Th6; ::_thesis: verum end; end; end; theorem :: ARYTM_1:17 for x, y, z being Element of REAL+ st x <=' y holds x -' z <=' y -' z proof let x, y, z be Element of REAL+ ; ::_thesis: ( x <=' y implies x -' z <=' y -' z ) assume A1: x <=' y ; ::_thesis: x -' z <=' y -' z percases ( z <=' x or not z <=' x ) ; supposeA2: z <=' x ; ::_thesis: x -' z <=' y -' z then z <=' y by A1, Th3; then A3: (y -' z) + z = y by Def1; (x -' z) + z = x by A2, Def1; hence x -' z <=' y -' z by A1, A3, Th7; ::_thesis: verum end; suppose not z <=' x ; ::_thesis: x -' z <=' y -' z then x -' z = {} by Def1; hence x -' z <=' y -' z by Th6; ::_thesis: verum end; end; end; Lm14: for x, y, z being Element of REAL+ holds x *' (y -' z) = (x *' y) -' (x *' z) proof let x, y, z be Element of REAL+ ; ::_thesis: x *' (y -' z) = (x *' y) -' (x *' z) percases ( z <=' y or x = {} or ( not z <=' y & x <> {} ) ) ; supposeA1: z <=' y ; ::_thesis: x *' (y -' z) = (x *' y) -' (x *' z) then A2: x *' z <=' x *' y by Th8; (x *' (y -' z)) + (x *' z) = x *' ((y -' z) + z) by ARYTM_2:13 .= x *' y by A1, Def1 .= ((x *' y) -' (x *' z)) + (x *' z) by A2, Def1 ; hence x *' (y -' z) = (x *' y) -' (x *' z) by ARYTM_2:11; ::_thesis: verum end; supposeA3: x = {} ; ::_thesis: x *' (y -' z) = (x *' y) -' (x *' z) then x *' y = {} by ARYTM_2:4; hence x *' (y -' z) = x *' y by A3, ARYTM_2:4 .= (x *' y) -' (x *' z) by A3, Lm4, ARYTM_2:4 ; ::_thesis: verum end; supposeA4: ( not z <=' y & x <> {} ) ; ::_thesis: x *' (y -' z) = (x *' y) -' (x *' z) then A5: not x *' z <=' x *' y by Lm2; y -' z = {} by A4, Def1; hence x *' (y -' z) = {} by ARYTM_2:4 .= (x *' y) -' (x *' z) by A5, Def1 ; ::_thesis: verum end; end; end; definition let x, y be Element of REAL+ ; funcx - y -> set equals :Def2: :: ARYTM_1:def 2 x -' y if y <=' x otherwise [{},(y -' x)]; correctness coherence ( ( y <=' x implies x -' y is set ) & ( not y <=' x implies [{},(y -' x)] is set ) ); consistency for b1 being set holds verum; ; end; :: deftheorem Def2 defines - ARYTM_1:def_2_:_ for x, y being Element of REAL+ holds ( ( y <=' x implies x - y = x -' y ) & ( not y <=' x implies x - y = [{},(y -' x)] ) ); theorem :: ARYTM_1:18 for x being Element of REAL+ holds x - x = {} proof let x be Element of REAL+ ; ::_thesis: x - x = {} x <=' x ; then x - x = x -' x by Def2; hence x - x = {} by Lm3; ::_thesis: verum end; theorem :: ARYTM_1:19 for x, y being Element of REAL+ st x = {} & y <> {} holds x - y = [{},y] proof let x, y be Element of REAL+ ; ::_thesis: ( x = {} & y <> {} implies x - y = [{},y] ) assume that A1: x = {} and A2: y <> {} ; ::_thesis: x - y = [{},y] x <=' y by A1, Th6; then not y <=' x by A1, A2, Th4; hence x - y = [{},(y -' x)] by Def2 .= [{},y] by A1, Lm4 ; ::_thesis: verum end; theorem :: ARYTM_1:20 for z, y, x being Element of REAL+ st z <=' y holds x + (y -' z) = (x + y) - z proof let z, y, x be Element of REAL+ ; ::_thesis: ( z <=' y implies x + (y -' z) = (x + y) - z ) assume A1: z <=' y ; ::_thesis: x + (y -' z) = (x + y) - z y <=' x + y by ARYTM_2:19; then z <=' x + y by A1, Th3; then (x + y) - z = (x + y) -' z by Def2; hence x + (y -' z) = (x + y) - z by A1, Th13; ::_thesis: verum end; theorem :: ARYTM_1:21 for z, y, x being Element of REAL+ st not z <=' y holds x - (z -' y) = (x + y) - z proof let z, y, x be Element of REAL+ ; ::_thesis: ( not z <=' y implies x - (z -' y) = (x + y) - z ) assume A1: not z <=' y ; ::_thesis: x - (z -' y) = (x + y) - z percases ( z -' y <=' x or not z -' y <=' x ) ; supposeA2: z -' y <=' x ; ::_thesis: x - (z -' y) = (x + y) - z then z <=' x + y by Lm7; then A3: (x + y) - z = (x + y) -' z by Def2; x - (z -' y) = x -' (z -' y) by A2, Def2; hence x - (z -' y) = (x + y) - z by A1, A3, Lm11; ::_thesis: verum end; supposeA4: not z -' y <=' x ; ::_thesis: x - (z -' y) = (x + y) - z then A5: not z <=' x + y by Lm7; (z -' y) -' x = z -' (x + y) by Lm9; hence x - (z -' y) = [{},(z -' (x + y))] by A4, Def2 .= (x + y) - z by A5, Def2 ; ::_thesis: verum end; end; end; theorem :: ARYTM_1:22 for y, x, z being Element of REAL+ st y <=' x & not y <=' z holds x - (y -' z) = (x -' y) + z proof let y, x, z be Element of REAL+ ; ::_thesis: ( y <=' x & not y <=' z implies x - (y -' z) = (x -' y) + z ) assume that A1: y <=' x and A2: not y <=' z ; ::_thesis: x - (y -' z) = (x -' y) + z y -' z <=' y by Th11; then y -' z <=' x by A1, Th3; then x - (y -' z) = x -' (y -' z) by Def2; hence x - (y -' z) = (x -' y) + z by A1, A2, Lm12; ::_thesis: verum end; theorem :: ARYTM_1:23 for y, x, z being Element of REAL+ st not y <=' x & not y <=' z holds x - (y -' z) = z - (y -' x) proof let y, x, z be Element of REAL+ ; ::_thesis: ( not y <=' x & not y <=' z implies x - (y -' z) = z - (y -' x) ) assume A1: ( not y <=' x & not y <=' z ) ; ::_thesis: x - (y -' z) = z - (y -' x) percases ( y <=' x + z or not y <=' x + z ) ; supposeA2: y <=' x + z ; ::_thesis: x - (y -' z) = z - (y -' x) then y -' x <=' z by Lm7; then A3: z - (y -' x) = z -' (y -' x) by Def2; y -' z <=' x by A2, Lm7; then x - (y -' z) = x -' (y -' z) by Def2; hence x - (y -' z) = z - (y -' x) by A1, A3, Lm13; ::_thesis: verum end; supposeA4: not y <=' x + z ; ::_thesis: x - (y -' z) = z - (y -' x) then A5: not y -' x <=' z by Lm7; A6: (y -' z) -' x = (y -' x) -' z by Lm10; not y -' z <=' x by A4, Lm7; hence x - (y -' z) = [{},((y -' x) -' z)] by A6, Def2 .= z - (y -' x) by A5, Def2 ; ::_thesis: verum end; end; end; theorem :: ARYTM_1:24 for y, x, z being Element of REAL+ st y <=' x holds x - (y + z) = (x -' y) - z proof let y, x, z be Element of REAL+ ; ::_thesis: ( y <=' x implies x - (y + z) = (x -' y) - z ) assume A1: y <=' x ; ::_thesis: x - (y + z) = (x -' y) - z percases ( y + z <=' x or ( not y + z <=' x & x <=' y ) or ( not y + z <=' x & not x <=' y ) ) ; supposeA2: y + z <=' x ; ::_thesis: x - (y + z) = (x -' y) - z then z <=' x -' y by A1, Lm8; then A3: (x -' y) - z = (x -' y) -' z by Def2; x - (y + z) = x -' (y + z) by A2, Def2; hence x - (y + z) = (x -' y) - z by A3, Lm9; ::_thesis: verum end; supposethat A4: not y + z <=' x and A5: x <=' y ; ::_thesis: x - (y + z) = (x -' y) - z A6: not z <=' x -' y by A1, A4, Lm8; A7: (x + z) -' x = z by Lm5 .= z -' (x -' x) by Lm3, Lm4 ; x = y by A1, A5, Th4; hence x - (y + z) = [{},(z -' (x -' y))] by A4, A7, Def2 .= (x -' y) - z by A6, Def2 ; ::_thesis: verum end; supposethat A8: not y + z <=' x and A9: not x <=' y ; ::_thesis: x - (y + z) = (x -' y) - z A10: not z <=' x -' y by A1, A8, Lm8; (y + z) -' x = z -' (x -' y) by A9, Lm11; hence x - (y + z) = [{},(z -' (x -' y))] by A8, Def2 .= (x -' y) - z by A10, Def2 ; ::_thesis: verum end; end; end; theorem :: ARYTM_1:25 for x, y, z being Element of REAL+ st x <=' y & z <=' y holds (y -' z) - x = (y -' x) - z proof let x, y, z be Element of REAL+ ; ::_thesis: ( x <=' y & z <=' y implies (y -' z) - x = (y -' x) - z ) assume that A1: x <=' y and A2: z <=' y ; ::_thesis: (y -' z) - x = (y -' x) - z percases ( x + z <=' y or ( not x + z <=' y & y <=' x ) or ( not x + z <=' y & y <=' z ) or ( not x + z <=' y & not y <=' x & not y <=' z ) ) ; supposeA3: x + z <=' y ; ::_thesis: (y -' z) - x = (y -' x) - z then z <=' y -' x by A1, Lm8; then A4: (y -' x) -' z = (y -' x) - z by Def2; x <=' y -' z by A2, A3, Lm8; then (y -' z) -' x = (y -' z) - x by Def2; hence (y -' z) - x = (y -' x) - z by A4, Lm10; ::_thesis: verum end; supposethat A5: not x + z <=' y and A6: y <=' x ; ::_thesis: (y -' z) - x = (y -' x) - z A7: not x <=' y -' z by A2, A5, Lm8; A8: not z <=' y -' x by A1, A5, Lm8; A9: x = y by A1, A6, Th4; then x -' (x -' z) = z by A2, Lm6 .= z -' (x -' x) by Lm3, Lm4 ; hence (y -' z) - x = [{},(z -' (y -' x))] by A7, A9, Def2 .= (y -' x) - z by A8, Def2 ; ::_thesis: verum end; supposethat A10: not x + z <=' y and A11: y <=' z ; ::_thesis: (y -' z) - x = (y -' x) - z A12: not x <=' y -' z by A2, A10, Lm8; A13: not z <=' y -' x by A1, A10, Lm8; A14: z = y by A2, A11, Th4; x -' (z -' z) = x by Lm3, Lm4 .= z -' (z -' x) by A1, A14, Lm6 ; hence (y -' z) - x = [{},(z -' (y -' x))] by A12, A14, Def2 .= (y -' x) - z by A13, Def2 ; ::_thesis: verum end; supposethat A15: not x + z <=' y and A16: ( not y <=' x & not y <=' z ) ; ::_thesis: (y -' z) - x = (y -' x) - z A17: not z <=' y -' x by A1, A15, Lm8; ( not x <=' y -' z & x -' (y -' z) = z -' (y -' x) ) by A15, A16, Lm8, Lm13; hence (y -' z) - x = [{},(z -' (y -' x))] by Def2 .= (y -' x) - z by A17, Def2 ; ::_thesis: verum end; end; end; theorem :: ARYTM_1:26 for z, y, x being Element of REAL+ st z <=' y holds x *' (y -' z) = (x *' y) - (x *' z) proof let z, y, x be Element of REAL+ ; ::_thesis: ( z <=' y implies x *' (y -' z) = (x *' y) - (x *' z) ) assume z <=' y ; ::_thesis: x *' (y -' z) = (x *' y) - (x *' z) then x *' z <=' x *' y by Th8; then (x *' y) - (x *' z) = (x *' y) -' (x *' z) by Def2; hence x *' (y -' z) = (x *' y) - (x *' z) by Lm14; ::_thesis: verum end; theorem Th27: :: ARYTM_1:27 for z, y, x being Element of REAL+ st not z <=' y & x <> {} holds [{},(x *' (z -' y))] = (x *' y) - (x *' z) proof let z, y, x be Element of REAL+ ; ::_thesis: ( not z <=' y & x <> {} implies [{},(x *' (z -' y))] = (x *' y) - (x *' z) ) assume ( not z <=' y & x <> {} ) ; ::_thesis: [{},(x *' (z -' y))] = (x *' y) - (x *' z) then A1: not x *' z <=' x *' y by Lm2; thus [{},(x *' (z -' y))] = [{},((x *' z) -' (x *' y))] by Lm14 .= (x *' y) - (x *' z) by A1, Def2 ; ::_thesis: verum end; theorem :: ARYTM_1:28 for y, z, x being Element of REAL+ st y -' z <> {} & z <=' y & x <> {} holds (x *' z) - (x *' y) = [{},(x *' (y -' z))] proof let y, z, x be Element of REAL+ ; ::_thesis: ( y -' z <> {} & z <=' y & x <> {} implies (x *' z) - (x *' y) = [{},(x *' (y -' z))] ) assume y -' z <> {} ; ::_thesis: ( not z <=' y or not x <> {} or (x *' z) - (x *' y) = [{},(x *' (y -' z))] ) then A1: y <> z by Lm3; assume z <=' y ; ::_thesis: ( not x <> {} or (x *' z) - (x *' y) = [{},(x *' (y -' z))] ) then not y <=' z by A1, Th4; hence ( not x <> {} or (x *' z) - (x *' y) = [{},(x *' (y -' z))] ) by Th27; ::_thesis: verum end;