Copyright (c) 2003 Association of Mizar Users
environ
vocabulary ARYTM, ARYTM_1, RELAT_1, ARYTM_3, ORDINAL1, ORDINAL2, COMPLEX1,
OPPCAT_1, XCMPLX_0;
notation SUBSET_1, ORDINAL1, ORDINAL2, NUMBERS, ARYTM_0, XCMPLX_0;
constructors ARYTM_0, ARYTM_1, XCMPLX_0, FUNCT_4, ARYTM_3, XBOOLE_0;
clusters ARYTM_2, NUMBERS, XCMPLX_0, ARYTM_3, ZFMISC_1, XBOOLE_0;
requirements NUMERALS, SUBSET, BOOLE;
theorems ARYTM_0, ORDINAL2, XCMPLX_0;
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 number;
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:11;
0 = [*0,0*] by ARYTM_0:def 7;
then x + 0 = [*+(x1,0),+(x2,0)*] by A1,XCMPLX_0:def 4
.= [* x1,+(x2,0)*] by ARYTM_0:13
.= x by A1,ARYTM_0:13;
hence thesis;
end;
Lm1: -0 = 0
proof
0 + -0 = -0 by Th1;
hence thesis by XCMPLX_0:def 6;
end;
Lm2: opp 0 = 0
proof
+(0,0) = 0 by ARYTM_0:13;
hence thesis by ARYTM_0:def 4;
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:11;
0 = [*0,0*] by ARYTM_0:def 7;
then x * 0 = [* +(*(x1,0),opp*(x2,0)), +(*(x1,0),*(x2,0)) *]
by A1,XCMPLX_0:def 5
.= [* +(*(x1,0),opp 0), +(*(x1,0),*(x2,0)) *] by ARYTM_0:14
.= [* +(*(x1,0),opp 0), +(*(x1,0),0) *] by ARYTM_0:14
.= [* +(0,opp 0), +(*(x1,0),0) *] by ARYTM_0:14
.= [* +(0,opp 0), +(0,0) *] by ARYTM_0:14
.= [* +(0,opp 0), 0 *] by ARYTM_0:13
.= [* opp 0, 0 *] by ARYTM_0:13
.= 0 by Lm2,ARYTM_0:def 7;
hence thesis;
end;
Lm3:one = succ 0 by ORDINAL2:def 4 .= 1;
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:11;
1 = [*1,0*] by ARYTM_0:def 7;
then x * 1 = [* +(*(x1,1),opp*(x2,0)), +(*(x1,0),*(x2,1)) *]
by A1,XCMPLX_0:def 5
.= [* +(*(x1,1),opp 0), +(*(x1,0),*(x2,1)) *] by ARYTM_0:14
.= [* +(x1,opp 0), +(*(x1,0),*(x2,1)) *] by Lm3,ARYTM_0:21
.= [* +(x1,opp 0), +(*(x1,0),x2) *] by Lm3,ARYTM_0:21
.= [* +(x1,0), +(0,x2) *] by Lm2,ARYTM_0:14
.= [* x1, +(0,x2) *] by ARYTM_0:13
.= x by A1,ARYTM_0:13;
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;
Lm4: 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 Lm4,XCMPLX_0:def 9;
hence thesis by Th3;
end;