let x be Surreal; :: thesis: ( 0_No < x implies ex y being Surreal st
( - 1_No == y & sqrt y < - x & y = [{},{0_No,(((sqrt ((x * x) + 1_No)) - x) * ((sqrt ((x * x) + 1_No)) - x))}] ) )
assume A1: 0_No < x ; :: thesis: ex y being Surreal st
( - 1_No == y & sqrt y < - x & y = [{},{0_No,(((sqrt ((x * x) + 1_No)) - x) * ((sqrt ((x * x) + 1_No)) - x))}] )
reconsider p = x as positive Surreal by A1, SURREALI:def 8;
A2: - 1_No = [(-- (R_ 1_No)),(-- (L_ 1_No))] by SURREALR:7
.= [{},{(- 0_No)}] by SURREALR:21, SURREALR:22 ;
A3: 0_No <= x by A1;
then A4: x * 0_No <= x * x by SURREALR:75;
A5: (x * x) + 0_No < (x * x) + 1_No by SURREALR:44, SURREALI:def 8;
then ( x == sqrt (x * x) & sqrt (x * x) < sqrt ((x * x) + 1_No) ) by A4, Th27, A3, Th29;
then x < sqrt ((x * x) + 1_No) by SURREALO:4;
then 0_No < (sqrt ((x * x) + 1_No)) - x by SURREALR:45;
then reconsider Y = (sqrt ((x * x) + 1_No)) + (- x) as positive Surreal by SURREALI:def 8;
set YY = Y * Y;
{0_No} \/ {(Y * Y)} is surreal-membered ;
then reconsider Y0 = {0_No,(Y * Y)} as surreal-membered set by ENUMSET1:1;
consider M being Ordinal such that
A6: for o being object st o in {} \/ Y0 holds
ex A being Ordinal st
( A in M & o in Day A ) by SURREAL0:47;
{} << Y0 ;
then [{},Y0] in Day M by A6, SURREAL0:46;
then reconsider y = [{},Y0] as Surreal ;
take y ; :: thesis: ( - 1_No == y & sqrt y < - x & y = [{},{0_No,(((sqrt ((x * x) + 1_No)) - x) * ((sqrt ((x * x) + 1_No)) - x))}] )
A7: 0_No <= Y * Y by SURREALI:def 8;
A8: for z being Surreal st z in R_ y holds
0_No <= z by A7, TARSKI:def 2;
A9: - 1_No = [(L_ y),{0_No}] by A2;
0_No in R_ y by TARSKI:def 2;
hence A10: - 1_No == y by A9, A8, SURREALO:24; :: thesis: ( sqrt y < - x & y = [{},{0_No,(((sqrt ((x * x) + 1_No)) - x) * ((sqrt ((x * x) + 1_No)) - x))}] )
(sqrt (Y * Y)) + (sqrt (Y * Y)) is positive ;
then A11: not (sqrt (Y * Y)) + (sqrt (Y * Y)) == 0_No ;
Y * Y in R_ y by TARSKI:def 2;
then Y * Y in R_ (NonNegativePart y) by A7, Def1;
then sqrt (Y * Y) in R_ (sqrt_0 y) by Def9;
then sqrt (Y * Y) in (sqrtR ((sqrt_0 y),y)) . 0 by Th6;
then A12: (y + ((sqrt (Y * Y)) * (sqrt (Y * Y)))) * (((sqrt (Y * Y)) + (sqrt (Y * Y))) ") in sqrt (y,((sqrtR ((sqrt_0 y),y)) . 0),((sqrtR ((sqrt_0 y),y)) . 0)) by A11, Def2;
sqrt y = [(Union (sqrtL ((sqrt_0 y),y))),(Union (sqrtR ((sqrt_0 y),y)))] by Th15;
then A13: ( {(sqrt y)} << R_ (sqrt y) & R_ (sqrt y) = Union (sqrtR ((sqrt_0 y),y)) & sqrt y in {(sqrt y)} ) by TARSKI:def 1, SURREALO:11;
(sqrtR ((sqrt_0 y),y)) . (0 + 1) = (((sqrtR ((sqrt_0 y),y)) . 0) \/ (sqrt (y,((sqrtL ((sqrt_0 y),y)) . 0),((sqrtL ((sqrt_0 y),y)) . 0)))) \/ (sqrt (y,((sqrtR ((sqrt_0 y),y)) . 0),((sqrtR ((sqrt_0 y),y)) . 0))) by Th8;
then A14: ( (y + ((sqrt (Y * Y)) * (sqrt (Y * Y)))) * (((sqrt (Y * Y)) + (sqrt (Y * Y))) ") in (sqrtR ((sqrt_0 y),y)) . 1 & (sqrtR ((sqrt_0 y),y)) . 1 c= Union (sqrtR ((sqrt_0 y),y)) ) by ABCMIZ_1:1, XBOOLE_0:def 3, A12;
set TWO = 1_No + 1_No;
A15: ( not 0_No == Y " & not 0_No == Y & not 1_No + 1_No == 0_No ) by SURREALI:def 8;
then A16: ( (Y ") " == Y & Y * (Y ") == 1_No & (1_No + 1_No) * ((1_No + 1_No) ") == 1_No ) by SURREALI:44, SURREALI:33;
0_No <= Y by SURREALI:def 8;
then sqrt (Y * Y) == Y by Th29;
then ( (sqrt (Y * Y)) + (sqrt (Y * Y)) == Y + Y & Y + Y = (1_No * Y) + (1_No * Y) & (1_No * Y) + (1_No * Y) == (1_No + 1_No) * Y ) by SURREALR:66, SURREALR:67;
then (sqrt (Y * Y)) + (sqrt (Y * Y)) == (1_No + 1_No) * Y by SURREALO:4;
then ( ((sqrt (Y * Y)) + (sqrt (Y * Y))) " == ((1_No + 1_No) * Y) " & ((1_No + 1_No) * Y) " == ((1_No + 1_No) ") * (Y ") ) by A11, A15, SURREALI:43, SURREALI:45;
then A17: ((sqrt (Y * Y)) + (sqrt (Y * Y))) " == ((1_No + 1_No) ") * (Y ") by SURREALO:4;
A18: (sqrt (Y * Y)) * (sqrt (Y * Y)) == Y * Y by A7, Th19;
A19: Y * Y == (((sqrt ((x * x) + 1_No)) * (sqrt ((x * x) + 1_No))) + ((- x) * (- x))) + (((sqrt ((x * x) + 1_No)) * (- x)) + ((- x) * (sqrt ((x * x) + 1_No)))) by SURREALR:76;
0_No <= (x * x) + 1_No by A4, A5, SURREALO:4;
then ( (sqrt ((x * x) + 1_No)) * (sqrt ((x * x) + 1_No)) == (x * x) + 1_No & (- x) * (- x) = x * x ) by Th19, SURREALR:58;
then A20: ( ((sqrt ((x * x) + 1_No)) * (sqrt ((x * x) + 1_No))) + ((- x) * (- x)) == ((x * x) + 1_No) + (x * x) & ((x * x) + 1_No) + (x * x) = 1_No + ((x * x) + (x * x)) ) by SURREALR:37, SURREALR:66;
x * x = 1_No * (x * x) ;
then (x * x) + (x * x) == (1_No + 1_No) * (x * x) by SURREALR:67;
then 1_No + ((x * x) + (x * x)) == 1_No + ((1_No + 1_No) * (x * x)) by SURREALR:66;
then A21: ((sqrt ((x * x) + 1_No)) * (sqrt ((x * x) + 1_No))) + ((- x) * (- x)) == 1_No + ((1_No + 1_No) * (x * x)) by A20, SURREALO:4;
1_No * ((sqrt ((x * x) + 1_No)) * (- x)) = (sqrt ((x * x) + 1_No)) * (- x) ;
then ((sqrt ((x * x) + 1_No)) * (- x)) + ((sqrt ((x * x) + 1_No)) * (- x)) == (1_No + 1_No) * ((sqrt ((x * x) + 1_No)) * (- x)) by SURREALR:67;
then (((sqrt ((x * x) + 1_No)) * (sqrt ((x * x) + 1_No))) + ((- x) * (- x))) + (((sqrt ((x * x) + 1_No)) * (- x)) + ((- x) * (sqrt ((x * x) + 1_No)))) == (1_No + ((1_No + 1_No) * (x * x))) + ((1_No + 1_No) * ((sqrt ((x * x) + 1_No)) * (- x))) by A21, SURREALR:66;
then Y * Y == (1_No + ((1_No + 1_No) * (x * x))) + ((1_No + 1_No) * ((sqrt ((x * x) + 1_No)) * (- x))) by A19, SURREALO:4;
then A22: ( (sqrt (Y * Y)) * (sqrt (Y * Y)) == (1_No + ((1_No + 1_No) * (x * x))) + ((1_No + 1_No) * ((sqrt ((x * x) + 1_No)) * (- x))) & (1_No + ((1_No + 1_No) * (x * x))) + ((1_No + 1_No) * ((sqrt ((x * x) + 1_No)) * (- x))) = 1_No + (((1_No + 1_No) * (x * x)) + ((1_No + 1_No) * ((sqrt ((x * x) + 1_No)) * (- x)))) ) by A18, SURREALO:4, SURREALR:37;
A23: 1_No - 1_No == 0_No by SURREALR:39;
x * x = (- x) * (- x) by SURREALR:58;
then ( ((1_No + 1_No) * (x * x)) + ((1_No + 1_No) * ((sqrt ((x * x) + 1_No)) * (- x))) == (1_No + 1_No) * ((x * x) + ((sqrt ((x * x) + 1_No)) * (- x))) & (1_No + 1_No) * ((x * x) + ((sqrt ((x * x) + 1_No)) * (- x))) == (1_No + 1_No) * ((- x) * Y) ) by SURREALR:54, SURREALR:67;
then ((1_No + 1_No) * (x * x)) + ((1_No + 1_No) * ((sqrt ((x * x) + 1_No)) * (- x))) == (1_No + 1_No) * ((- x) * Y) by SURREALO:4;
then 1_No + (((1_No + 1_No) * (x * x)) + ((1_No + 1_No) * ((sqrt ((x * x) + 1_No)) * (- x)))) == 1_No + ((1_No + 1_No) * ((- x) * Y)) by SURREALR:66;
then (sqrt (Y * Y)) * (sqrt (Y * Y)) == 1_No + ((1_No + 1_No) * ((- x) * Y)) by A22, SURREALO:4;
then ( y + ((sqrt (Y * Y)) * (sqrt (Y * Y))) == (- 1_No) + (1_No + ((1_No + 1_No) * ((- x) * Y))) & (- 1_No) + (1_No + ((1_No + 1_No) * ((- x) * Y))) = (1_No - 1_No) + ((1_No + 1_No) * ((- x) * Y)) & (1_No - 1_No) + ((1_No + 1_No) * ((- x) * Y)) == 0_No + ((1_No + 1_No) * ((- x) * Y)) ) by A23, A10, SURREALR:66, SURREALR:37;
then y + ((sqrt (Y * Y)) * (sqrt (Y * Y))) == (1_No + 1_No) * ((- x) * Y) by SURREALO:4;
then ( (y + ((sqrt (Y * Y)) * (sqrt (Y * Y)))) * (((sqrt (Y * Y)) + (sqrt (Y * Y))) ") == ((1_No + 1_No) * ((- x) * Y)) * (((sqrt (Y * Y)) + (sqrt (Y * Y))) ") & ((1_No + 1_No) * ((- x) * Y)) * (((sqrt (Y * Y)) + (sqrt (Y * Y))) ") == ((1_No + 1_No) * ((- x) * Y)) * (((1_No + 1_No) ") * (Y ")) ) by A17, SURREALR:54;
then A24: (y + ((sqrt (Y * Y)) * (sqrt (Y * Y)))) * (((sqrt (Y * Y)) + (sqrt (Y * Y))) ") == ((1_No + 1_No) * ((- x) * Y)) * (((1_No + 1_No) ") * (Y ")) by SURREALO:4;
( ((1_No + 1_No) * ((- x) * Y)) * (((1_No + 1_No) ") * (Y ")) == ((- x) * ((1_No + 1_No) * Y)) * (((1_No + 1_No) ") * (Y ")) & ((- x) * ((1_No + 1_No) * Y)) * (((1_No + 1_No) ") * (Y ")) == (- x) * (((1_No + 1_No) * Y) * (((1_No + 1_No) ") * (Y "))) ) by SURREALR:69, SURREALR:54;
then A25: ((1_No + 1_No) * ((- x) * Y)) * (((1_No + 1_No) ") * (Y ")) == (- x) * (((1_No + 1_No) * Y) * (((1_No + 1_No) ") * (Y "))) by SURREALO:4;
( ((1_No + 1_No) * Y) * (((1_No + 1_No) ") * (Y ")) == (((1_No + 1_No) * Y) * ((1_No + 1_No) ")) * (Y ") & (((1_No + 1_No) * Y) * ((1_No + 1_No) ")) * (Y ") == (Y * ((1_No + 1_No) * ((1_No + 1_No) "))) * (Y ") ) by SURREALR:69, SURREALR:54;
then ( ((1_No + 1_No) * Y) * (((1_No + 1_No) ") * (Y ")) == (Y * ((1_No + 1_No) * ((1_No + 1_No) "))) * (Y ") & (Y * ((1_No + 1_No) * ((1_No + 1_No) "))) * (Y ") == ((1_No + 1_No) * ((1_No + 1_No) ")) * (Y * (Y ")) ) by SURREALR:69, SURREALO:4;
then ( ((1_No + 1_No) * Y) * (((1_No + 1_No) ") * (Y ")) == ((1_No + 1_No) * ((1_No + 1_No) ")) * (Y * (Y ")) & ((1_No + 1_No) * ((1_No + 1_No) ")) * (Y * (Y ")) == ((1_No + 1_No) * ((1_No + 1_No) ")) * 1_No ) by A16, SURREALR:54, SURREALO:4;
then ((1_No + 1_No) * Y) * (((1_No + 1_No) ") * (Y ")) == (1_No + 1_No) * ((1_No + 1_No) ") by SURREALO:4;
then ((1_No + 1_No) * Y) * (((1_No + 1_No) ") * (Y ")) == 1_No by A16, SURREALO:4;
then (- x) * (((1_No + 1_No) * Y) * (((1_No + 1_No) ") * (Y "))) == (- x) * 1_No by SURREALR:54;
then ((1_No + 1_No) * ((- x) * Y)) * (((1_No + 1_No) ") * (Y ")) == (- x) * 1_No by A25, SURREALO:4;
then (y + ((sqrt (Y * Y)) * (sqrt (Y * Y)))) * (((sqrt (Y * Y)) + (sqrt (Y * Y))) ") == - x by A24, SURREALO:4;
hence ( sqrt y < - x & y = [{},{0_No,(((sqrt ((x * x) + 1_No)) - x) * ((sqrt ((x * x) + 1_No)) - x))}] ) by A14, A13, SURREALO:4; :: thesis: verum