let d1, d2 be Dyadic; :: thesis: (uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2)
defpred S1[ Nat] means for n1, n2 being Nat st n1 + n2 <= $1 & n1 <= n2 holds
for d1, d2 being Dyadic st d1 in DYADIC n1 & d2 in DYADIC n2 holds
(uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2);
A1: S1[ 0 ]
proof
let n1, n2 be Nat; :: thesis: ( n1 + n2 <= 0 & n1 <= n2 implies for d1, d2 being Dyadic st d1 in DYADIC n1 & d2 in DYADIC n2 holds
(uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2) )
assume A2: ( n1 + n2 <= 0 & n1 <= n2 ) ; :: thesis: for d1, d2 being Dyadic st d1 in DYADIC n1 & d2 in DYADIC n2 holds
(uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2)
A3: ( n1 = 0 & 0 = n2 ) by A2;
let d1, d2 be Dyadic; :: thesis: ( d1 in DYADIC n1 & d2 in DYADIC n2 implies (uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2) )
assume A4: ( d1 in DYADIC n1 & d2 in DYADIC n2 ) ; :: thesis: (uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2)
reconsider i1 = d1, i2 = d2 as Integer by A4, A3, Th21;
( uDyadic . d1 = uInt . i1 & uDyadic . d2 = uInt . i2 & uDyadic . (d1 + d2) = uInt . (i1 + i2) ) by Def5;
hence (uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2) by Th14; :: thesis: verum
end;
A5: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A6: S1[m] ; :: thesis: S1[m + 1]
set m1 = m + 1;
let n1, n2 be Nat; :: thesis: ( n1 + n2 <= m + 1 & n1 <= n2 implies for d1, d2 being Dyadic st d1 in DYADIC n1 & d2 in DYADIC n2 holds
(uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2) )
assume A7: ( n1 + n2 <= m + 1 & n1 <= n2 ) ; :: thesis: for d1, d2 being Dyadic st d1 in DYADIC n1 & d2 in DYADIC n2 holds
(uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2)
let d1, d2 be Dyadic; :: thesis: ( d1 in DYADIC n1 & d2 in DYADIC n2 implies (uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2) )
assume A8: ( d1 in DYADIC n1 & d2 in DYADIC n2 ) ; :: thesis: (uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2)
per cases ( n1 = 0 or n1 <> 0 ) ;
suppose n1 = 0 ; :: thesis: (uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2)
then reconsider i1 = d1 as Integer by A8, Th21;
(uDyadic . i1) + (uDyadic . d2) == uDyadic . (i1 + d2) by Lm8;
hence (uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2) ; :: thesis: verum
end;
suppose A9: n1 <> 0 ; :: thesis: (uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2)
then reconsider N1 = n1 - 1 as Nat by NAT_1:20;
(N1 + n2) + 1 <= m + 1 by A7;
then A10: N1 + n2 <= m by XREAL_1:6;
n2 <> 0 by A7, A9;
then reconsider N2 = n2 - 1 as Nat by NAT_1:20;
A11: N1 + n2 = n1 + N2 ;
A12: ( ( N1 <= n2 or n2 <= N1 ) & ( n1 <= N2 or N2 <= n1 ) ) ;
per cases ( d1 in DYADIC N1 or d2 in DYADIC N2 or ( not d1 in DYADIC N1 & not d2 in DYADIC N2 ) ) ;
suppose ( d1 in DYADIC N1 or d2 in DYADIC N2 ) ; :: thesis: (uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2)
hence (uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2) by A11, A10, A8, A6, A12; :: thesis: verum
end;
suppose A13: ( not d1 in DYADIC N1 & not d2 in DYADIC N2 ) ; :: thesis: (uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2)
then d1 in (DYADIC (N1 + 1)) \ (DYADIC N1) by A8, XBOOLE_0:def 5;
then consider i1 being Integer such that
A14: d1 = ((2 * i1) + 1) / (2 |^ (N1 + 1)) by Th20;
d2 in (DYADIC (N2 + 1)) \ (DYADIC N2) by A8, A13, XBOOLE_0:def 5;
then consider i2 being Integer such that
A15: d2 = ((2 * i2) + 1) / (2 |^ (N2 + 1)) by Th20;
A16: uDyadic . d1 = [{(uDyadic . (i1 / (2 |^ N1)))},{(uDyadic . ((i1 + 1) / (2 |^ N1)))}] by A14, Def5;
A17: uDyadic . d2 = [{(uDyadic . (i2 / (2 |^ N2)))},{(uDyadic . ((i2 + 1) / (2 |^ N2)))}] by A15, Def5;
i1 / (2 |^ N1) in DYADIC N1 by Def4;
then A18: (uDyadic . (i1 / (2 |^ N1))) + (uDyadic . d2) == uDyadic . ((i1 / (2 |^ N1)) + d2) by A10, A8, A6, A12;
(L_ (uDyadic . d1)) ++ {(uDyadic . d2)} = {((uDyadic . (i1 / (2 |^ N1))) + (uDyadic . d2))} by A16, SURREALR:36;
then A19: (L_ (uDyadic . d1)) ++ {(uDyadic . d2)} <==> {(uDyadic . ((i1 / (2 |^ N1)) + d2))} by A18, SURREALO:32;
i2 / (2 |^ N2) in DYADIC N2 by Def4;
then A20: (uDyadic . d1) + (uDyadic . (i2 / (2 |^ N2))) == uDyadic . (d1 + (i2 / (2 |^ N2))) by A11, A10, A8, A6, A12;
{(uDyadic . d1)} ++ (L_ (uDyadic . d2)) = {((uDyadic . d1) + (uDyadic . (i2 / (2 |^ N2))))} by A17, SURREALR:36;
then A21: {(uDyadic . d1)} ++ (L_ (uDyadic . d2)) <==> {(uDyadic . (d1 + (i2 / (2 |^ N2))))} by A20, SURREALO:32;
(i1 + 1) / (2 |^ N1) in DYADIC N1 by Def4;
then A22: (uDyadic . ((i1 + 1) / (2 |^ N1))) + (uDyadic . d2) == uDyadic . (((i1 + 1) / (2 |^ N1)) + d2) by A10, A8, A6, A12;
(R_ (uDyadic . d1)) ++ {(uDyadic . d2)} = {((uDyadic . ((i1 + 1) / (2 |^ N1))) + (uDyadic . d2))} by A16, SURREALR:36;
then A23: (R_ (uDyadic . d1)) ++ {(uDyadic . d2)} <==> {(uDyadic . (((i1 + 1) / (2 |^ N1)) + d2))} by A22, SURREALO:32;
(i2 + 1) / (2 |^ N2) in DYADIC N2 by Def4;
then A24: (uDyadic . d1) + (uDyadic . ((i2 + 1) / (2 |^ N2))) == uDyadic . (d1 + ((i2 + 1) / (2 |^ N2))) by A11, A10, A8, A6, A12;
{(uDyadic . d1)} ++ (R_ (uDyadic . d2)) = {((uDyadic . d1) + (uDyadic . ((i2 + 1) / (2 |^ N2))))} by A17, SURREALR:36;
then A25: {(uDyadic . d1)} ++ (R_ (uDyadic . d2)) <==> {(uDyadic . (d1 + ((i2 + 1) / (2 |^ N2))))} by A24, SURREALO:32;
A26: ( ((L_ (uDyadic . d1)) ++ {(uDyadic . d2)}) \/ ({(uDyadic . d1)} ++ (L_ (uDyadic . d2))) <==> {(uDyadic . ((i1 / (2 |^ N1)) + d2))} \/ {(uDyadic . (d1 + (i2 / (2 |^ N2))))} & {(uDyadic . ((i1 / (2 |^ N1)) + d2))} \/ {(uDyadic . (d1 + (i2 / (2 |^ N2))))} = {(uDyadic . ((i1 / (2 |^ N1)) + d2)),(uDyadic . (d1 + (i2 / (2 |^ N2))))} ) by A19, A21, SURREALO:31, ENUMSET1:1;
A27: ( ((R_ (uDyadic . d1)) ++ {(uDyadic . d2)}) \/ ({(uDyadic . d1)} ++ (R_ (uDyadic . d2))) <==> {(uDyadic . (((i1 + 1) / (2 |^ N1)) + d2))} \/ {(uDyadic . (d1 + ((i2 + 1) / (2 |^ N2))))} & {(uDyadic . (((i1 + 1) / (2 |^ N1)) + d2))} \/ {(uDyadic . (d1 + ((i2 + 1) / (2 |^ N2))))} = {(uDyadic . (((i1 + 1) / (2 |^ N1)) + d2)),(uDyadic . (d1 + ((i2 + 1) / (2 |^ N2))))} ) by A23, A25, SURREALO:31, ENUMSET1:1;
A28: (uDyadic . d1) + (uDyadic . d2) = [(((L_ (uDyadic . d1)) ++ {(uDyadic . d2)}) \/ ({(uDyadic . d1)} ++ (L_ (uDyadic . d2)))),(((R_ (uDyadic . d1)) ++ {(uDyadic . d2)}) \/ ({(uDyadic . d1)} ++ (R_ (uDyadic . d2))))] by SURREALR:28;
reconsider DD = [{(uDyadic . ((i1 / (2 |^ N1)) + d2)),(uDyadic . (d1 + (i2 / (2 |^ N2))))},{(uDyadic . (((i1 + 1) / (2 |^ N1)) + d2)),(uDyadic . (d1 + ((i2 + 1) / (2 |^ N2))))}] as Surreal by A28, TARSKI:1, A26, A27, SURREALI:37;
DD = DD ;
then reconsider DD1 = [{(uDyadic . (d1 + (i2 / (2 |^ N2))))},{(uDyadic . (((i1 + 1) / (2 |^ N1)) + d2)),(uDyadic . (d1 + ((i2 + 1) / (2 |^ N2))))}] as Surreal by SURREALO:26;
DD1 = DD1 ;
then reconsider DD2 = [{(uDyadic . (d1 + (i2 / (2 |^ N2))))},{(uDyadic . (d1 + ((i2 + 1) / (2 |^ N2))))}] as Surreal by SURREALO:28;
N1 + 1 <= n2 by A7;
then ( N1 < n2 & n2 = N2 + 1 ) by NAT_1:13;
then N1 <= N2 by NAT_1:13;
then reconsider N = N2 - N1 as Nat by NAT_1:21;
set 2N1 = 2 |^ N1;
set 2N2 = 2 |^ N2;
set P = 2 |^ N;
A29: ( 2 |^ (N1 + 1) = 2 * (2 |^ N1) & 2 |^ (N2 + 1) = 2 * (2 |^ N2) ) by NEWTON:6;
N2 = N1 + N ;
then A30: 2 |^ N2 = (2 |^ N1) * (2 |^ N) by NEWTON:8;
A31: (i1 / (2 |^ N1)) + d2 = ((i1 * ((2 |^ N) * 2)) / ((2 |^ N1) * ((2 |^ N) * 2))) + (((2 * i2) + 1) / (2 * (2 |^ N2))) by A15, A29, XCMPLX_1:91
.= ((i1 * ((2 |^ N) * 2)) + ((2 * i2) + 1)) / (2 * (2 |^ N2)) by XCMPLX_1:62, A30
.= ((2 * (((2 |^ N) * i1) + i2)) + 1) / (2 * (2 |^ N2)) ;
A32: d1 + (i2 / (2 |^ N2)) = ((((2 * i1) + 1) * (2 |^ N)) / (((2 |^ N1) * 2) * (2 |^ N))) + (i2 / (2 |^ N2)) by A14, A29, XCMPLX_1:91
.= ((((2 * i1) + 1) * (2 |^ N)) / ((2 |^ N2) * 2)) + ((i2 * 2) / ((2 |^ N2) * 2)) by A30, XCMPLX_1:91
.= ((((2 * i1) + 1) * (2 |^ N)) + (i2 * 2)) / ((2 |^ N2) * 2) by XCMPLX_1:62
.= ((2 * (((2 |^ N) * i1) + i2)) + (2 |^ N)) / (2 * (2 |^ N2)) ;
(2 * (((2 |^ N) * i1) + i2)) + 1 <= (2 * (((2 |^ N) * i1) + i2)) + (2 |^ N) by NAT_1:14, XREAL_1:6;
then (i1 / (2 |^ N1)) + d2 <= d1 + (i2 / (2 |^ N2)) by A31, A32, XREAL_1:72;
then A33: DD == DD1 by Th24, SURREALO:25;
A34: ((i1 + 1) / (2 |^ N1)) + d2 = (((i1 + 1) * ((2 |^ N) * 2)) / ((2 |^ N1) * ((2 |^ N) * 2))) + (((2 * i2) + 1) / (2 * (2 |^ N2))) by A15, A29, XCMPLX_1:91
.= (((i1 + 1) * ((2 |^ N) * 2)) + ((2 * i2) + 1)) / (2 * (2 |^ N2)) by XCMPLX_1:62, A30
.= ((2 * (((2 |^ N) * i1) + i2)) + ((2 * (2 |^ N)) + 1)) / (2 * (2 |^ N2)) ;
A35: d1 + ((i2 + 1) / (2 |^ N2)) = ((((2 * i1) + 1) * (2 |^ N)) / (((2 |^ N1) * 2) * (2 |^ N))) + ((i2 + 1) / (2 |^ N2)) by A29, XCMPLX_1:91, A14
.= ((((2 * i1) + 1) * (2 |^ N)) / ((2 |^ N2) * 2)) + (((i2 + 1) * 2) / ((2 |^ N2) * 2)) by A30, XCMPLX_1:91
.= ((((2 * i1) + 1) * (2 |^ N)) + ((i2 + 1) * 2)) / ((2 |^ N2) * 2) by XCMPLX_1:62
.= ((2 * (((2 |^ N) * i1) + i2)) + ((2 |^ N) + 2)) / (2 * (2 |^ N2)) ;
1 + ((2 |^ N) + 1) <= (2 |^ N) + ((2 |^ N) + 1) by NAT_1:14, XREAL_1:6;
then (2 * (((2 |^ N) * i1) + i2)) + ((2 |^ N) + 2) <= (2 * (((2 |^ N) * i1) + i2)) + ((2 * (2 |^ N)) + 1) by XREAL_1:6;
then d1 + ((i2 + 1) / (2 |^ N2)) <= ((i1 + 1) / (2 |^ N1)) + d2 by A34, A35, XREAL_1:72;
then A36: DD1 == DD2 by Th24, SURREALO:27;
(uDyadic . d1) + (uDyadic . d2) == DD by A28, A26, A27, SURREALO:29;
then (uDyadic . d1) + (uDyadic . d2) == DD1 by A33, SURREALO:4;
then A37: (uDyadic . d1) + (uDyadic . d2) == DD2 by A36, SURREALO:4;
d1 = (((2 * i1) + 1) * (2 |^ N)) / ((2 * (2 |^ N1)) * (2 |^ N)) by A29, XCMPLX_1:91, A14;
then A38: d1 + d2 = ((((2 * i1) + 1) * (2 |^ N)) + ((2 * i2) + 1)) / (2 * (2 |^ N2)) by XCMPLX_1:62, A29, A30, A15
.= ((2 * ((i1 * (2 |^ N)) + i2)) + ((2 |^ N) + 1)) / (2 * (2 |^ N2)) ;
per cases ( N1 <> N2 or N1 = N2 ) ;
suppose N1 <> N2 ; :: thesis: (uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2)
then N <> 0 ;
then reconsider nn = N - 1 as Nat by NAT_1:14, NAT_1:21;
set 2n = 2 |^ nn;
N = nn + 1 ;
then A39: 2 |^ N = 2 * (2 |^ nn) by NEWTON:6;
A40: d1 + (i2 / (2 |^ N2)) = (2 * ((((2 |^ N) * i1) + i2) + (2 |^ nn))) / (2 * (2 |^ N2)) by A39, A32
.= ((((2 |^ N) * i1) + i2) + (2 |^ nn)) / (2 |^ N2) by XCMPLX_1:91 ;
A41: d1 + ((i2 + 1) / (2 |^ N2)) = (2 * (((((2 |^ N) * i1) + i2) + (2 |^ nn)) + 1)) / (2 * (2 |^ N2)) by A35, A39
.= (((((2 |^ N) * i1) + i2) + (2 |^ nn)) + 1) / (2 |^ N2) by XCMPLX_1:91 ;
d1 + d2 = ((2 * (((i1 * (2 |^ N)) + i2) + (2 |^ nn))) + 1) / (2 |^ (N2 + 1)) by NEWTON:6, A39, A38;
hence (uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2) by A37, A40, A41, Def5; :: thesis: verum
end;
suppose N1 = N2 ; :: thesis: (uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2)
then A42: 2 |^ N = 1 by NEWTON:4;
then A43: d1 + d2 = (((2 * (i1 + i2)) + 1) + 1) / (2 |^ (N2 + 1)) by NEWTON:6, A38;
A44: d1 + (i2 / (2 |^ N2)) = ((2 * (i1 + i2)) + 1) / (2 |^ (N2 + 1)) by A42, A32, NEWTON:6;
d1 + ((i2 + 1) / (2 |^ N2)) = (((2 * (i1 + i2)) + 1) + 2) / (2 |^ (N2 + 1)) by NEWTON:6, A42, A35;
then DD2 == uDyadic . (d1 + d2) by A43, A44, Th38;
hence (uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2) by A37, SURREALO:4; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
A45: for m being Nat holds S1[m] from NAT_1:sch 2(A1, A5);
 consider i1 being Integer, n1 being Nat such that
A46: d1 = i1 / (2 |^ n1) by Th18;
consider i2 being Integer, n2 being Nat such that
A47: d2 = i2 / (2 |^ n2) by Th18;
A48: ( d2 in DYADIC n2 & DYADIC n2 c= DYADIC (n1 + n2) ) by A47, Def4, Th19, NAT_1:11;
A49: d1 in DYADIC n1 by A46, Def4;
A50: n1 <= n1 + n2 by NAT_1:11;
S1[n1 + (n1 + n2)] by A45;
hence (uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2) by A48, A49, A50; :: thesis: verum