ARITHM

:: Field Properties of Complex Numbers - Requirements
::  by Library Committee
::
:: Received May 29, 2003
:: Copyright (c) 2003-2026 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, ARYTM_3, CARD_1, NUMBERS, SUBSET_1, ARYTM_0, ARYTM_1,
      RELAT_1;
 notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, ARYTM_0, XCMPLX_0;
 constructors FUNCT_4, ARYTM_0, XCMPLX_0, NUMBERS;
 registrations XCMPLX_0, ORDINAL1;
 requirements NUMERALS, SUBSET, BOOLE;
 theorems ARYTM_0, XCMPLX_0, NUMBERS;

begin

:: This file contains statements which are obvious for Mizar checker if
:: "requirements ARITHM" is included in the environment description
:: of an article. "requirements NUMERALS" is also required.
:: They are published for testing purposes only.
:: Users should use appropriate requirements instead of referencing
:: to these theorems.
:: Some of these items need also other requirements for proper work.

reserve x for Complex;

theorem Th1:
  x + 0 = x
proof
  0 in NAT;
  then reconsider Z =0 as Element of REAL by NUMBERS:19;
  x in COMPLEX by XCMPLX_0:def 2;
  then consider x1,x2 being Element of REAL such that
A1: x = [*x1,x2*] by ARYTM_0:9;
  0 = [*Z,Z*] by ARYTM_0:def 5;
  then x + 0 = [*+(x1,Z),+(x2,Z)*] by A1,XCMPLX_0:def 4
    .= [* x1,+(x2,Z)*] by ARYTM_0:11
    .= x by A1,ARYTM_0:11;
  hence thesis;
end;

Lm1: -0 = 0
proof
  0 + -0 = -0 by Th1;
  hence thesis by XCMPLX_0:def 6;
end;

theorem Th2:
  x * 0 = 0
proof
  0 in NAT;
  then reconsider Z =0 as Element of REAL by NUMBERS:19;

  x in COMPLEX by XCMPLX_0:def 2;
  then consider x1,x2 being Element of REAL such that
A1: x = [*x1,x2*] by ARYTM_0:9;

     +(Z,Z) = 0 by ARYTM_0:11;
  then Lm2: opp Z = 0 by ARYTM_0:def 3;
  0 = [*Z,Z*] by ARYTM_0:def 5;
  then x * 0 = [* +(*(x1,Z),opp*(x2,Z)), +(*(x1,Z),*(x2,Z)) *] by A1,
XCMPLX_0:def 5
    .= [* +(*(x1,Z),opp Z), +(*(x1,Z),*(x2,Z)) *] by ARYTM_0:12
    .= [* +(*(x1,Z),opp Z), +(*(x1,Z),Z) *] by ARYTM_0:12
    .= [* +(Z,opp Z), +(*(x1,Z),Z) *] by ARYTM_0:12
    .= [* +(Z,opp Z), +(Z,Z) *] by ARYTM_0:12
    .= [* +(Z,opp Z), Z *] by ARYTM_0:11
    .= [* opp Z, Z *] by ARYTM_0:11
    .= 0 by Lm2,ARYTM_0:def 5;
  hence thesis;
end;

theorem Th3:
  1 * x = x
proof
  0 in NAT & 1 in NAT;
then reconsider Z =0,J = 1 as Element of REAL by NUMBERS:19;
     +(Z,Z) = 0 by ARYTM_0:11;
  then Lm2: opp Z = 0 by ARYTM_0:def 3;     
  x in COMPLEX by XCMPLX_0:def 2;
  then consider x1,x2 being Element of REAL such that
A1: x = [*x1,x2*] by ARYTM_0:9;
  1 = [*J,Z*] by ARYTM_0:def 5;
  then x * 1 = [* +(*(x1,J),opp*(x2,Z)), +(*(x1,Z),*(x2,J)) *] by A1,
XCMPLX_0:def 5
    .= [* +(*(x1,J),opp Z), +(*(x1,Z),*(x2,J)) *] by ARYTM_0:12
    .= [* +(x1,opp Z), +(*(x1,Z),*(x2,J)) *] by ARYTM_0:19
    .= [* +(x1,opp Z), +(*(x1,Z),x2) *] by ARYTM_0:19
    .= [* +(x1,Z), +(Z,x2) *] by Lm2,ARYTM_0:12
    .= [* x1, +(Z,x2) *] by ARYTM_0:11
    .= x by A1,ARYTM_0:11;
  hence thesis;
end;

theorem
  x - 0 = x
proof
  x - 0 = x + 0 by Lm1,XCMPLX_0:def 8;
  hence thesis by Th1;
end;

theorem
  0 / x = 0
proof
  0 / x = 0 * x" by XCMPLX_0:def 9;
  hence thesis by Th2;
end;

Lm3: 1" = 1
proof
  1 * 1" = 1" by Th3;
  hence thesis by XCMPLX_0:def 7;
end;

theorem
  x / 1 = x
proof
  x / 1 = x * 1 by Lm3,XCMPLX_0:def 9;
  hence thesis by Th3;
end;