let d be Dyadic; :: thesis: for i being Integer holds (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d)
let i be Integer; :: thesis: (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d)
A1: ( uDyadic . 0 = uInt . 0 & uInt . 0 = 0_No ) by Def1, Def5;
defpred S₁[ Nat] means for i, j being Nat st i + j <= $1 holds
for d being Dyadic st d in DYADIC j holds
(uDyadic . i) * (uDyadic . d) == uDyadic . (i * d);
A2: S₁[ 0 ]

proof

let i, j be Nat; :: thesis: ( i + j <= 0 implies for d being Dyadic st d in DYADIC j holds
(uDyadic . i) * (uDyadic . d) == uDyadic . (i * d) )
assume A3: i + j <= 0 ; :: thesis: for d being Dyadic st d in DYADIC j holds
(uDyadic . i) * (uDyadic . d) == uDyadic . (i * d)
let d be Dyadic; :: thesis: ( d in DYADIC j implies (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d) )
assume d in DYADIC j ; :: thesis: (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d)
i = 0 by A3;
hence (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d) by A1; :: thesis: verum

end;

A4: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A5: S₁[m] ; :: thesis: S₁[m + 1]
set m1 = m + 1;
let i, j be Nat; :: thesis: ( i + j <= m + 1 implies for d being Dyadic st d in DYADIC j holds
(uDyadic . i) * (uDyadic . d) == uDyadic . (i * d) )
assume A6: i + j <= m + 1 ; :: thesis: for d being Dyadic st d in DYADIC j holds
(uDyadic . i) * (uDyadic . d) == uDyadic . (i * d)
let d be Dyadic; :: thesis: ( d in DYADIC j implies (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d) )
assume A7: d in DYADIC j ; :: thesis: (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d)

per cases ( i + j < m + 1 or i = 0 or j = 0 or ( i + j = m + 1 & i <> 0 & j <> 0 ) ) by A6, XXREAL_0:1;

suppose i + j < m + 1 ; :: thesis: (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d)

then i + j <= m by NAT_1:13;
hence (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d) by A5, A7; :: thesis: verum

end;

suppose i = 0 ; :: thesis: (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d)

hence (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d) by A1; :: thesis: verum

end;

suppose j = 0 ; :: thesis: (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d)

then reconsider dd = d as Integer by A7, Th21;
uDyadic . i = uInt . i by Def5;
then (uDyadic . i) * (uDyadic . d) = (uInt . i) * (uInt . dd) by Def5;
then (uDyadic . i) * (uDyadic . d) == uInt . (i * dd) by Th15;
hence (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d) by Def5; :: thesis: verum

end;

suppose A8: ( i + j = m + 1 & i <> 0 & j <> 0 ) ; :: thesis: (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d)

then reconsider i1 = i - 1, j1 = j - 1 as Nat by NAT_1:20;

per cases ( d in DYADIC j1 or not d in DYADIC j1 ) ;

suppose A9: d in DYADIC j1 ; :: thesis: (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d)

m + 1 = (i + j1) + 1 by A8;
hence (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d) by A9, A5; :: thesis: verum

end;

suppose not d in DYADIC j1 ; :: thesis: (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d)

