:: Field Properties of Complex Numbers - Requirements :: by Library Committee :: :: Received May 29, 2003 :: Copyright (c) 2003-2017 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; 0 in NAT; then reconsider Z = 0 as Element of REAL by NUMBERS:19; 1 in NAT; then reconsider J = 1 as Element of REAL by NUMBERS:19; theorem Th1: x + 0 = x proof 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; Lm2: opp Z = 0 proof +(Z,Z) = 0 by ARYTM_0:11; hence thesis by ARYTM_0:def 3; end; theorem Th2: x * 0 = 0 proof 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),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 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;