let m be non trivial Nat; for M being Jpolynom of m, F_Complex
for f being Function of m,F_Real holds
( eval ((Jsqrt M),f) = 0 iff ex A being Subset of ((Seg m) \ {1}) st the addF of F_Complex "**" (SignGen ((_sqrt (XFS2FS (@ f))), the addF of F_Complex,A)) = 0 )
let M be Jpolynom of m, F_Complex ; for f being Function of m,F_Real holds
( eval ((Jsqrt M),f) = 0 iff ex A being Subset of ((Seg m) \ {1}) st the addF of F_Complex "**" (SignGen ((_sqrt (XFS2FS (@ f))), the addF of F_Complex,A)) = 0 )
let f be Function of m,F_Real; ( eval ((Jsqrt M),f) = 0 iff ex A being Subset of ((Seg m) \ {1}) st the addF of F_Complex "**" (SignGen ((_sqrt (XFS2FS (@ f))), the addF of F_Complex,A)) = 0 )
reconsider F = XFS2FS (@ f) as FinSequence of REAL ;
set MC = the multF of F_Complex;
set AC = the addF of F_Complex;
rng (FS2XFS F) c= COMPLEX
by NUMBERS:11;
then A1:
rng (FS2XFS F) c= the carrier of F_Complex
by COMPLFLD:def 1;
A2:
( len F = len (FS2XFS F) & len (FS2XFS F) = len (@ f) & len (@ f) = m )
by AFINSQ_1:def 8, CARD_1:def 7;
then reconsider xf = FS2XFS F as Function of m,F_Complex by A1, FUNCT_2:2;
A3:
len (_sqrt F) = m
by A2, Def11;
then reconsider cF = _sqrt F as m -element FinSequence of F_Complex by CARD_1:def 7;
A4:
rng (FS2XFS cF) c= the carrier of F_Complex
by RELAT_1:def 19;
dom (FS2XFS cF) = m
by A3, AFINSQ_1:def 8;
then reconsider fcf = FS2XFS cF as Function of m,F_Complex by A4, FUNCT_2:2;
A5:
m > 1
by NEWTON03:def 1;
A6:
Jsqrt M = JsqrtSeries M
by NEWTON03:def 1, Def13;
eval ((Jsqrt M),f) = eval ((JsqrtSeries M),xf)
by A6, Th69;
then
eval ((Jsqrt M),f) = eval (M,fcf)
by Th66;
then A7:
eval ((Jsqrt M),f) = SignGenOp (cF, the multF of F_Complex, the addF of F_Complex,((Seg m) \ {1}))
by A5, Def10;
set B = (Seg m) \ {1};
set theE = the Enumeration of bool ((Seg m) \ {1});
set CE = (SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1});
A8:
SignGenOp (cF, the multF of F_Complex, the addF of F_Complex,((Seg m) \ {1})) = the multF of F_Complex $$ (([#] (dom ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})))),( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))))
by HILB10_7:def 13;
defpred S1[ set ] means for X being Element of Fin (dom ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))) st X = $1 holds
( the multF of F_Complex $$ (X,( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})))) = 0. F_Complex iff ex x being object st
( x in X & 0. F_Complex = ( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))) . x ) );
A9:
the multF of F_Complex = multcomplex
by COMPLFLD:def 1;
the multF of F_Complex $$ (({}. (dom ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})))),( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})))) =
the_unity_wrt the multF of F_Complex
by SETWISEO:31
.=
1
by BINOP_2:6, COMPLFLD:def 1, A9
;
then A10:
S1[ {}. (dom ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})))]
by COMPLFLD:def 1;
A11:
for B9 being Element of Fin (dom ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})))
for b being Element of dom ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})) st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]
proof
let B9 be
Element of
Fin (dom ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})));
for b being Element of dom ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})) st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]let b be
Element of
dom ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}));
( S1[B9] & not b in B9 implies S1[B9 \/ {b}] )
assume A12:
(
S1[
B9] & not
b in B9 )
;
S1[B9 \/ {b}]
let X be
Element of
Fin (dom ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})));
( X = B9 \/ {b} implies ( the multF of F_Complex $$ (X,( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})))) = 0. F_Complex iff ex x being object st
( x in X & 0. F_Complex = ( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))) . x ) ) )
assume A13:
X = B9 \/ {b}
;
( the multF of F_Complex $$ (X,( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})))) = 0. F_Complex iff ex x being object st
( x in X & 0. F_Complex = ( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))) . x ) )
A14:
the
multF of
F_Complex $$ (
X,
( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))))
= ( the multF of F_Complex $$ (B9,( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))))) * (( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))) . b)
by A12, A13, SETWOP_2:2;
thus
( the
multF of
F_Complex $$ (
X,
( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))))
= 0. F_Complex implies ex
x being
object st
(
x in X &
0. F_Complex = ( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))) . x ) )
( ex x being object st
( x in X & 0. F_Complex = ( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))) . x ) implies the multF of F_Complex $$ (X,( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})))) = 0. F_Complex )
given x being
object such that A17:
(
x in X &
0. F_Complex = ( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))) . x )
;
the multF of F_Complex $$ (X,( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})))) = 0. F_Complex
end;
A18:
for B being Element of Fin (dom ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))) holds S1[B]
from SETWISEO:sch 2(A10, A11);
then A19:
( the multF of F_Complex $$ (([#] (dom ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})))),( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})))) = 0. F_Complex iff ex x being object st
( x in [#] (dom ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))) & 0. F_Complex = ( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))) . x ) )
;
A20:
len ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})) = len the Enumeration of bool ((Seg m) \ {1})
by CARD_1:def 7;
then A21:
dom ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})) = dom the Enumeration of bool ((Seg m) \ {1})
by FINSEQ_3:29;
thus
( eval ((Jsqrt M),f) = 0 implies ex A being Subset of ((Seg m) \ {1}) st the addF of F_Complex "**" (SignGen ((_sqrt (XFS2FS (@ f))), the addF of F_Complex,A)) = 0 )
( ex A being Subset of ((Seg m) \ {1}) st the addF of F_Complex "**" (SignGen ((_sqrt (XFS2FS (@ f))), the addF of F_Complex,A)) = 0 implies eval ((Jsqrt M),f) = 0 )proof
assume
eval (
(Jsqrt M),
f)
= 0
;
ex A being Subset of ((Seg m) \ {1}) st the addF of F_Complex "**" (SignGen ((_sqrt (XFS2FS (@ f))), the addF of F_Complex,A)) = 0
then
the
multF of
F_Complex $$ (
([#] (dom ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})))),
( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))))
= 0. F_Complex
by A8, A7, COMPLFLD:def 1;
then consider x being
object such that A22:
(
x in [#] (dom ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))) &
0. F_Complex = ( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))) . x )
by A18;
A23:
x in dom ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))
by A22, HILB10_7:def 1;
then reconsider x =
x as
Nat ;
( the
Enumeration of
bool ((Seg m) \ {1}) . x in rng the
Enumeration of
bool ((Seg m) \ {1}) &
rng the
Enumeration of
bool ((Seg m) \ {1}) = bool ((Seg m) \ {1}) )
by A21, A23, FUNCT_1:def 3, RLAFFIN3:def 1;
then reconsider Ex = the
Enumeration of
bool ((Seg m) \ {1}) . x as
Subset of
((Seg m) \ {1}) ;
take
Ex
;
the addF of F_Complex "**" (SignGen ((_sqrt (XFS2FS (@ f))), the addF of F_Complex,Ex)) = 0
A24:
( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))) . x = the
addF of
F_Complex "**" (((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})) . x)
by A23, HILB10_7:def 10;
x in dom ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))
by A22, HILB10_7:def 1;
then
((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})) . x = SignGen (
cF, the
addF of
F_Complex,
Ex)
by HILB10_7:80;
hence
the
addF of
F_Complex "**" (SignGen ((_sqrt (XFS2FS (@ f))), the addF of F_Complex,Ex)) = 0
by COMPLFLD:def 1, A22, A24;
verum
end;
given A being Subset of ((Seg m) \ {1}) such that A25:
the addF of F_Complex "**" (SignGen ((_sqrt (XFS2FS (@ f))), the addF of F_Complex,A)) = 0
; eval ((Jsqrt M),f) = 0
( A in bool ((Seg m) \ {1}) & bool ((Seg m) \ {1}) = rng the Enumeration of bool ((Seg m) \ {1}) & rng the Enumeration of bool ((Seg m) \ {1}) = bool ((Seg m) \ {1}) )
by RLAFFIN3:def 1;
then consider x being object such that
A26:
( x in dom the Enumeration of bool ((Seg m) \ {1}) & the Enumeration of bool ((Seg m) \ {1}) . x = A )
by FUNCT_1:def 3;
reconsider x = x as Nat by A26;
A27:
x in dom ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))
by A26, A20, FINSEQ_3:29;
A28:
x in [#] (dom ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})))
by A26, A21, HILB10_7:def 1;
A29:
SignGen (cF, the addF of F_Complex,( the Enumeration of bool ((Seg m) \ {1}) . x)) = ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1})) . x
by A26, HILB10_7:80;
the addF of F_Complex "**" (SignGen (cF, the addF of F_Complex,( the Enumeration of bool ((Seg m) \ {1}) . x))) = 0. F_Complex
by A26, A25, COMPLFLD:def 1;
then
( the addF of F_Complex "**" ((SignGenOp (cF, the addF of F_Complex,(bool ((Seg m) \ {1})))) * the Enumeration of bool ((Seg m) \ {1}))) . x = 0. F_Complex
by A29, HILB10_7:def 10, A27;
hence
eval ((Jsqrt M),f) = 0
by A8, A7, A28, A19, COMPLFLD:def 1; verum