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 i + j <= 0 ; :: thesis: for d being Dyadic st d in DYADIC j holds
(uDyadic . i) + (uDyadic . d) == uDyadic . (i + d)
then i = 0 ;
hence for d being Dyadic st d in DYADIC j holds
(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 Th14;
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;
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;
i1 + j = m by A8;
then A13: (uDyadic . i1) + (uDyadic . d) == uDyadic . (i1 + d) by A7, A5;
(L_ (uDyadic . i)) ++ {(uDyadic . d)} = {((uInt . i1) + (uDyadic . d))} by A12, SURREALR:36
.= {((uDyadic . i1) + (uDyadic . d))} by Def5 ;
then A14: (L_ (uDyadic . i)) ++ {(uDyadic . d)} <==> {(uDyadic . (i1 + d))} by SURREALO:32, A13;
A15: k / (2 |^ j1) in DYADIC j1 by Def4;
m = i + j1 by A8;
then A16: (uDyadic . i) + (uDyadic . (k / (2 |^ j1))) == uDyadic . (i + (k / (2 |^ j1))) by A15, A5;
{(uDyadic . i)} ++ (L_ (uDyadic . d)) = {((uDyadic . i) + (uDyadic . (k / (2 |^ j1))))} by A11, SURREALR:36;
then {(uDyadic . i)} ++ (L_ (uDyadic . d)) <==> {(uDyadic . (i + (k / (2 |^ j1))))} by SURREALO:32, A16;
then A17: ((L_ (uDyadic . i)) ++ {(uDyadic . d)}) \/ ({(uDyadic . i)} ++ (L_ (uDyadic . d))) <==> {(uDyadic . (i1 + d))} \/ {(uDyadic . (i + (k / (2 |^ j1))))} by A14, SURREALO:31;
A18: (R_ (uDyadic . i)) ++ {(uDyadic . d)} = {} by SURREALR:27, A12;
A19: (k + 1) / (2 |^ j1) in DYADIC j1 by Def4;
m = i + j1 by A8;
then A20: (uDyadic . i) + (uDyadic . ((k + 1) / (2 |^ j1))) == uDyadic . (i + ((k + 1) / (2 |^ j1))) by A19, A5;
{(uDyadic . i)} ++ (R_ (uDyadic . d)) = {((uDyadic . i) + (uDyadic . ((k + 1) / (2 |^ j1))))} by SURREALR:36, A11;
then A21: ((R_ (uDyadic . i)) ++ {(uDyadic . d)}) \/ ({(uDyadic . i)} ++ (R_ (uDyadic . d))) <==> {(uDyadic . (i + ((k + 1) / (2 |^ j1))))} by A18, SURREALO:32, A20;
A22: (uDyadic . i) + (uDyadic . d) = [(((L_ (uDyadic . i)) ++ {(uDyadic . d)}) \/ ({(uDyadic . i)} ++ (L_ (uDyadic . d)))),(((R_ (uDyadic . i)) ++ {(uDyadic . d)}) \/ ({(uDyadic . i)} ++ (R_ (uDyadic . d))))] by SURREALR:28;
then [({(uDyadic . (i1 + d))} \/ {(uDyadic . (i + (k / (2 |^ j1))))}),{(uDyadic . (i + ((k + 1) / (2 |^ j1))))}] is surreal by A17, A21, SURREALI:37;
then reconsider DD = [({(uDyadic . (i1 + d))} \/ {(uDyadic . (i + (k / (2 |^ j1))))}),{(uDyadic . (i + ((k + 1) / (2 |^ j1))))}] as Surreal ;
A23: {(uDyadic . (i1 + d))} \/ {(uDyadic . (i + (k / (2 |^ j1))))} = {(uDyadic . (i1 + d)),(uDyadic . (i + (k / (2 |^ j1))))} by ENUMSET1:1;
(i * (2 |^ j1)) + (k + 1) = ((i * (2 |^ j1)) + k) + 1 ;
then A24: ( ((i * (2 |^ j1)) + k) / (2 |^ j1) = i + (k / (2 |^ j1)) & (((i * (2 |^ j1)) + k) + 1) / (2 |^ j1) = i + ((k + 1) / (2 |^ j1)) ) by XCMPLX_1:113;
A25: 2 |^ (j1 + 1) = 2 * (2 |^ j1) by NEWTON:6;
i + d = ((i * (2 * (2 |^ j1))) + ((2 * k) + 1)) / (2 |^ (j1 + 1)) by A10, A25, XCMPLX_1:113
.= ((2 * ((i * (2 |^ j1)) + k)) + 1) / (2 |^ (j1 + 1)) ;
then A26: uDyadic . (i + d) = [{(uDyadic . (i + (k / (2 |^ j1))))},{(uDyadic . (i + ((k + 1) / (2 |^ j1))))}] by A24, Def5;
(2 * k) + 1 <= (2 * k) + ((2 |^ j1) * 2) by NAT_1:14, XREAL_1:6;
then ((2 * k) + 1) * (2 |^ j1) <= (((1 * (2 |^ j1)) + k) * 2) * (2 |^ j1) by XREAL_1:64;
then ((2 * k) + 1) * (2 |^ j1) <= ((1 * (2 |^ j1)) + k) * (2 |^ (j1 + 1)) by A25;
then ((2 * k) + 1) / (2 |^ (j1 + 1)) <= ((1 * (2 |^ j1)) + k) / (2 |^ j1) by XREAL_1:102;
then d <= (k / (2 |^ j1)) + 1 by A10, XCMPLX_1:113;
then d + i1 <= ((k / (2 |^ j1)) + 1) + i1 by XREAL_1:6;
then A27: DD == uDyadic . (i + d) by A26, SURREALO:25, A23, Th24;
(uDyadic . i) + (uDyadic . d) == DD by A22, A17, A21, SURREALO:29;
hence (uDyadic . i) + (uDyadic . d) == uDyadic . (i + d) by A27, SURREALO:4; :: thesis: verum

end;

end;

end;

end;

end;

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

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

suppose A30: i = n ; :: thesis: (uDyadic . i) + (uDyadic . d) == uDyadic . (i + d)

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

end;

suppose A33: i = - n ; :: thesis: (uDyadic . i) + (uDyadic . d) == uDyadic . (i + d)

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

end;

end;