let i1, j1 be Nat; :: thesis: quotient (i1,j1) = i1 / j1
set x = quotient (i1,j1);
per cases ( j1 = {} or j1 <> 0 ) ;
suppose A1: j1 = {} ; :: thesis: quotient (i1,j1) = i1 / j1
hence quotient (i1,j1) = {} by ARYTM_3:def 10
.= i1 / j1 by A1 ;
:: thesis: verum
end;
suppose A2: j1 <> 0 ; :: thesis: 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 ;
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 ;
then A8: 1 = + ((* (x1,y1)),(opp (* (x2,y2)))) by
.= + ((* (x1,y1)),(opp (In (0,REAL)))) by
.= * (x1,y1) by ;
j1 in REAL by XREAL_0:def 1;
then x2 = 0 by ;
then A9: j1 = x1 by ;
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 ;
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 ;
then A13: y1 in RAT+ ;
j1 " in REAL by XREAL_0:def 1;
then y2 = 0 by ;
then A14: j1 " = y1 by ;
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 ;
x1 in omega by ;
then consider x19, y19 being Element of REAL+ such that
A20: x1 = x19 and
A21: y1 = y19 and
A22: * (x1,y1) = x19 *' y19 by ;
A23: ex x199, y199 being Element of RAT+ st
( x19 = x199 & y19 = y199 & x19 *' y19 = x199 *' y199 ) by ;
j1 " in REAL by XREAL_0:def 1;
then A24: y92 = 0 by ;
then j1 " = y91 by ;
then A25: i1 * (j1 ") = + ((* (x91,y1)),(opp (* (x92,(In (0,REAL)))))) by
.= + ((* (x91,y1)),(In (0,REAL))) by
.= * (x91,y1) by ARYTM_0:11 ;
i1 in REAL by XREAL_0:def 1;
then x92 = 0 by ;
then A26: i1 = x91 by ;
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 ;
consider x99, y99 being Element of RAT+ such that
A31: x9 = x99 and
A32: y9 = y99 and
A33: i1 * (j1 ") = x99 *' y99 by ;
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
.= quotient (i1,one) by ARYTM_3:53
.= i1 by ARYTM_3:40
.= x99 *' one by
.= (x99 *' y99) *' b by A9, A8, A29, A32, A20, A21, A22, A23, ARYTM_3:52 ;
hence quotient (i1,j1) = i1 / j1 by ; :: thesis: verum
end;
end;