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
x9,
y9 being
Element of
RAT+ st
(
xx1 = x9 &
yy1 = y9 &
xx1 *' yy1 = x9 *' y9 )
by ARYTM_2:22;
yy1 in REAL+
;
then reconsider xx1 =
xx1,
yy1 =
yy1 as
Element of
REAL by ARYTM_0:1;
ex
x9,
y9 being
Element of
REAL+ st
(
xx1 = x9 &
yy1 = y9 &
* xx1,
yy1 = x9 *' y9 )
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 x91,
x92,
y91,
y92 being
Real such that A16:
i1 = [*x91,x92*]
and A17:
j1 " = [*y91,y92*]
and A18:
i1 * (j1 " ) = [*(+ (* x91,y91),(opp (* x92,y92))),(+ (* x91,y92),(* x92,y91))*]
by XCMPLX_0:def 5;
A19:
+ (* x91,y92),
(* x92,y91) = 0
by A18, ARYTM_0:26;
x1 in omega
by A8;
then consider x19,
y19 being
Element of
REAL+ such that A20:
x1 = x19
and A21:
y1 = y19
and A22:
* x1,
y1 = x19 *' y19
by A13, ARYTM_0:def 3, ARYTM_2:1, ARYTM_2:2;
A23:
ex
x199,
y199 being
Element of
RAT+ st
(
x19 = x199 &
y19 = y199 &
x19 *' y19 = x199 *' y199 )
by A8, A12, A15, A20, A21, Lm1, ARYTM_2:22;
A24:
y92 = 0
by A17, ARYTM_0:26;
then
j1 " = y91
by A17, ARYTM_0:def 7;
then A25:
i1 * (j1 " ) =
+ (* x91,y1),
(opp (* x92,0 ))
by A14, A18, A24, A19, ARYTM_0:def 7
.=
+ (* x91,y1),
0
by A3, ARYTM_0:14
.=
* x91,
y1
by ARYTM_0:13
;
x92 = 0
by A16, ARYTM_0:26;
then A26:
i1 = x91
by A16, ARYTM_0:def 7;
then A27:
x91 in omega
;
then
x91 in RAT+
by Lm1;
then consider x9,
y9 being
Element of
REAL+ such that A28:
x91 = x9
and A29:
y1 = y9
and A30:
i1 * (j1 " ) = x9 *' y9
by A25, A13, ARYTM_0:def 3, ARYTM_2:1;
consider x99,
y99 being
Element of
RAT+ such that A31:
x9 = x99
and A32:
y9 = y99
and A33:
i1 * (j1 " ) = x99 *' y99
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
.=
x99 *' one
by A26, A28, A31, ARYTM_3:59
.=
(x99 *' y99) *' 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;