:: Complex Numbers - Basic Theorems
::  by Library Committee
::
:: Received April 10, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XCMPLX_0, ORDINAL1, ARYTM_3, CARD_1, RELAT_1, ARYTM_1;
 notations ORDINAL1, NUMBERS, XCMPLX_0;
 constructors NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0;
 registrations XCMPLX_0, XXREAL_0, XREAL_0, ORDINAL1, XBOOLE_0;
 requirements SUBSET, BOOLE, NUMERALS, ARITHM;
 theorems XCMPLX_0;

begin

reserve a, b, c, d, e for complex number;

:: '+' operation only

theorem :: AXIOMS'13
  a + (b + c) = (a + b) + c;

theorem :: REAL_1'10
  a + c = b + c implies a = b;

theorem :: INT_1'24
  a = a + b implies b = 0;

:: using operation '*'

theorem Th4:
  a * (b * c) = (a * b) * c;

theorem :: REAL_1'9
  c <> 0 & a * c = b * c implies a = b
proof
  assume
A1: c<>0;
  assume a * c = b * c;
  then a * (c * c") = b * c * c" by Th4;
  then a * 1 = b * c * c" by A1,XCMPLX_0:def 7;
  then a = b * (c * c");
  then a = b * 1 by A1,XCMPLX_0:def 7;
  hence thesis;
end;

theorem :: REAL_1'23  :: right to left - requirements REAL
  a*b=0 implies a=0 or b=0;

theorem Th7: :: REAL_2'37
  b <> 0 & a * b = b implies a = 1
proof
  assume that
A1: b<>0 and
A2: a*b=b;
  a*b*b"=1 by A1,A2,XCMPLX_0:def 7;
  then a*1=1 by A2,Th4;
  hence thesis;
end;

:: operations '+' and '*' only

theorem :: AXIOMS'18
  a * (b + c) = a * b + a * c;

theorem :: REAL_2'99_1
  (a + b + c) * d = a * d + b * d + c * d;

theorem :: REAL_2'101_1
  (a + b) * (c + d) = a * c + a * d + b * c + b * d;

theorem :: SQUARE_1'5
  2 * a = a + a;

theorem :: REAL_2'88_1
  3 * a = a + a + a;

theorem :: REAL_2'88_2
  4 * a = a + a + a + a;

:: using operation '-'

theorem :: REAL_1'36
  a - a = 0;

theorem :: SQUARE_1'8
  a - b = 0 implies a = b;

theorem :: REAL_2'1
  b - a = b implies a = 0;

:: 2 times '-'

theorem :: REAL_2'17_2
  a = a - (b - b);

theorem :: SEQ_4'3
  a - (a - b) = b;

theorem :: REAL_2'2_3
  a - c = b - c implies a = b;

theorem :: REAL_2'2_5
  c - a = c - b implies a = b;

theorem :: REAL_2'24_1
  a - b - c = a - c - b;

theorem :: REAL_2'29_1
  a - c = (a - b) - (c - b);

theorem :: JGRAPH_6'1_1
  (c - a) - (c - b) = b - a;

theorem :: REAL_2'15
  a - b = c - d implies a - c = b - d;

:: using '-' and '+'

Lm1: a"*b"=(a*b)"
proof
  per cases;
  suppose
A1: a = 0 or b = 0;
    then a" = 0 or b" = 0;
    hence thesis by A1;
  end;
  suppose that
A2: a<>0 and
A3: b<>0;
    thus a"*b"=a"*b"*1 .=a"*b"*((a*b)*(a*b)") by A2,A3,XCMPLX_0:def 7
      .=a"*a*(b"*b)*(a*b)"
      .=1*(b"*b)*(a*b)" by A2,XCMPLX_0:def 7
      .=1*(a*b)" by A3,XCMPLX_0:def 7
      .=(a*b)";
  end;
end;

Lm2: a/(b/c)=(a*c)/b
proof
  thus a/(b/c)=a/(b*c") by XCMPLX_0:def 9
    .=a*(b*c")" by XCMPLX_0:def 9
    .=a*(b"*c"") by Lm1
    .=a*c*b"
    .=(a*c)/b by XCMPLX_0:def 9;
end;

Lm3: b<>0 implies a/b*b=a
proof
  assume
A1: b<>0;
  thus a/b*b=a*b"*b by XCMPLX_0:def 9
    .=a*(b"*b)
    .=a*1 by A1,XCMPLX_0:def 7
    .=a;
end;

Lm4: 1/a=a"
proof
  thus 1/a= 1 * a" by XCMPLX_0:def 9
    .=a";
end;

Lm5: a<>0 implies a/a = 1
proof
  assume
A1: a<>0;
  thus a/a=a*a" by XCMPLX_0:def 9
    .=1 by A1,XCMPLX_0:def 7;
end;

:: using operations '-' and '+'

theorem :: REAL_2'17_1
  a = a + (b - b);

theorem :: REAL_1'30
  a = a + b - b;

theorem :: SQUARE_1'6
  a = a - b + b;

theorem :: REAL_2'28_1
  a + c = a + b + (c - b);

:: 2 times '-'

theorem :: REAL_2'22_1, INT_1'1, REAL_1'17
  a + b - c = a - c + b;

theorem :: REAL_2'23_1
  a - b + c = c - b + a;

theorem :: REAL_2'28_2
  a + c = a + b - (b - c);

theorem :: REAL_2'29_3
  a - c = a + b - (c + b);

theorem :: REAL_2'13
  a + b = c + d implies a - c = d - b;

theorem :: REAL_2'14
  a - c = d - b implies a + b = c + d;

theorem :: REAL_2'16
  a + b = c - d implies a + d = c - b;

:: 3 times '-'

theorem :: REAL_1'27
  a - (b + c) = a - b - c;

theorem :: REAL_1'28
  a - (b - c) = a - b + c;

theorem :: REAL_2'18
  a - (b - c) = a + (c - b);

theorem :: REAL_2'29_2
  a - c = (a - b) + (b - c);

theorem :: REAL_1'29
  a * (b - c) = a * b - a * c;

theorem :: REAL_2'98
  (a - b) * (c - d) = (b - a) * (d - c);

theorem :: REAL_2'99_4
  (a - b - c) * d = a * d - b * d - c * d;

:: using operations '-' and '*', '+'

theorem :: REAL_2'99_2
  (a + b - c) * d = a * d + b * d - c * d;

theorem :: REAL_2'99_3
  (a - b + c) * d = a * d - b * d + c * d;

theorem :: REAL_2'101_2
  (a + b) * (c - d) = a * c - a * d + b * c - b * d;

theorem :: REAL_2'101_3
  (a - b) * (c + d) = a * c + a * d - b * c - b * d;

theorem :: REAL_2'101_4
  (a - b) * (e - d) = a * e - a * d - b * e + b * d;

:: using operation '/'

theorem :: REAL_2'67_1
  a / b / c = a / c / b
proof
  thus a/b/c =a*b"/c by XCMPLX_0:def 9
    .=a*b"*c" by XCMPLX_0:def 9
    .=a*c"*b"
    .=a/c*b" by XCMPLX_0:def 9
    .=a/c/b by XCMPLX_0:def 9;
end;

:: 0

theorem Th49: :: REAL_2'19
  a / 0 = 0
proof
  thus a/0 = a*0" by XCMPLX_0:def 9
    .= 0;
end;

theorem :: REAL_2'42_2
  a <> 0 & b <> 0 implies a / b <> 0;

:: 2 times '/'

theorem :: REAL_2'62_4
  b <> 0 implies a = a / (b / b)
proof
A1: a=a/1;
  assume b<>0;
  hence thesis by A1,Lm5;
end;

Lm6: (a/b) * (c/d) = (a*c)/(b*d)
proof
  thus (a/b) * (c/d) =(a*b")*(c/d) by XCMPLX_0:def 9
    .=(a*b")*(c*d") by XCMPLX_0:def 9
    .=(a*c)*(b"*d")
    .=(a*c)*(b*d)" by Lm1
    .=(a*c)/(b*d) by XCMPLX_0:def 9;
end;

Lm7: (a/b)"=b/a
proof
  per cases;
  suppose
A1: a = 0;
    hence (a/b)" =b*0" .=b/a by A1,XCMPLX_0:def 9;
  end;
  suppose
A2: b = 0;
    hence (a/b)" =(a*0")" by XCMPLX_0:def 9
      .=b/a by A2;
  end;
  suppose
A3: a<>0 & b<>0;
    (a/b) * (b/a) =(a*b)/(a*b) by Lm6;
    then (a/b)*(b/a) = 1 by A3,Lm5;
    hence thesis by A3,XCMPLX_0:def 7;
  end;
end;

Lm8: a*(b/c) = (a*b)/c
proof
  thus a*(b/c) = (a/1)*(b/c) .= (a*b)/(1*c) by Lm6
    .= (a*b)/c;
end;

theorem :: TOPREAL6'5
  a <> 0 implies a / (a / b) = b
proof
  assume
A1: a <> 0;
  thus a/(a/b) = a * (a/b)" by XCMPLX_0:def 9
    .= a * (b/a) by Lm7
    .= a*b/a by Lm8
    .= a/a*b by Lm8
    .= 1 * b by A1,Lm5
    .= b;
end;

theorem :: REAL_2'31
  c <> 0 & a / c = b / c implies a = b
proof
  assume that
A1: c<>0 and
A2: a/c =b/c;
  a=b/c*c by A1,A2,Lm3;
  hence thesis by A1,Lm3;
end;

:: 3 times '/'

Lm9: b<>0 implies a=a*b/b
proof
A1: a=a*1;
  assume b<>0;
  then a=a*(b/b) by A1,Lm5;
  then a=a*(b*b") by XCMPLX_0:def 9;
  then a=a*b*b";
  hence thesis by XCMPLX_0:def 9;
end;

theorem :: REAL_2'74
  a / b <> 0 implies b = a / (a / b)
proof
  assume
A1: a/b<>0;
  then b<>0 by Th49;
  then a/b*b = a by Lm3;
  hence thesis by A1,Lm9;
end;

:: 4 times '/'

Lm10: c<>0 implies a/b=(a*c)/(b*c)
proof
  assume
A1: c<>0;
  thus a/b =a*b"*1 by XCMPLX_0:def 9
    .=a*b"*(c*c") by A1,XCMPLX_0:def 7
    .=(a*c)*(b"*c")
    .=(a*c)*(b*c)" by Lm1
    .=(a*c)/(b*c) by XCMPLX_0:def 9;
end;

theorem :: REAL_2'55_1
  c <> 0 implies a / b = (a / c) / (b / c)
proof
  assume c<>0;
  hence a/b=(a*c")/(b*c") by Lm10
    .=(a/c)/(b*c") by XCMPLX_0:def 9
    .=(a/c)/(b/c) by XCMPLX_0:def 9;
end;

:: 1

theorem :: SQUARE_1'16
  1 / (1 / a) = a
proof
  thus 1/(1/a) = (1*a) /1 by Lm2
    .= a;
end;

Lm11: (a*b")"=a"*b
proof
  thus (a*b")"=a"*b"" by Lm1
    .=a"*b;
end;

theorem :: REAL_2'48_1
  1 / (a / b) = b / a
proof
  thus 1/(a/b)=1/(a*b") by XCMPLX_0:def 9
    .=(a*b")" by Lm4
    .=b*a" by Lm11
    .=b/a by XCMPLX_0:def 9;
end;

theorem Th58:
  a / b = 1 implies a = b
proof
  assume
A1: a/b = 1;
  then b <> 0 by Th49;
  then a=1*b by A1,Lm3;
  hence thesis;
end;

Lm12: a"=b" implies a=b
proof
  assume a"=b";
  then a=b"";
  hence thesis;
end;

theorem Th59: :: REAL_2'33_2
  1 / a = 1 / b implies a = b
proof
  assume 1/a=1/b;
  then a"=1/b by Lm4;
  then a" = b" by Lm4;
  hence thesis by Lm12;
end;

:: 0 and 1

theorem :: REAL_1'37
  a <> 0 implies a / a = 1 by Lm5;

theorem :: REAL_2'39
  b <> 0 & b / a = b implies a = 1
proof
  assume that
A1: b<>0 and
A2: b/a=b;
  a <> 0 by A1,A2,Th49;
  then b=b*a by A2,Lm3;
  hence thesis by A1,Th7;
end;

:: using operations '/' and '+'

theorem Th62: :: REAL_1'40_1
  a / c + b / c = (a + b) / c
proof
  thus a/c + b/c =a*c" + b/c by XCMPLX_0:def 9
    .= a*c" + b*c" by XCMPLX_0:def 9
    .= (a+b)*c"
    .= (a+b)/c by XCMPLX_0:def 9;
end;

theorem :: REAL_2'100_1
  (a + b + e) / d = a / d + b / d + e / d
proof
  thus (a+b+e)/d=(a+b)/d+e/d by Th62
    .=a/d+b/d+e/d by Th62;
end;

:: 2

theorem :: SQUARE_1'15
  (a + a) / 2 = a;

theorem :: SEQ_2'2_1
  a/2 + a/2 = a;

theorem :: TOPREAL3'4
  a = (a + b) / 2 implies a = b;

:: 3

theorem :: REAL_2'89_1
  (a + a + a)/3 = a;

theorem :: SEQ_4'5
  a/3 + a/3 + a/3 = a;

:: 4

theorem :: REAL_2'89_2
  (a + a + a + a) / 4 = a;

theorem :: REAL_2'90
  a/4 + a/4 + a/4 + a/4 = a;

theorem :: SEQ_2'2_2
  a / 4 + a / 4 = a / 2;

theorem :: REAL_2'89_3
  (a + a) / 4 = a / 2;

:: using operations '/' and '*'

theorem :: REAL_2'35_1
  a * b = 1 implies a = 1 / b
proof
  assume
A1: a*b=1;
  then b<>0;
  then a*1=1*b" by A1,XCMPLX_0:def 7;
  hence thesis by Lm4;
end;

theorem :: SQUARE_1'18
  a * (b / c) = (a * b) / c by Lm8;

theorem :: REAL_2'80_1
  a / b * e = e / b * a
proof
  thus a/b*e=a*e/b by Lm8
    .=e/b*a by Lm8;
end;

:: 3 times '/'

theorem :: REAL_1'35
  (a / b) * (c / d) = (a * c) / (b * d) by Lm6;

theorem :: REAL_1'42
  a / (b / c) = (a * c) / b by Lm2;

Lm13: (a/b)/(c/d)=(a*d)/(b*c)
proof
  thus (a/b)/(c/d) = (a/b) * (c/d)" by XCMPLX_0:def 9
    .=(a/b) * (d/c) by Lm7
    .=(a*d)/(b*c) by Lm6;
end;

theorem Th78: :: SQUARE_1'17
  a / (b * c) = a / b / c
proof
  thus a/(b*c) = a*1/(b*c) .= a/b/(c/1) by Lm13
    .= a/b/c;
end;

theorem :: REAL_2'61_1
  a / (b / c) = a * (c / b)
proof
  thus a/(b/c)=(a*c)/b by Lm2
    .=a*c*b" by XCMPLX_0:def 9
    .=a*(c*b")
    .=a*(c/b) by XCMPLX_0:def 9;
end;

theorem :: REAL_2'61_2
  a / (b / c) = c / b * a
proof
  a/(b/c)=(a*c)/b by Lm2
    .=a*c*b" by XCMPLX_0:def 9
    .=a*(c*b")
    .=a*(c/b) by XCMPLX_0:def 9;
  hence thesis;
end;

theorem Th81: :: REAL_2'61_3
  a / (b / e) = e * (a / b)
proof
  thus a/(b/e)=(a*e)/b by Lm2
    .=e*a*b" by XCMPLX_0:def 9
    .=e*(a*b")
    .=e*(a/b) by XCMPLX_0:def 9;
end;

theorem :: REAL_2'61_4
  a / (b / c) = a / b * c
proof
  a/(b/c)=(a*c)/b by Lm2
    .=c*a*b" by XCMPLX_0:def 9
    .=c*(a*b")
    .=c*(a/b) by XCMPLX_0:def 9;
  hence thesis;
end;

Lm14: a*(1/b)=a/b
proof
  thus a/b=a*b" by XCMPLX_0:def 9
    .=a*(1/b) by Lm4;
end;

Lm15: 1/c*(a/b)=a/(b*c)
proof
  a/b/c =c"*(a/b) by XCMPLX_0:def 9
    .=1/c*(a/b) by Lm4;
  hence thesis by Th78;
end;

theorem :: REAL_2'70
  (a * b) / (c * d) = (a / c * b) / d
proof
  thus a*b/(c*d)=1/c*(a*b/d) by Lm15
    .=1/c*(a*b)/d by Lm8
    .=1/c*a*b/d
    .=a/c*b/d by Lm14;
end;

:: 4 times '/'

theorem :: REAL_1'82
  (a / b) / (c / d) = (a * d) / (b * c) by Lm13;

theorem :: REAL_2'53
  (a / c) * (b / d) = (a / d) * (b / c)
proof
  thus a/c*(b/d)=a*b/(d*c) by Lm6
    .=a/d*(b/c) by Lm6;
end;

theorem :: IRRAT_1'5
  a / (b * c * (d / e)) = (e / c) * (a / (b * d))
proof
  thus a/(b*c*(d/e)) = a/(b*c*(d*e")) by XCMPLX_0:def 9
    .= a/(c*(b*d*e"))
    .= a/(c*((b*d)/e)) by XCMPLX_0:def 9
    .= a/((b*d)/(e/c)) by Th81
    .= (e/c)*(a/(b*d)) by Th81;
end;

:: 0

theorem :: REAL_1'43
  b <> 0 implies a / b * b = a by Lm3;

theorem :: REAL_2'62_1
  b <> 0 implies a = a * (b / b)
proof
A1: a=a*1;
  assume b<>0;
  hence thesis by A1,Lm5;
end;

theorem :: REAL_2'62_2
  b <> 0 implies a = a * b / b by Lm9;

theorem :: REAL_2'78
  b <> 0 implies a * c = a * b * (c / b)
proof
  assume
A1: b<>0;
  thus a*c =a*1*c .=a*(b*b")*c by A1,XCMPLX_0:def 7
    .=a*b*(b"*c)
    .=a*b*(c/b) by XCMPLX_0:def 9;
end;

:: 2 times '/'

theorem :: REAL_1'38
  c <> 0 implies a / b = (a * c) / (b * c) by Lm10;

theorem :: REAL_2'55_2
  c <> 0 implies a / b = a / (b * c) * c
proof
  assume
A1: c<>0;
  c*(a/(b*c))=c*((a*1)/(b*c)) .=c*(1/c*(a/b)) by Lm6
    .=1/c*c*(a/b)
    .=1*(a/b) by A1,Lm3
    .=a/b;
  hence thesis;
end;

theorem :: REAL_2'79
  b <> 0 implies a * c = a * b / (b / c)
proof
  assume
A1: b<>0;
  thus a*c =a*1*c .=a*(b*b")*c by A1,XCMPLX_0:def 7
    .=a*b*(b"*c)
    .=a*b*(b*c")" by Lm11
    .=a*b/(b*c") by XCMPLX_0:def 9
    .=a*b/(b/c) by XCMPLX_0:def 9;
end;

theorem Th94: :: REAL_2'75
  c <> 0 & d <> 0 & a * c = b * d implies a / d = b / c
proof
  assume that
A1: c<>0 and
A2: d<>0;
  assume a*c = b*d;
  then a=b*d/c by A1,Lm9;
  then a=d*(b/c) by Lm8;
  hence thesis by A2,Lm9;
end;

theorem Th95: :: REAL_2'76
  c <> 0 & d<>0 & a/d=b/c implies a*c = b*d
proof
  assume that
A1: c<>0 and
A2: d<>0 and
A3: a/d=b/c;
  c*(a/d)=b by A1,A3,Lm3;
  then a*c/d=b by Lm8;
  hence thesis by A2,Lm3;
end;

theorem :: REAL_2'77
  c <> 0 & d <> 0 & a * c = b / d implies a * d = b / c
proof
  assume that
A1: c<>0 and
A2: d<>0;
  assume a*c =b/d;
  then a*c*d=b by A2,Lm3;
  then a*d*c =b;
  hence thesis by A1,Lm9;
end;

:: 3 times '/'

theorem :: REAL_2'55_3
  c <> 0 implies a / b = c * (a / c / b)
proof
  assume
A1: c<>0;
  thus a/b=a*b" by XCMPLX_0:def 9
    .=c*(a/c)*b" by A1,Lm3
    .=c*(a/c*b")
    .=c*(a/c/b) by XCMPLX_0:def 9;
end;

theorem :: REAL_2'55
  c <> 0 implies a / b = a / c * (c / b)
proof
  assume
A1: c<>0;
  thus a/b=a*b" by XCMPLX_0:def 9
    .=a/c*c*b" by A1,Lm3
    .=a/c*(c*b")
    .=a/c*(c/b) by XCMPLX_0:def 9;
end;

:: 1

theorem :: REAL_2'56:
  a * (1 / b) = a / b by Lm14;

Lm16: 1/a"=a
proof
  1/a"=a"" by Lm4
    .=a;
  hence thesis;
end;

theorem :: REAL_2'57
  a / (1 / b) = a * b
proof
  thus a/(1/b)=a/b" by Lm4
    .=a*(1/b") by Lm14
    .=a*b by Lm16;
end;

theorem :: REAL_2'80_3
  a / b * c = 1 / b * c * a
proof
  a/b*c = 1/b*a*c by Lm14;
  hence thesis;
end;

:: 3 times '/'

theorem :: REAL_2'51
  (1 / a) * (1 / b) = 1 / (a * b)
proof
  thus (1/a)*(1/b)=a"*(1/b) by Lm4
    .=a"*b" by Lm4
    .=(a*b)" by Lm1
    .=1/(a*b) by Lm4;
end;

theorem :: REAL_2'67_4
  1 / c * (a / b) = a / (b * c) by Lm15;

:: 4 times '/'

theorem :: REAL_2'67_2
  a / b / c = 1 / b * (a / c)
proof
  a/b/c =a*b"/c by XCMPLX_0:def 9
    .=a*b"*c" by XCMPLX_0:def 9
    .=a*c"*b"
    .=a/c*b" by XCMPLX_0:def 9
    .=a/c/b by XCMPLX_0:def 9;
  hence a/b/c =b"*(a/c) by XCMPLX_0:def 9
    .=1/b*(a/c) by Lm4;
end;

theorem :: REAL_2'67_3
  a / b / c = 1 / c * (a / b)
proof
  thus a/b/c =c"*(a/b) by XCMPLX_0:def 9
    .=1/c*(a/b) by Lm4;
end;

:: 1 and 0

theorem Th106: :: REAL_1'34
  a <> 0 implies a * (1 / a) = 1
proof
  assume
A1: a<>0;
  thus a*(1/a)=a*a" by Lm4
    .=1 by A1,XCMPLX_0:def 7;
end;

theorem :: REAL_2'62_3
  b <> 0 implies a = a * b * (1 / b)
proof
A1: a=a*1;
  assume b<>0;
  then a=a*(b/b) by A1,Lm5;
  then a=a*(b*b") by XCMPLX_0:def 9
    .=a*(b*(1/b)) by Lm4;
  hence thesis;
end;

theorem :: REAL_2'62_6
  b <> 0 implies a = a * (1 / b * b)
proof
  assume
A1: b<>0;
  thus a=a*1 .=a*(1/b*b) by A1,Lm3;
end;

theorem :: REAL_2'62_7
  b <> 0 implies a = a * (1 / b) * b
proof
  assume
A1: b<>0;
  a=a*1 .=a*(1/b*b) by A1,Lm3;
  hence thesis;
end;

theorem :: REAL_2'62_5
  b <> 0 implies a = a / (b * (1 / b))
proof
  assume
A1: b<>0;
  thus a=a/1 .=a/(b*(1/b)) by A1,Th106;
end;

theorem :: REAL_2'42_4
  a <> 0 & b <> 0 implies 1 / (a * b) <> 0;

theorem :: JGRAPH_2'1
  a <> 0 & b <> 0 implies (a / b) * (b / a) = 1
proof
  assume
A1: a<>0 & b<>0;
  (b/a)=(a/b)" by Lm7;
  hence thesis by A1,XCMPLX_0:def 7;
end;

:: using operations '*', '+' and '/'

theorem Th113: :: REAL_2'65
  b <> 0 implies a / b + c = (a + b * c) / b
proof
  assume
A1: b<>0;
  a/b+c =a/b+1*c .=a/b+b*b"*c by A1,XCMPLX_0:def 7
    .=a/b+b*c*b"
    .=a/b+c*b/b by XCMPLX_0:def 9
    .=(a+c*b)/b by Th62;
  hence thesis;
end;

theorem Th114: :: REAL_2'92
  c <> 0 implies a + b = c * (a / c + b / c)
proof
  assume
A1: c<>0;
  hence a+b=c*(a/c)+b by Lm3
    .=c*(a/c)+c*(b/c) by A1,Lm3
    .=c*(a/c+b/c);
end;

theorem Th115: :: REAL_2'94
  c <> 0 implies a + b = (a * c + b * c) / c
proof
  assume
A1: c<>0;
  hence a+b=a*c/c+b by Lm9
    .=a*c/c+b*c/c by A1,Lm9
    .=(a*c+b*c)/c by Th62;
end;

theorem Th116: :: REAL_1'41_1
  b <> 0 & d <> 0 implies a / b + c / d =(a * d + c * b) / (b * d )
proof
  assume
A1: b<>0;
  assume d<>0;
  hence a/b + c/d=(a*d)/(b*d) + c/d by Lm10
    .=(a*d)/(b*d) + (c*b)/(b*d) by A1,Lm10
    .=(a*d + c*b)/(b*d) by Th62;
end;

theorem Th117: :: REAL_2'96
  a <> 0 implies a + b = a * (1 + b / a)
proof
  assume
A1: a<>0;
  hence a+b=a*(a/a+b/a) by Th114
    .=a*(1+b/a) by A1,Lm5;
end;

:: 2

theorem :: REAL_2'91_1
  a / (2 * b) + a / (2 * b) = a / b
proof
  thus a/(2*b)+a/(2*b)=(a+a)/(2*b) by Th62
    .=2*a/(2*b)
    .=a/b by Lm10;
end;

:: 3

theorem :: REAL_2'91_2
  a / (3 * b) + a / (3 * b) + a / (3 * b) = a / b
proof
  thus a/(3*b)+a/(3*b)+a/(3*b)=(a+a)/(3*b)+a/(3*b) by Th62
    .=(a+a+a)/(3*b) by Th62
    .=3*a/(3*b)
    .=a/b by Lm10;
end;

:: using operations '-' and '/'

Lm17: -a/b=(-a)/b
proof
  thus -a/b=-(a*b") by XCMPLX_0:def 9
    .=(-a)*b"
    .=(-a)/b by XCMPLX_0:def 9;
end;

theorem Th120: :: REAL_1'40_2
  a / c - b / c = (a - b) / c
proof
  thus a/c - b/c = a/c+ -b/c .=a/c+(-b)/c by Lm17
    .=(a+ -b)/c by Th62
    .=(a-b)/c;
end;

theorem :: TOPREAL6'4
  a - a / 2 = a / 2;

theorem :: REAL_2'100_4
  (a - b - c) / d = a / d - b / d - c / d
proof
  thus (a-b-c)/d=(a-b)/d-c/d by Th120
    .=a/d-b/d-c/d by Th120;
end;

theorem :: REAL_2'82
  b <> 0 & d <> 0 & b <> d & a / b = e / d implies a / b = (a - e) / (b - d )
proof
  assume that
A1: b<>0 and
A2: d<>0 and
A3: b<>d and
A4: a/b=e/d;
  a*d=e*b by A1,A2,A4,Th95;
  then
A5: a*(b-d)=(a-e)*b;
  b-d<>0 by A3;
  hence thesis by A1,A5,Th94;
end;

:: using operations '-', '/' and '+'

theorem :: REAL_2'100_2
  (a + b - e) / d = a / d + b / d - e / d
proof
  thus (a+b-e)/d=(a+b)/d-e/d by Th120
    .=a/d+b/d-e/d by Th62;
end;

theorem :: REAL_2'100_3
  (a - b + e) / d = a / d - b / d + e / d
proof
  thus (a-b+e)/d=(a-b)/d+e/d by Th62
    .=a/d-b/d+e/d by Th120;
end;

:: using operations '-', '/' and '*'

theorem Th126: :: REAL_2'66_1
  b <> 0 implies a / b - e = (a - e * b) / b
proof
  assume
A1: b<>0;
  thus a/b-e=a/b+-e .=(a+(-e)*b)/b by A1,Th113
    .=(a-e*b)/b;
end;

theorem :: REAL_2'66_2
  b <> 0 implies c - a / b = (c * b - a) / b
proof
  assume
A1: b<>0;
  thus c-a/b = -(a/b-c) .=-(a-c*b)/b by A1,Th126
    .=(-(a-c*b))/b by Lm17
    .=(c*b-a)/b;
end;

theorem :: REAL_2'93
  c <> 0 implies a - b = c * (a / c - b / c)
proof
  assume
A1: c<>0;
  hence a-b=c*(a/c)-b by Lm3
    .=c*(a/c)-c*(b/c) by A1,Lm3
    .=c*(a/c-b/c);
end;

theorem :: REAL_2'95
  c <> 0 implies a - b = (a * c - b * c) / c
proof
  assume
A1: c<>0;
  thus a-b=a+-b .=(a*c+(-b)*c)/c by A1,Th115
    .=(a*c-b*c)/c;
end;

theorem :: REAL_1'41_2
  b <> 0 & d <> 0 implies a / b - c / d = (a * d - c * b) / (b * d)
proof
  assume
A1: b<>0;
  assume
A2: d<>0;
  thus a/b - c/d =a/b + -c/d .=a/b + (-c)/d by Lm17
    .=(a*d + (-c)*b)/(b*d) by A1,A2,Th116
    .=(a*d - c*b)/(b*d);
end;

theorem :: REAL_2'97
  a <> 0 implies a - b = a * (1 - b / a)
proof
  assume
A1: a<>0;
  thus a-b=a+-b .=a*(1+(-b)/a) by A1,Th117
    .=a*(1+-b/a) by Lm17
    .=a*(1-b/a);
end;

:: using operation '-', '/', '*' and '+'

theorem :: POLYEQ_1'24
  a <> 0 implies c = (a * c + b - b) / a by Lm9;

:: using unary operation '-'

theorem :: REAL_2'2_2
  -a = -b implies a = b;

theorem :: REAL_1'22:  :: right to left - requirements REAL
  -a = 0 implies a = 0;

theorem :: REAL_2'2_1
  a + -b = 0 implies a = b;

theorem :: REAL_2'11
  a = a + b + -b;

theorem :: REAL_2'17_1
  a = a + (b + -b);

theorem :: INT_1'3
  a = (- b + a) + b;

theorem :: REAL_2'6_1
  - (a + b) = -a + -b;

theorem :: REAL_2'9_2
  - (-a + b) = a + -b;

theorem :: REAL_2'10_2
  a+b=-(-a+-b);

:: using unary and binary operation '-'

theorem :: REAL_1'83
  -(a - b) = b - a;

theorem :: REAL_2'5
  - a - b = - b - a;

theorem :: REAL_2'17_4
  a = - b - (- a - b);

:: binary '-' 4 times

theorem :: REAL_2'26_1
  - a - b - c = - a - c - b;

theorem :: REAL_2'26_2
  - a - b - c = - b - c - a;

theorem :: REAL_2'26_4
  - a - b - c = - c - b - a;

theorem :: JGRAPH_6'1_2
  (c - a) - (c - b) = - (a - b);

:: 0

theorem :: REAL_1'19
  0 - a = - a;

:: using unary and binary operations '-' and '+'

theorem :: REAL_2'10_3
  a + b = a - - b;

theorem :: REAL_2'17_3
  a = a - (b + -b);

theorem :: REAL_2'2_4
  a - c = b + - c implies a = b;

theorem :: REAL_2'2_6
  c - a = c + - b implies a = b;

:: '+' 3 times

theorem :: REAL_2'22_2
  a + b - c = - c + a + b;

theorem :: REAL_2'23_2
  a - b + c = - b + c + a;

theorem :: REAL_2'20_2
  a - (- b - c) = a + b + c;

:: binary '-' 3 times

theorem :: REAL_2'20_1
  a - b - c = - b - c + a;

theorem :: REAL_2'24_3
  a - b - c = - c + a - b;

theorem :: REAL_2'24_4
  a - b - c = - c - b + a;

:: using unary and binary operations '-' and '+'

theorem :: REAL_2'6_2
  - (a + b) = - b - a;

theorem :: REAL_2'8
  - (a - b) = - a + b;

theorem :: REAL_2'9_1
  -(-a+b)=a-b;

theorem :: REAL_2'10_1
  a + b = -(- a - b);

theorem :: REAL_2'25_1
  - a + b - c = - c + b - a;

:: using unary and binary operations '-' and '+' (both '-' 2 times)

theorem :: REAL_2'25_2
  - a + b - c = - c - a + b;

theorem :: REAL_2'27_1
  - (a + b + c) = - a - b - c;

theorem :: REAL_2'27_2
  - (a + b - c) = - a - b + c;

theorem :: REAL_2'27_3
  - (a - b + c) = - a + b - c;

theorem :: REAL_2'27_5
  - (a - b - c) = - a + b + c;

theorem :: REAL_2'27_4
  - (- a + b + c) = a - b - c;

theorem :: REAL_2'27_6
  - (- a + b - c) = a - b + c;

theorem :: REAL_2'27_7
  - (- a - b + c) = a + b - c;

theorem :: REAL_2'27_8
  - (- a - b - c) = a + b + c;

:: using unary operations '-' and '*'

theorem :: REAL_1'21_1
  (- a) * b = -(a * b);

theorem :: REAL_1'21_2
  (- a) * b = a * (- b);

theorem :: REAL_2'49_1
  (- a) * (- b) = a * b;

theorem :: REAL_2'49_2
  - a * (- b) = a * b;

theorem :: REAL_2'49_3
  -(-a) * b = a * b;

theorem :: REAL_2'71_1
  (-1) * a = -a;

theorem :: REAL_2'71_2
  (- a) * (- 1) = a;

theorem Th181: :: REAL_2'38
  b<>0 & a*b=-b implies a=-1
proof
  assume that
A1: b<>0 and
A2: a*b=-b;
  a*(b*b")=(-b)*b" by A2,Th4;
  then a*1=(-b)*b" by A1,XCMPLX_0:def 7;
  hence a=-b*b" .=-1 by A1,XCMPLX_0:def 7;
end;

:: Thx

theorem Th182:
  a * a = 1 implies a = 1 or a = -1
proof
  assume a*a=1;
  then (a-1)*(a+1) =0;
  then a-1=0 or a+1=0;
  hence thesis;
end;

theorem :: TOPREAL6'3
  -a + 2 * a = a;

theorem :: REAL_2'85_1
  (a - b) * c = (b - a) * (- c);

theorem :: REAL_2'85_2
  (a - b) * c = - (b - a) * c;

theorem :: TOPREAL6'2
  a - 2 * a = -a;

:: using unary operations '-' and '/'

theorem :: REAL_1'39_1
  -a / b = (-a) / b by Lm17;

theorem Th188: :: REAL_1'39_2
  a / (- b) = -a / b
proof
  a/(-b)=(a*(-1))/((-b)*(-1)) by Lm10;
  then a/(-b)= (-a)/((-(-b))*1) .= -a/b by Lm17;
  hence thesis;
end;

theorem :: REAL_2'58_1
  - a / (- b) = a / b
proof
  thus -a/(-b)=--a/b by Th188
    .=a/b;
end;

theorem Th190: :: REAL_2'58_2
  -(- a) / b = a / b
proof
  thus -(-a)/b=--a/b by Lm17
    .=a/b;
end;

theorem :: REAL_2'58_3
  (- a) / (- b) = a / b
proof
  -(-a)/b=a/b by Th190;
  hence thesis by Th188;
end;

theorem :: REAL_2'58
  (-a) / b = a / (-b)
proof
  thus (-a)/b=-a/b by Lm17
    .=a/(-b) by Th188;
end;

theorem :: REAL_2'71_3
  -a = a / (-1);

theorem :: REAL_2'71
  a = (- a) / (-1);

theorem :: REAL_2'34
  a / b = - 1 implies a = - b & b = - a
proof
  assume
A1: a/b=-1;
  then b <> 0 by Th49;
  then a=(-1)*b by A1,Lm3;
  hence thesis;
end;

theorem :: REAL_2'40
  b <> 0 & b / a = - b implies a = -1
proof
  assume that
A1: b<>0 and
A2: b/a=-b;
  a <> 0 by A1,A2,Th49;
  then b=(-b)*a by A2,Lm3;
  then b=-b*a;
  hence thesis by A1,A2,Th181;
end;

theorem :: REAL_2'45_2
  a <> 0 implies (-a) / a = -1
proof
  assume
A1: a<>0;
  thus (-a)/a=-a/a by Lm17
    .=-1 by A1,Lm5;
end;

theorem :: REAL_2'45_3
  a <> 0 implies a / (- a) = -1
proof
  assume
A1: a<>0;
  thus a/(-a)=-a/a by Th188
    .=-1 by A1,Lm5;
end;

Lm18: a<>0 & a=a" implies a=1 or a=-1
proof
  assume
A1: a<>0;
  assume a=a";
  then a*a=1 by A1,XCMPLX_0:def 7;
  hence thesis by Th182;
end;

theorem :: REAL_2'46_2
  a <> 0 & a = 1 / a implies a = 1 or a = -1
proof
  assume a<>0;
  then a=a" implies a=1 or a=-1 by Lm18;
  hence thesis by Lm4;
end;

theorem :: REAL_2'83:
  b <> 0 & d <> 0 & b <> -d & a / b = e / d implies a / b = (a + e) / (b + d )
proof
  assume that
A1: b<>0 and
A2: d<>0 and
A3: b<>-d and
A4: a/b=e/d;
  a*d=e*b by A1,A2,A4,Th95;
  then
A5: a*(b+d)=(a+e)*b;
  b+d<>0 by A3;
  hence thesis by A1,A5,Th94;
end;

:: using operation '"'

theorem :: REAL_2'33_1
  a" = b" implies a = b by Lm12;

theorem :: REAL_1'31
  0" = 0;

:: using '"' and '*'

theorem
  b <> 0 implies a = a*b*b"
proof
A1: a*(b*b") = a*b*b";
  assume b <> 0;
  then a*1 = a*b*b" by A1,XCMPLX_0:def 7;
  hence thesis;
end;

theorem :: REAL_1'24
  a" * b" = (a * b)" by Lm1;

theorem :: REAL_2'47_1
  (a * b")" = a" * b by Lm11;

theorem :: REAL_2'47_2
  (a" * b")" = a * b
proof
  thus (a"*b")"=a""*b"" by Lm1
    .=a*b;
end;

theorem :: REAL_2'42_1
  a <> 0 & b <> 0 implies a * b" <> 0;

theorem :: REAL_2'42_3
  a <> 0 & b <> 0 implies a" * b" <> 0;

theorem :: REAL_2'30_2
  a * b" = 1 implies a = b
proof
  assume a*b"=1;
  then a/b = 1 by XCMPLX_0:def 9;
  hence thesis by Th58;
end;

theorem :: REAL_2'35_2
  a * b = 1 implies a = b"
proof
  assume
A1: a*b=1;
  then b<>0;
  hence thesis by A1,XCMPLX_0:def 7;
end;

:: using '"', '*', and '+'

theorem Th211:
  a <> 0 & b <> 0 implies a" + b" = (a + b)*(a*b)"
proof
  assume that
A1: a <> 0 and
A2: b <> 0;
  b" = b"*1;
  then b" = b"*(a"*a) by A1,XCMPLX_0:def 7;
  then b" = (a"*b")*a;
  then
A3: b" = (a*b)"*a by Lm1;
  a" = a"*1;
  then a" = a"*(b"*b) by A2,XCMPLX_0:def 7;
  then a" = (a"*b")*b;
  then a" = (a*b)"*b by Lm1;
  hence thesis by A3;
end;

Lm19: (- a)" = -a"
proof
  thus (-a)"=1/(-a) by Lm4
    .=-1/a by Th188
    .=-a" by Lm4;
end;

:: using '"', '*', and '-'

theorem
  a <> 0 & b <> 0 implies a" - b" = (b - a)*(a*b)"
proof
  assume
A1: a <> 0 & b <> 0;
  thus a" - b" = a" + -(b") .= a" + (-b)" by Lm19
    .= (a + -b)*(a*-b)" by A1,Th211
    .= (a + -b)*(-a*b)"
    .= (a + -b)*-((a*b)") by Lm19
    .= (b - a)*(a*b)";
end;

:: using '"' and '/'

theorem :: REAL_1'81
  (a / b)" = b / a by Lm7;

theorem
  (a"/b") = b/a
proof
  thus (a"/b") = a"*b"" by XCMPLX_0:def 9
    .= b/a by XCMPLX_0:def 9;
end;

theorem :: REAL_1'33_1
  1 / a = a" by Lm4;

theorem :: REAL_1'33_2
  1 / a" = a by Lm16;

theorem :: REAL_2'36_21
  (1 / a)" = a
proof
  1/a=a" implies (1/a)"=a;
  hence thesis by Lm4;
end;

theorem :: REAL_2'33_3
  1 / a = b" implies a = b
proof
  1/a=1/b implies a=b by Th59;
  hence thesis by Lm4;
end;

:: using '"', '*', and '/'

theorem
  a/b" = a*b
proof
  thus a/b" = a*b"" by XCMPLX_0:def 9
    .= a*b;
end;

theorem
  a"*(c/b) = c/(a*b)
proof
  thus a"*(c/b) = a"*(c*b") by XCMPLX_0:def 9
    .= c*(a"*b")
    .= c*(a*b)" by Lm1
    .= c/(a*b) by XCMPLX_0:def 9;
end;

theorem
  a"/b = (a*b)"
proof
  thus a"/b = a"*b" by XCMPLX_0:def 9
    .= (a*b)" by Lm1;
end;

:: both unary operations

theorem :: REAL_2'45_1
  (- a)" = -a" by Lm19;

theorem :: REAL_2'46_1
  a <> 0 & a = a" implies a = 1 or a = -1 by Lm18;

begin :: additional
:: from JORDAN4

theorem
  a+b+c-b=a+c;

theorem
  a-b+c+b=a+c;

theorem
  a+b-c-b=a-c;

theorem
  a-b-c+b=a-c;

theorem
  a-a-b=-b;

theorem
  -a+a-b=-b;

theorem
  a-b-a=-b;

theorem
  -a-b+a=-b;

begin :: Addenda
:: from REAL_2, 2005.02.05, A.T.

theorem
  for a,b st b<>0 ex e st a=b/e
proof
  let a,b;
  assume
A1: b<>0;
  per cases;
  suppose
A2: a = 0;
    take 0;
    b/0 = b*0" by XCMPLX_0:def 9;
    hence thesis by A2;
  end;
  suppose
A3: a <> 0;
    take e=b/a;
    thus a=a*1 .=a*(e*e") by A1,A3,XCMPLX_0:def 7
      .=a*e*e"
      .=a*(a"*b)*e" by XCMPLX_0:def 9
      .=a*a"*b*e"
      .=1*b*e" by A3,XCMPLX_0:def 7
      .=b/e by XCMPLX_0:def 9;
  end;
end;

:: from IRRAT_1, 2005.02.05, A.T.

theorem
  a/(b*c*(d/e))=(e/c)*(a/(b*d))
proof
  thus a/(b*c*(d/e)) = a/(b*c*(d*e")) by XCMPLX_0:def 9
    .= a/(c*(b*d*e"))
    .= a/(c*((b*d)/e)) by XCMPLX_0:def 9
    .= a/((b*d)/(e/c)) by Th81
    .= (e/c)*(a/(b*d)) by Th81;
end;

:: from BORSUK_6, 2005.02.05, A.T.

theorem
  ((d - c)/b) * a + c = (1 - a/b)*c + (a/b) * d
proof
  per cases;
  suppose
A1: b = 0;
A2: a/b = a*b" by XCMPLX_0:def 9
      .= a*0 by A1;
    thus ((d - c)/b) * a + c = ((d - c)*b") * a + c by XCMPLX_0:def 9
      .= ((d - c)*0) * a + c by A1
      .= (1 - (a/b))*c + (a/b) * d by A2;
  end;
  suppose
A3: b <> 0;
    ((d - c)/b) * a + c = ((d - c)/b) * a + c*1
      .= ((d - c)/b) * a + c*(b/b) by A3,Lm5
      .= ((d - c)/b) * a + c*b/b by Lm8
      .= (d - c) * a / b + c*b/b by Lm8
      .= ((d-c)*a + c*b)/ b by Th62
      .= ((b-a)*c + a * d) / b
      .= (b-a)*c/b + a*d/b by Th62
      .= (b-a)*c/b + (a/b) * d by Lm8
      .= ((b - a)/b)*c + (a/b) * d by Lm8
      .= (b/b - a/b)*c + (a/b) * d by Th120
      .= (1 - a/b)*c + (a/b) * d by A3,Lm5;
    hence thesis;
  end;
end;

:: Missing, 2005.07.04, A.T.

theorem
  a <> 0 implies a * b + c = a * (b + (c/a))
proof
  assume a <> 0;
  hence a * b + c = a * b + a*(c/a) by Lm3
    .= a * (b + (c/a));
end;