let i1, j1 be 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
+ (
(In (0,REAL)),
(opp (In (0,REAL))))
= 0
by ARYTM_0:def 3;
then A3:
opp (In (0,REAL)) = 0
by ARYTM_0:11;
reconsider y = 1 as
Element of
REAL by NUMBERS:19;
j1 * (j1 ") = 1
by A2, XCMPLX_0:def 7;
then consider x1,
x2,
y1,
y2 being
Element of
REAL such that A4:
j1 = [*x1,x2*]
and A5:
j1 " = [*y1,y2*]
and A6:
y = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*]
by XCMPLX_0:def 5;
A7:
j1 in REAL
by XREAL_0:def 1;
+ (
(* (x1,y2)),
(* (x2,y1)))
= 0
by A6, ARYTM_0:24;
then A8: 1 =
+ (
(* (x1,y1)),
(opp (* (x2,y2))))
by A6, ARYTM_0:def 5
.=
+ (
(* (x1,y1)),
(opp (In (0,REAL))))
by A4, ARYTM_0:12, ARYTM_0:24, A7
.=
* (
x1,
y1)
by A3, ARYTM_0:11
;
j1 in REAL
by XREAL_0:def 1;
then
x2 = 0
by A4, ARYTM_0:24;
then A9:
j1 = x1
by A4, ARYTM_0:def 5;
then
x1 in omega
by ORDINAL1:def 12;
then reconsider xx =
x1 as
Element of
RAT+ by Lm1;
consider yy being
Element of
RAT+ such that A10:
xx *' yy = one
by A2, A9, ARYTM_3:54;
reconsider xx1 =
xx,
yy1 =
yy as
Element of
REAL+ by ARYTM_2:1;
A11:
ex
x9,
y9 being
Element of
RAT+ st
(
xx1 = x9 &
yy1 = y9 &
xx1 *' yy1 = x9 *' y9 )
by ARYTM_2:21;
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 2;
then A12:
yy = y1
by A2, A9, A8, A10, A11, ARYTM_0:18;
then A13:
y1 in RAT+
;
j1 " in REAL
by XREAL_0:def 1;
then
y2 = 0
by A5, ARYTM_0:24;
then A14:
j1 " = y1
by A5, ARYTM_0:def 5;
A15:
j1 in omega
by ORDINAL1:def 12;
then reconsider a =
quotient (
i1,
j1),
b =
j1 as
Element of
RAT+ by Lm1;
consider x91,
x92,
y91,
y92 being
Element of
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;
i1 * (j1 ") in REAL
by XREAL_0:def 1;
then A19:
+ (
(* (x91,y92)),
(* (x92,y91)))
= 0
by A18, ARYTM_0:24;
x1 in omega
by A9, ORDINAL1:def 12;
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 2, ARYTM_2:1, ARYTM_2:2;
A23:
ex
x199,
y199 being
Element of
RAT+ st
(
x19 = x199 &
y19 = y199 &
x19 *' y19 = x199 *' y199 )
by A9, A12, A15, A20, A21, Lm1, ARYTM_2:21;
j1 " in REAL
by XREAL_0:def 1;
then A24:
y92 = 0
by A17, ARYTM_0:24;
then
j1 " = y91
by A17, ARYTM_0:def 5;
then A25:
i1 * (j1 ") =
+ (
(* (x91,y1)),
(opp (* (x92,(In (0,REAL))))))
by A14, A18, A24, A19, ARYTM_0:def 5
.=
+ (
(* (x91,y1)),
(In (0,REAL)))
by A3, ARYTM_0:12
.=
* (
x91,
y1)
by ARYTM_0:11
;
i1 in REAL
by XREAL_0:def 1;
then
x92 = 0
by A16, ARYTM_0:24;
then A26:
i1 = x91
by A16, ARYTM_0:def 5;
then A27:
x91 in omega
by ORDINAL1:def 12;
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 2, 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:21;
a *' b =
(quotient (i1,j1)) *' (quotient (j1,one))
by ARYTM_3:40
.=
quotient (
(i1 *^ j1),
(j1 *^ one))
by ARYTM_3:49
.=
(quotient (i1,one)) *' (quotient (j1,j1))
by ARYTM_3:49
.=
(quotient (i1,one)) *' one
by A2, ARYTM_3:41
.=
quotient (
i1,
one)
by ARYTM_3:53
.=
i1
by ARYTM_3:40
.=
x99 *' one
by A26, A28, A31, ARYTM_3:53
.=
(x99 *' y99) *' b
by A9, A8, A29, A32, A20, A21, A22, A23, ARYTM_3:52
;
hence
quotient (
i1,
j1)
= i1 / j1
by A2, A33, ARYTM_3:56;
verum end;