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