let i1, j1 be Element of NAT ; :: thesis: quotient i1,j1 = i1 / j1
set x = quotient i1,j1;
per cases
( j1 = {} or j1 <> 0 )
;
suppose A2:
j1 <> 0
;
:: thesis: quotient i1,j1 = i1 / j1then
j1 * (j1 " ) = 1
by XCMPLX_0:def 7;
then consider x1,
x2,
y1,
y2 being
Real such that A3:
j1 = [*x1,x2*]
and A4:
j1 " = [*y1,y2*]
and A5:
1
= [*(+ (* x1,y1),(opp (* x2,y2))),(+ (* x1,y2),(* x2,y1))*]
by XCMPLX_0:def 5;
x2 = 0
by A3, ARYTM_0:26;
then A6:
j1 = x1
by A3, ARYTM_0:def 7;
y2 = 0
by A4, ARYTM_0:26;
then A7:
j1 " = y1
by A4, ARYTM_0:def 7;
+ 0 ,
(opp 0 ) = 0
by ARYTM_0:def 4;
then A8:
opp 0 = 0
by ARYTM_0:13;
+ (* x1,y2),
(* x2,y1) = 0
by A5, ARYTM_0:26;
then A9: 1 =
+ (* x1,y1),
(opp (* x2,y2))
by A5, ARYTM_0:def 7
.=
+ (* x1,y1),
(opp 0 )
by A3, ARYTM_0:14, ARYTM_0:26
.=
* x1,
y1
by A8, ARYTM_0:13
;
consider x'1,
x'2,
y'1,
y'2 being
Real such that A10:
i1 = [*x'1,x'2*]
and A11:
j1 " = [*y'1,y'2*]
and A12:
i1 * (j1 " ) = [*(+ (* x'1,y'1),(opp (* x'2,y'2))),(+ (* x'1,y'2),(* x'2,y'1))*]
by XCMPLX_0:def 5;
x'2 = 0
by A10, ARYTM_0:26;
then A13:
i1 = x'1
by A10, ARYTM_0:def 7;
A14:
y'2 = 0
by A11, ARYTM_0:26;
then A15:
j1 " = y'1
by A11, ARYTM_0:def 7;
+ (* x'1,y'2),
(* x'2,y'1) = 0
by A12, ARYTM_0:26;
then A16:
i1 * (j1 " ) =
+ (* x'1,y1),
(opp (* x'2,0 ))
by A7, A12, A14, A15, ARYTM_0:def 7
.=
+ (* x'1,y1),
0
by A8, ARYTM_0:14
.=
* x'1,
y1
by ARYTM_0:13
;
A17:
x'1 in omega
by A13;
then A18:
x'1 in RAT+
by Lm1;
x1 in omega
by A6;
then reconsider xx =
x1 as
Element of
RAT+ by Lm1;
consider yy being
Element of
RAT+ such that A19:
xx *' yy = one
by A2, A6, ARYTM_3:60;
(
xx in RAT+ &
yy in RAT+ )
;
then reconsider xx1 =
xx,
yy1 =
yy as
Element of
REAL+ by ARYTM_2:1;
A20:
ex
x',
y' being
Element of
RAT+ st
(
xx1 = x' &
yy1 = y' &
xx1 *' yy1 = x' *' y' )
by ARYTM_2:22;
(
xx1 in REAL+ &
yy1 in REAL+ )
;
then reconsider xx1 =
xx1,
yy1 =
yy1 as
Element of
REAL by ARYTM_0:1;
ex
x',
y' being
Element of
REAL+ st
(
xx1 = x' &
yy1 = y' &
* xx1,
yy1 = x' *' y' )
by ARYTM_0:def 3;
then A21:
yy = y1
by A2, A6, A9, A19, A20, ARYTM_0:20;
then A22:
y1 in RAT+
;
then consider x',
y' being
Element of
REAL+ such that A23:
x'1 = x'
and A24:
y1 = y'
and A25:
i1 * (j1 " ) = x' *' y'
by A16, A18, ARYTM_0:def 3, ARYTM_2:1;
consider x'',
y'' being
Element of
RAT+ such that A26:
x' = x''
and A27:
y' = y''
and A28:
i1 * (j1 " ) = x'' *' y''
by A17, A21, A23, A24, A25, Lm1, ARYTM_2:22;
A29:
j1 in omega
;
then reconsider a =
quotient i1,
j1,
b =
j1 as
Element of
RAT+ by Lm1;
x1 in omega
by A6;
then consider x1',
y1' being
Element of
REAL+ such that A30:
x1 = x1'
and A31:
y1 = y1'
and A32:
* x1,
y1 = x1' *' y1'
by A22, ARYTM_0:def 3, ARYTM_2:1, ARYTM_2:2;
A33:
ex
x1'',
y1'' being
Element of
RAT+ st
(
x1' = x1'' &
y1' = y1'' &
x1' *' y1' = x1'' *' y1'' )
by A6, A21, A29, A30, A31, Lm1, ARYTM_2:22;
a *' b =
(quotient i1,j1) *' (quotient j1,one )
by ARYTM_3:46
.=
quotient (i1 *^ j1),
(j1 *^ one )
by ARYTM_3:55
.=
(quotient i1,one ) *' (quotient j1,j1)
by ARYTM_3:55
.=
(quotient i1,one ) *' one
by A2, ARYTM_3:47
.=
quotient i1,
one
by ARYTM_3:59
.=
i1
by ARYTM_3:46
.=
x'' *' one
by A13, A23, A26, ARYTM_3:59
.=
(x'' *' y'') *' b
by A6, A9, A24, A27, A30, A31, A32, A33, ARYTM_3:58
;
hence
quotient i1,
j1 = i1 / j1
by A2, A28, ARYTM_3:62;
:: thesis: verum end;