then d in (DYADIC (j1 + 1)) \ (DYADIC j1) by A7, XBOOLE_0:def 5;
then consider k being Integer such that
A10: d = ((2 * k) + 1) / (2 |^ (j1 + 1)) by Th20;
set x = uDyadic . i;
set y = uDyadic . d;
A11: uDyadic . d = [{(uDyadic . (k / (2 |^ j1)))},{(uDyadic . ((k + 1) / (2 |^ j1)))}] by A10, Def5;
uDyadic . i = uInt . (i1 + 1) by Def5;
then A12: uDyadic . i = [{(uInt . i1)},{}] by Def1
.= [{(uDyadic . i1)},{}] by Def5 ;
( comp ((R_ (uDyadic . i)),(uDyadic . i),(uDyadic . d),(R_ (uDyadic . d))) = comp ((R_ (uDyadic . d)),(uDyadic . d),(uDyadic . i),(R_ (uDyadic . i))) & comp ((R_ (uDyadic . i)),(uDyadic . i),(uDyadic . d),(L_ (uDyadic . d))) = comp ((L_ (uDyadic . d)),(uDyadic . d),(uDyadic . i),(R_ (uDyadic . i))) ) by SURREALR:53;
then A13: ( comp ((R_ (uDyadic . i)),(uDyadic . i),(uDyadic . d),(L_ (uDyadic . d))) = {} & {} = comp ((R_ (uDyadic . i)),(uDyadic . i),(uDyadic . d),(R_ (uDyadic . d))) ) by A12, SURREALR:49;
(i1 + j1) + 1 = m by A8;
then A14: i1 + j1 < m by NAT_1:13;
A15: ( i1 + j = m & i + j1 = m ) by A8;
A16: k / (2 |^ j1) in DYADIC j1 by Def4;
set M = 2 |^ (j1 + 1);
A17: 2 * (2 |^ j1) = 2 |^ (j1 + 1) by NEWTON:6;
A18: i1 * (k / (2 |^ j1)) = i1 * ((2 * k) / (2 |^ (j1 + 1))) by A17, XCMPLX_1:91
.= (i1 * (2 * k)) / (2 |^ (j1 + 1)) by XCMPLX_1:74 ;
(i1 * d) + (i * (k / (2 |^ j1))) = (i1 * (((2 * k) + 1) / (2 |^ (j1 + 1)))) + (i * ((2 * k) / (2 |^ (j1 + 1)))) by A10, A17, XCMPLX_1:91
.= ((i1 * ((2 * k) + 1)) / (2 |^ (j1 + 1))) + (i * ((2 * k) / (2 |^ (j1 + 1)))) by XCMPLX_1:74
.= ((i1 * ((2 * k) + 1)) / (2 |^ (j1 + 1))) + ((i * (2 * k)) / (2 |^ (j1 + 1))) by XCMPLX_1:74
.= ((i1 * ((2 * k) + 1)) + (i * (2 * k))) / (2 |^ (j1 + 1)) by XCMPLX_1:62 ;
then A19: ((i1 * d) + (i * (k / (2 |^ j1)))) + (- (i1 * (k / (2 |^ j1)))) = (((i1 * ((2 * k) + 1)) + (i * (2 * k))) / (2 |^ (j1 + 1))) - ((i1 * (2 * k)) / (2 |^ (j1 + 1))) by A18
.= (((i1 * ((2 * k) + 1)) + (i * (2 * k))) - (i1 * (2 * k))) / (2 |^ (j1 + 1)) by XCMPLX_1:120
.= ((i * ((2 * k) + 1)) - 1) / (2 |^ (j1 + 1)) ;
( (uDyadic . i1) * (uDyadic . d) == uDyadic . (i1 * d) & (uDyadic . i) * (uDyadic . (k / (2 |^ j1))) == uDyadic . (i * (k / (2 |^ j1))) & (uDyadic . i1) * (uDyadic . (k / (2 |^ j1))) == uDyadic . (i1 * (k / (2 |^ j1))) ) by A14, A15, A16, A7, A5;
then A20: ( - ((uDyadic . i1) * (uDyadic . (k / (2 |^ j1)))) == - (uDyadic . (i1 * (k / (2 |^ j1)))) & - (uDyadic . (i1 * (k / (2 |^ j1)))) = uDyadic . (- (i1 * (k / (2 |^ j1)))) & ((uDyadic . i1) * (uDyadic . d)) + ((uDyadic . i) * (uDyadic . (k / (2 |^ j1)))) == (uDyadic . (i1 * d)) + (uDyadic . (i * (k / (2 |^ j1)))) & (uDyadic . (i1 * d)) + (uDyadic . (i * (k / (2 |^ j1)))) == uDyadic . ((i1 * d) + (i * (k / (2 |^ j1)))) ) by SURREALR:10, SURREALR:43, Th27, Th39;
then ((uDyadic . i1) * (uDyadic . d)) + ((uDyadic . i) * (uDyadic . (k / (2 |^ j1)))) == uDyadic . ((i1 * d) + (i * (k / (2 |^ j1)))) by SURREALO:4;
then ( (((uDyadic . i1) * (uDyadic . d)) + ((uDyadic . i) * (uDyadic . (k / (2 |^ j1))))) + (- ((uDyadic . i1) * (uDyadic . (k / (2 |^ j1))))) == (uDyadic . ((i1 * d) + (i * (k / (2 |^ j1))))) + (uDyadic . (- (i1 * (k / (2 |^ j1))))) & (uDyadic . ((i1 * d) + (i * (k / (2 |^ j1))))) + (uDyadic . (- (i1 * (k / (2 |^ j1))))) == uDyadic . (((i1 * d) + (i * (k / (2 |^ j1)))) + (- (i1 * (k / (2 |^ j1))))) ) by A20, SURREALR:43, Th39;
then (((uDyadic . i1) * (uDyadic . d)) + ((uDyadic . i) * (uDyadic . (k / (2 |^ j1))))) + (- ((uDyadic . i1) * (uDyadic . (k / (2 |^ j1))))) == uDyadic . (((i * ((2 * k) + 1)) - 1) / (2 |^ (j1 + 1))) by A19, SURREALO:4;
then A21: {((((uDyadic . i1) * (uDyadic . d)) + ((uDyadic . i) * (uDyadic . (k / (2 |^ j1))))) + (- ((uDyadic . i1) * (uDyadic . (k / (2 |^ j1))))))} <==> {(uDyadic . (((i * ((2 * k) + 1)) - 1) / (2 |^ (j1 + 1))))} by SURREALO:32;
A22: comp ((L_ (uDyadic . i)),(uDyadic . i),(uDyadic . d),(L_ (uDyadic . d))) = {((((uDyadic . i1) * (uDyadic . d)) + ((uDyadic . i) * (uDyadic . (k / (2 |^ j1))))) - ((uDyadic . i1) * (uDyadic . (k / (2 |^ j1)))))} by SURREALR:52, A11, A12;
A23: (k + 1) / (2 |^ j1) in DYADIC j1 by Def4;
A24: i1 * ((k + 1) / (2 |^ j1)) = i1 * ((2 * (k + 1)) / (2 |^ (j1 + 1))) by A17, XCMPLX_1:91
.= (i1 * (2 * (k + 1))) / (2 |^ (j1 + 1)) by XCMPLX_1:74 ;
(i1 * d) + (i * ((k + 1) / (2 |^ j1))) = (i1 * (((2 * k) + 1) / (2 |^ (j1 + 1)))) + (i * ((2 * (k + 1)) / (2 |^ (j1 + 1)))) by A10, A17, XCMPLX_1:91
.= ((i1 * ((2 * k) + 1)) / (2 |^ (j1 + 1))) + (i * ((2 * (k + 1)) / (2 |^ (j1 + 1)))) by XCMPLX_1:74
.= ((i1 * ((2 * k) + 1)) / (2 |^ (j1 + 1))) + ((i * (2 * (k + 1))) / (2 |^ (j1 + 1))) by XCMPLX_1:74
.= ((i1 * ((2 * k) + 1)) + (i * (2 * (k + 1)))) / (2 |^ (j1 + 1)) by XCMPLX_1:62 ;
then A25: ((i1 * d) + (i * ((k + 1) / (2 |^ j1)))) + (- (i1 * ((k + 1) / (2 |^ j1)))) = (((i1 * ((2 * k) + 1)) + (i * (2 * (k + 1)))) / (2 |^ (j1 + 1))) - ((i1 * (2 * (k + 1))) / (2 |^ (j1 + 1))) by A24
.= ((((i * ((2 * k) + 1)) - ((2 * k) + 1)) + (i * (2 * (k + 1)))) - ((i * (2 * (k + 1))) - (2 * (k + 1)))) / (2 |^ (j1 + 1)) by XCMPLX_1:120
.= (((i * ((2 * k) + 1)) - 1) + 2) / (2 |^ (j1 + 1)) ;
( (uDyadic . i1) * (uDyadic . d) == uDyadic . (i1 * d) & (uDyadic . i) * (uDyadic . ((k + 1) / (2 |^ j1))) == uDyadic . (i * ((k + 1) / (2 |^ j1))) & (uDyadic . i1) * (uDyadic . ((k + 1) / (2 |^ j1))) == uDyadic . (i1 * ((k + 1) / (2 |^ j1))) ) by A14, A15, A23, A7, A5;
then A26: ( - ((uDyadic . i1) * (uDyadic . ((k + 1) / (2 |^ j1)))) == - (uDyadic . (i1 * ((k + 1) / (2 |^ j1)))) & - (uDyadic . (i1 * ((k + 1) / (2 |^ j1)))) = uDyadic . (- (i1 * ((k + 1) / (2 |^ j1)))) & ((uDyadic . i1) * (uDyadic . d)) + ((uDyadic . i) * (uDyadic . ((k + 1) / (2 |^ j1)))) == (uDyadic . (i1 * d)) + (uDyadic . (i * ((k + 1) / (2 |^ j1)))) & (uDyadic . (i1 * d)) + (uDyadic . (i * ((k + 1) / (2 |^ j1)))) == uDyadic . ((i1 * d) + (i * ((k + 1) / (2 |^ j1)))) ) by SURREALR:10, SURREALR:43, Th27, Th39;
then ((uDyadic . i1) * (uDyadic . d)) + ((uDyadic . i) * (uDyadic . ((k + 1) / (2 |^ j1)))) == uDyadic . ((i1 * d) + (i * ((k + 1) / (2 |^ j1)))) by SURREALO:4;
then ( (((uDyadic . i1) * (uDyadic . d)) + ((uDyadic . i) * (uDyadic . ((k + 1) / (2 |^ j1))))) + (- ((uDyadic . i1) * (uDyadic . ((k + 1) / (2 |^ j1))))) == (uDyadic . ((i1 * d) + (i * ((k + 1) / (2 |^ j1))))) + (uDyadic . (- (i1 * ((k + 1) / (2 |^ j1))))) & (uDyadic . ((i1 * d) + (i * ((k + 1) / (2 |^ j1))))) + (uDyadic . (- (i1 * ((k + 1) / (2 |^ j1))))) == uDyadic . (((i1 * d) + (i * ((k + 1) / (2 |^ j1)))) + (- (i1 * ((k + 1) / (2 |^ j1))))) ) by A26, SURREALR:43, Th39;
then (((uDyadic . i1) * (uDyadic . d)) + ((uDyadic . i) * (uDyadic . ((k + 1) / (2 |^ j1))))) + (- ((uDyadic . i1) * (uDyadic . ((k + 1) / (2 |^ j1))))) == uDyadic . ((((i * ((2 * k) + 1)) - 1) + 2) / (2 |^ (j1 + 1))) by A25, SURREALO:4;
then A27: {((((uDyadic . i1) * (uDyadic . d)) + ((uDyadic . i) * (uDyadic . ((k + 1) / (2 |^ j1))))) + (- ((uDyadic . i1) * (uDyadic . ((k + 1) / (2 |^ j1))))))} <==> {(uDyadic . ((((i * ((2 * k) + 1)) - 1) + 2) / (2 |^ (j1 + 1))))} by SURREALO:32;
A28: comp ((L_ (uDyadic . i)),(uDyadic . i),(uDyadic . d),(R_ (uDyadic . d))) = {((((uDyadic . i1) * (uDyadic . d)) + ((uDyadic . i) * (uDyadic . ((k + 1) / (2 |^ j1))))) - ((uDyadic . i1) * (uDyadic . ((k + 1) / (2 |^ j1)))))} by SURREALR:52, A11, A12;
reconsider DD = [{(uDyadic . (((i * ((2 * k) + 1)) - 1) / (2 |^ (j1 + 1))))},{(uDyadic . ((((i * ((2 * k) + 1)) - 1) + 2) / (2 |^ (j1 + 1))))}] as Surreal by Th38;
(uDyadic . i) * (uDyadic . d) = [((comp ((L_ (uDyadic . i)),(uDyadic . i),(uDyadic . d),(L_ (uDyadic . d)))) \/ (comp ((R_ (uDyadic . i)),(uDyadic . i),(uDyadic . d),(R_ (uDyadic . d))))),((comp ((L_ (uDyadic . i)),(uDyadic . i),(uDyadic . d),(R_ (uDyadic . d)))) \/ (comp ((R_ (uDyadic . i)),(uDyadic . i),(uDyadic . d),(L_ (uDyadic . d)))))] by SURREALR:50
.= [(comp ((L_ (uDyadic . i)),(uDyadic . i),(uDyadic . d),(L_ (uDyadic . d)))),(comp ((L_ (uDyadic . i)),(uDyadic . i),(uDyadic . d),(R_ (uDyadic . d))))] by A13 ;
then A29: ( (uDyadic . i) * (uDyadic . d) == DD & DD == uDyadic . ((((i * ((2 * k) + 1)) - 1) + 1) / (2 |^ (j1 + 1))) ) by A22, A28, A21, A27, SURREALO:29, Th38;
(((i * ((2 * k) + 1)) - 1) + 1) / (2 |^ (j1 + 1)) = i * d by A10, XCMPLX_1:74;
hence (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d) by A29, SURREALO:4; :: thesis: verum

end;

end;

end;

end;

end;

A30: for m being Nat holds S₁[m] from NAT_1:sch 2(A2, A4);
consider n being Nat such that
A31: ( i = n or i = - n ) by INT_1:2;

per cases ( i = n or i = - n ) by A31;

suppose A32: i = n ; :: thesis: (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d)

consider j being Integer, m being Nat such that
A33: d = j / (2 |^ m) by Th18;
A34: d in DYADIC m by A33, Def4;
S₁[n + m] by A30;
hence (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d) by A34, A32; :: thesis: verum

end;

suppose A35: i = - n ; :: thesis: (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d)

consider j being Integer, m being Nat such that
A36: - d = j / (2 |^ m) by Th18;
A37: - d in DYADIC m by A36, Def4;
S₁[n + m] by A30;
then A38: ( (uDyadic . n) * (uDyadic . (- d)) == uDyadic . (n * (- d)) & uDyadic . (n * (- d)) = uDyadic . (i * d) ) by A35, A37;
( uDyadic . i = - (uDyadic . n) & - (uDyadic . (- d)) = uDyadic . (- (- d)) ) by A35, Th27;
hence (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d) by A38, SURREALR:58; :: thesis: verum

end;

end;