POLYNOM9: Prime Representing Polynomial with 10 Unknowns

proof end;

let x be object ;

cluster b +* (x,n) -> finite-support ;

proof end;

end;

theorem :: POLYNOM9:10

for X being set
for b being bag of X holds 0 (#) b = EmptyBag X

proof end;

theorem :: POLYNOM9:11

for n being Ordinal
for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for x being Function of n,L
for b being bag of n
for i being Nat st i <> 0 holds
eval ((i (#) b),x) = (power L) . ((eval (b,x)),i)

proof end;

theorem Th12: :: POLYNOM9:12

for X being non empty set
for x being Element of X
for i being Element of NAT holds (EmptyBag X) +* (x,i) = ({x},i) -bag

proof end;

theorem Th13: :: POLYNOM9:13

for X being set
for x being object
for i being Nat st x in X & i <> 0 holds
support ((EmptyBag X) +* (x,i)) = {x}

proof end;

theorem Th14: :: POLYNOM9:14

for i being Nat
for x being object
for n being Ordinal
for L being non trivial well-unital doubleLoopStr
for y being Function of n,L st x in n holds
eval (((EmptyBag n) +* (x,i)),y) = (power L) . ((y . x),i)

proof end;

theorem Th15: :: POLYNOM9:15

for X being set
for x being object
for b being bag of X holds b = (b +* (x,0)) + ((EmptyBag X) +* (x,(b . x)))

proof end;

theorem Th16: :: POLYNOM9:16

for X being set
for x being object
for b being bag of X holds support (b +* (x,0)) = (support b) \ {x}

proof end;

theorem Th17: :: POLYNOM9:17

for n being Ordinal
for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for x being Function of n,L
for b being bag of n
for i being object
for j being Nat st i in n holds
(eval ((b +* (i,j)),x)) * ((power L) . ((x /. i),(b . i))) = (eval (b,x)) * ((power L) . ((x /. i),j))

proof end;

definition

let A, B be set ;
let f be Function of A,B;
let x be object ;
let b be Element of B;
:: original: +*
redefine func f +* (x,b) -> Function of A,B;
coherence

proof end;

end;

theorem Th18: :: POLYNOM9:18

for x being object
for n being Ordinal
for L being non trivial well-unital doubleLoopStr
for b being bag of n
for f being Function of n,L
for u being Element of L st b . x = 0 holds
eval (b,(f +* (x,u))) = eval (b,f)

proof end;

theorem Th19: :: POLYNOM9:19

for n being Nat
for b being bag of n
for i being Nat st b . i = degree b holds
b = (EmptyBag n) +* (i,(b . i))

proof end;

theorem Th20: :: POLYNOM9:20

for X being set
for b1, b2 being bag of X st (2 (#) b1) +* (0,(b1 . 0)) = (2 (#) b2) +* (0,(b2 . 0)) holds
b1 = b2

proof end;

theorem Th21: :: POLYNOM9:21

for X being set
for b being bag of X holds support ((2 (#) b) +* (0,(b . 0))) = support b

proof end;

theorem Th22: :: POLYNOM9:22

for i, k being Nat
for X being set
for x being object
for b being bag of X holds b +* (x,(i + k)) = (b +* (x,i)) + ((EmptyBag X) +* (x,k))

proof end;

theorem :: POLYNOM9:23

for X being set
for L being non empty right_complementable add-associative right_zeroed doubleLoopStr
for a being Element of L
for b being bag of X holds Monom ((- a),b) = - (Monom (a,b))

proof end;

theorem :: POLYNOM9:24

for X being set
for L being non empty right_complementable add-associative right_zeroed doubleLoopStr
for a1, a2 being Element of L
for b being bag of X holds (Monom (a1,b)) + (Monom (a2,b)) = Monom ((a1 + a2),b)

proof end;

theorem Th25: :: POLYNOM9:25

for X being set
for L being non empty ZeroStr
for b being bag of X holds Monom ((0. L),b) = 0_ (X,L)

proof end;

theorem :: POLYNOM9:26

for O being Ordinal
for R being non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr
for p being Polynomial of O,R
for b being bag of O holds Support (p - (Monom ((p . b),b))) = (Support p) \ {b}

proof end;

theorem Th27: :: POLYNOM9:27

for n being Nat
for p being object st p in n holds
for i being integer Element of F_Real
for x being Function of n,F_Real holds eval ((Monom (i,((EmptyBag n) +* (p,1)))),x) = i * (x /. p)

proof end;

registration

let X be set ;
let b be bag of X;
let i be integer Element of F_Real;

cluster Monom (i,b) -> INT -valued ;

proof end;

end;

definition

let n be Ordinal;
let R be non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr ;
let p be Polynomial of n,R;
let k be Nat;

func p `^ k -> Polynomial of n,R equals :: POLYNOM9:def 1
(power (Polynom-Ring (n,R))) . (p,k);

proof end;

end;

:: deftheorem defines `^ POLYNOM9:def 1 :

theorem Th28: :: POLYNOM9:28

for O being Ordinal
for R being non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr
for p being Polynomial of O,R st R is well-unital holds
( p `^ 0 = 1_ (O,R) & p `^ 1 = p )

proof end;

theorem Th29: :: POLYNOM9:29

for n being Nat
for O being Ordinal
for R being non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr
for p being Polynomial of O,R holds p `^ (n + 1) = (p `^ n) *' p

proof end;

theorem Th30: :: POLYNOM9:30

for k being Nat
for O being Ordinal
for R being non trivial right_complementable associative commutative Abelian add-associative right_zeroed right_unital well-unital distributive doubleLoopStr
for p being Polynomial of O,R
for f being Function of O,R holds eval ((p `^ k),f) = (power R) . ((eval (p,f)),k)

proof end;

registration

let O be Ordinal;
let p be INT -valued Polynomial of O,F_Real;
let n be Nat;

cluster p `^ n -> INT -valued ;

proof end;

end;

definition

let X be set ;
let b, s be bag of X;
let x be object ;

func Subst (b,x,s) -> bag of X equals :: POLYNOM9:def 2
(b +* (x,0)) + s;

coherence ;

end;

:: deftheorem defines Subst POLYNOM9:def 2 :

theorem :: POLYNOM9:31

for X being set
for b, s being bag of X
for x being object holds support (Subst (b,x,s)) = ((support b) \ {x}) \/ (support s)

proof end;

theorem Th32: :: POLYNOM9:32

for X being set
for x being object
for s1, s2, b being bag of X st Subst (b,x,s1) = Subst (b,x,s2) holds
s1 = s2

proof end;

definition

let X be Ordinal;
let L be non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr ;
let t be bag of X;
let p be Polynomial of X,L;
let x be object ;

func Subst (t,x,p) -> Series of X,L means :Def3: :: POLYNOM9:def 3
for b being bag of X holds
( ( ex s being bag of X st b = Subst (t,x,s) implies for s being bag of X st b = Subst (t,x,s) holds
it . b = (p `^ (t . x)) . s ) & ( ( for s being bag of X holds b <> Subst (t,x,s) ) implies it . b = 0. L ) );

proof end;

proof end;

end;

:: deftheorem Def3 defines Subst POLYNOM9:def 3 :

theorem Th33: :: POLYNOM9:33

proof end;

theorem Th34: :: POLYNOM9:34

for x being object
for O being Ordinal
for R being non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr
for p being Polynomial of O,R
for t being bag of O
for ordP being one-to-one FinSequence of Bags O st rng ordP = Support (p `^ (t . x)) holds
ex ordS being one-to-one FinSequence of Bags O st
( rng ordS = Support (Subst (t,x,p)) & len ordS = len ordP & ( for j being Nat st 1 <= j & j <= len ordS holds
ordS . j = Subst (t,x,(ordP /. j)) ) )

proof end;

registration

let O be Ordinal;
let R be non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr ;
let t be bag of O;
let p be Polynomial of O,R;
let x be object ;

cluster Subst (t,x,p) -> finite-Support ;

proof end;

end;

theorem Th35: :: POLYNOM9:35

for O being Ordinal
for R being non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for t being bag of O
for p being Polynomial of O,R
for i being object
for x being Function of O,R st i in O holds
eval ((Subst (t,i,p)),x) = eval (t,(x +* (i,(eval (p,x)))))

proof end;

registration

let X be set ;
let L be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let p be finite-Support Series of X,L;
let a be Element of L;

cluster a * p -> finite-Support ;

proof end;

end;

definition

let X be Ordinal;
let L be non trivial right_complementable add-associative right_zeroed right_unital well-unital distributive doubleLoopStr ;
let p, s be Polynomial of X,L;
let x be object ;

func Subst (p,x,s) -> Polynomial of X,L means :Def4: :: POLYNOM9:def 4
ex S being FinSequence of (Polynom-Ring (X,L)) st
( it = Sum S & len (SgmX ((BagOrder X),(Support p))) = len S & ( for i being Nat st i in dom S holds
S . i = (p . ((SgmX ((BagOrder X),(Support p))) /. i)) * (Subst (((SgmX ((BagOrder X),(Support p))) /. i),x,s)) ) );

proof end;

proof end;

end;

:: deftheorem Def4 defines Subst POLYNOM9:def 4 :

registration

let O be Ordinal;
let t be bag of O;
let p be INT -valued Polynomial of O,F_Real;
let x be object ;

cluster Subst (t,x,p) -> INT -valued ;

proof end;

end;

registration

let O be Ordinal;
let p, s be INT -valued Polynomial of O,F_Real;
let x be object ;

cluster Subst (p,x,s) -> INT -valued ;

proof end;

end;

theorem Th36: :: POLYNOM9:36

for O being Ordinal
for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of O,L
for x being Function of O,L
for P being FinSequence of (Polynom-Ring (O,L)) st p = Sum P holds
for E being FinSequence of L st len E = len P & ( for s being Polynomial of O,L
for i being Nat st i in dom E & s = P . i holds
E . i = eval (s,x) ) holds
eval (p,x) = Sum E

proof end;

theorem Th37: :: POLYNOM9:37

for O being Ordinal
for R being non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p, s being Polynomial of O,R
for i being object
for x being Function of O,R st i in O holds
eval ((Subst (p,i,s)),x) = eval (p,(x +* (i,(eval (s,x)))))

proof end;

definition

let X be set ;
let S be ZeroStr ;
let p be Series of X,S;

func vars p -> Subset of X means :Def5: :: POLYNOM9:def 5
for x being object holds
( x in it iff ex b being bag of X st
( b in Support p & b . x <> 0 ) );

proof end;

proof end;

end;

:: deftheorem Def5 defines vars POLYNOM9:def 5 :

theorem Th38: :: POLYNOM9:38

for X being Ordinal
for S being non empty ZeroStr
for p being Series of X,S holds
( vars p = {} iff p is Constant )

proof end;

theorem Th39: :: POLYNOM9:39

for X being set
for S being ZeroStr
for p being Series of X,S holds vars p = union { (support b) where b is Element of Bags X : b in Support p }

proof end;

theorem Th40: :: POLYNOM9:40

for X being set
for S being ZeroStr
for p being Series of X,S
for b being bag of X st b in Support p holds
support b c= vars p

proof end;

registration

let X be Ordinal;
let S be non empty ZeroStr ;
let p be Polynomial of X,S;

cluster vars p -> finite ;

proof end;

end;

theorem Th41: :: POLYNOM9:41

for X being set
for S being non empty right_zeroed addLoopStr
for p, q being Series of X,S holds vars (p + q) c= (vars p) \/ (vars q)

proof end;

theorem Th42: :: POLYNOM9:42

for X being set
for S being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of X,S holds vars p = vars (- p)

proof end;

theorem Th43: :: POLYNOM9:43

for X being Ordinal
for S being non empty right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr
for p, q being Polynomial of X,S holds vars (p *' q) c= (vars p) \/ (vars q)

proof end;

theorem Th44: :: POLYNOM9:44

for X being set
for S being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for p being Series of X,S
for a being Element of S holds vars (a * p) c= vars p

proof end;

theorem Th45: :: POLYNOM9:45

for X being Ordinal
for S being non trivial right_complementable add-associative right_zeroed right_unital well-unital distributive doubleLoopStr
for p being Polynomial of X,S
for k being Nat holds vars (p `^ k) c= vars p

proof end;

theorem Th46: :: POLYNOM9:46

for x being object
for X being Ordinal
for S being non trivial right_complementable add-associative right_zeroed right_unital well-unital distributive doubleLoopStr
for p being Polynomial of X,S
for t being bag of X holds vars (Subst (t,x,p)) c= ((support t) \ {x}) \/ (vars p)

proof end;

theorem Th47: :: POLYNOM9:47

for x being object
for X being Ordinal
for S being non trivial right_complementable add-associative right_zeroed right_unital well-unital distributive doubleLoopStr
for p, s being Polynomial of X,S holds vars (Subst (p,x,s)) c= ((vars p) \ {x}) \/ (vars s)

proof end;

theorem Th48: :: POLYNOM9:48

for n being Nat
for x being object
for X being set
for S being non empty ZeroStr
for s being Element of S holds vars (Monom (s,((EmptyBag X) +* (x,n)))) c= {x}

proof end;

definition

let n be Nat;
let L be non empty ZeroStr ;
let p be Series of (n + 1),L;

func p removed_last -> Series of n,L means :Def6: :: POLYNOM9:def 6
for b being bag of n holds it . b = p . (b bag_extend 0);

proof end;

proof end;

end;

:: deftheorem Def6 defines removed_last POLYNOM9:def 6 :

registration

let n be Nat;
let L be non empty ZeroStr ;
let p be Polynomial of (n + 1),L;

cluster p removed_last -> finite-Support ;

proof end;

end;

theorem :: POLYNOM9:49

for n being Nat
for L being non empty ZeroStr
for p being Series of n,L holds (p extended_by_0) removed_last = p

proof end;

theorem Th50: :: POLYNOM9:50

for n being Nat
for L being non empty ZeroStr
for p being Series of (n + 1),L st not n in vars p holds
(p removed_last) extended_by_0 = p

proof end;

theorem Th51: :: POLYNOM9:51

for n being Nat
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of (n + 1),L
for x being Function of n,L
for y being Function of (n + 1),L st not n in vars p & y | n = x holds
eval ((p removed_last),x) = eval (p,y)

proof end;

theorem Th52: :: POLYNOM9:52

for n being Nat
for L being non empty ZeroStr
for p being Series of (n + 1),L holds vars (p removed_last) c= (vars p) \ {n}

proof end;

theorem Th53: :: POLYNOM9:53

for X being Ordinal
for S being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of X,S
for i being object
for x being Function of X,S st i in X \ (vars p) holds
for s being Element of S holds eval (p,x) = eval (p,(x +* (i,s)))

proof end;

definition

let n be Ordinal;
let x be object ;
let A be finite Subset of n;
let f be real-valued Function;

func _sqrtSegm (f,x,A) -> FinSequence of F_Complex means :: POLYNOM9:def 7
( len it = 1 + (card A) & it . 1 = f . x & ( for i being Nat st i in dom (SgmX ((RelIncl n),A)) holds
( (it . (i + 1)) ^2 = f . ((SgmX ((RelIncl n),A)) . i) & Re (it . (i + 1)) >= 0 & Im (it . (i + 1)) >= 0 ) ) );

proof end;

proof end;

end;

:: deftheorem defines _sqrtSegm POLYNOM9:def 7 :

definition

let n be Nat;
let f be finite Function;

func count_reps (f,n) -> bag of n means :Def8: :: POLYNOM9:def 8
for i being Nat st i in n holds
it . i = card (f " {(i + 1)});

proof end;

proof end;

end;

:: deftheorem Def8 defines count_reps POLYNOM9:def 8 :

theorem Th54: :: POLYNOM9:54

for n being Nat holds count_reps ({},n) = EmptyBag n

proof end;

theorem Th55: :: POLYNOM9:55

for i, n being Nat
for f being FinSequence holds count_reps ((f ^ <*(i + 1)*>),n) = (count_reps (f,n)) + ((EmptyBag n) +* (i,1))

proof end;

definition

let f be finite Function;
let L be doubleLoopStr ;
let E be Function;

func SgnMembershipNumber (f,L,E) -> Element of L means :Def9: :: POLYNOM9:def 9
for c being Nat st c = card { x where x is Element of dom f : ( x in dom f & f . x in E . x ) } holds
( ( c is even implies it = 1. L ) & ( c is odd implies it = - (1. L) ) );

proof end;

proof end;

end;

:: deftheorem Def9 defines SgnMembershipNumber POLYNOM9:def 9 :

theorem Th56: :: POLYNOM9:56

for L being doubleLoopStr
for E being Function holds SgnMembershipNumber ({},L,E) = 1. L

proof end;

theorem Th57: :: POLYNOM9:57

for L being doubleLoopStr
for f, e being FinSequence
for x being object
for E being set st len f = len e & not x in E holds
SgnMembershipNumber ((f ^ <*x*>),L,(e ^ <*E*>)) = SgnMembershipNumber (f,L,e)

proof end;

theorem Th58: :: POLYNOM9:58

for L being non empty right_complementable add-associative right_zeroed doubleLoopStr
for f, e being FinSequence
for x being object
for E being set st len f = len e & x in E holds
SgnMembershipNumber ((f ^ <*x*>),L,(e ^ <*E*>)) = - (SgnMembershipNumber (f,L,e))

proof end;

theorem Th59: :: POLYNOM9:59

for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for n being Nat
for f being FinSequence of L
for xf being Function of n,L st xf = FS2XFS f holds
for F being finite set
for E being Enumeration of F
for d being FinSequence st d in doms ((SignGenOp (f, the addF of L,F)) * E) holds
the multF of L "**" ((App ((SignGenOp (f, the addF of L,F)) * E)) . d) = eval ((Monom ((SgnMembershipNumber (d,L,E)),(count_reps (d,n)))),xf)

proof end;

theorem Th60: :: POLYNOM9:60

for n being Nat
for x being object
for f being finite Function st f is with_evenly_repeated_values holds
(count_reps (f,n)) . x is even

proof end;

theorem Th61: :: POLYNOM9:61

for n being Nat
for f being FinSequence of Seg n holds degree (count_reps (f,n)) = len f

proof end;

theorem Th62: :: POLYNOM9:62

for L being doubleLoopStr
for f being finite Function
for E being Function holds
( SgnMembershipNumber (f,L,E) = 1. L or SgnMembershipNumber (f,L,E) = - (1. L) )

proof end;

theorem Th63: :: POLYNOM9:63

for n being Nat
for f being FinSequence of Seg n
for i being Nat st i in n & count_reps (f,n) = (EmptyBag n) +* (i,(len f)) holds
f = (len f) |-> (i + 1)

proof end;

theorem Th64: :: POLYNOM9:64

for i, n, m being Nat st i in n holds
count_reps ((m |-> (i + 1)),n) = (EmptyBag n) +* (i,m)

proof end;

definition

let L be non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ;
let m be Nat;
assume A1: m > 1 ;

mode Jpolynom of m,L -> Polynomial of m,L means :Def10: :: POLYNOM9:def 10
( it . ((EmptyBag m) +* (0,(2 |^ (m -' 1)))) = 1. L & ( for b being bag of m st b in Support it holds
( degree b = 2 |^ (m -' 1) & ex i being Integer st it . b = i '*' (1_ L) & ( not 2 |^ (m -' 1) in rng b or it . b = 1. L or it . b = - (1. L) ) & ( for n being Nat holds b . n is even ) ) ) & ( for f being FinSequence of L
for xf being Function of m,L st xf = FS2XFS f holds
eval (it,xf) = SignGenOp (f, the multF of L, the addF of L,((Seg m) \ {1})) ) );

proof end;

end;

:: deftheorem Def10 defines Jpolynom POLYNOM9:def 10 :

definition

let f be real-valued FinSequence;

func _sqrt f -> FinSequence of F_Complex means :Def11: :: POLYNOM9:def 11
( len it = len f & it . 1 = f . 1 & ( for i being Nat st i in dom f & i <> 1 holds
( (it . i) ^2 = f . i & Re (it . i) >= 0 & Im (it . i) >= 0 ) ) );

proof end;

proof end;

end;

:: deftheorem Def11 defines _sqrt POLYNOM9:def 11 :

definition

let L be non empty 1-sorted ;
let m be set ;
let P be Series of m,L;

func JsqrtSeries P -> Series of m,L means :Def12: :: POLYNOM9:def 12
for b being bag of m holds it . b = P . ((2 (#) b) +* (0,(b . 0)));

proof end;

proof end;

end;

:: deftheorem Def12 defines JsqrtSeries POLYNOM9:def 12 :

registration

let L be non empty ZeroStr ;
let m be Ordinal;
let P be Polynomial of m,L;

cluster JsqrtSeries P -> finite-Support ;

proof end;

end;

theorem Th65: :: POLYNOM9:65

for L being non empty ZeroStr
for m being Nat
for p being Polynomial of m,L st ( for b being bag of m
for n being Nat st b in Support p holds
b . n is even ) holds
for CS being one-to-one FinSequence of Bags m st rng CS = Support (JsqrtSeries p) holds
ex S being one-to-one FinSequence of Bags m st
( len S = len CS & rng S = Support p & ( for i being Nat st i in dom S holds
S . i = (2 (#) (CS /. i)) +* (0,((CS /. i) . 0)) ) )

proof end;

theorem Th66: :: POLYNOM9:66

for m being non trivial Nat
for p being Jpolynom of m, F_Complex
for f being FinSequence of REAL
for xf, cxf being Function of m,F_Complex st xf = FS2XFS f & cxf = FS2XFS (_sqrt f) holds
eval (p,cxf) = eval ((JsqrtSeries p),xf)

proof end;

theorem Th67: :: POLYNOM9:67

for fc being FinSequence of F_Complex
for fr being FinSequence of F_Real st fc = fr holds
Product fc = Product fr

proof end;

theorem Th68: :: POLYNOM9:68

for m being Ordinal
for b being bag of m
for xc being Function of m,F_Complex
for xr being Function of m,F_Real st xc = xr holds
eval (b,xc) = eval (b,xr)

proof end;

theorem Th69: :: POLYNOM9:69

for m being Ordinal
for Pc being Polynomial of m,F_Complex
for Pr being Polynomial of m,F_Real st Pc = Pr holds
for xc being Function of m,F_Complex
for xr being Function of m,F_Real st xc = xr holds
eval (Pc,xc) = eval (Pr,xr)

proof end;

definition

let m be Nat;
assume A1: m > 1 ;
let M be Jpolynom of m, F_Complex ;

func Jsqrt M -> INT -valued Polynomial of m,F_Real equals :Def13: :: POLYNOM9:def 13
JsqrtSeries M;

proof end;

end;

:: deftheorem Def13 defines Jsqrt POLYNOM9:def 13 :

theorem Th70: :: POLYNOM9:70

for m being 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 )

proof end;

registration

let x, y, z, t be object ;

cluster <%x,y,z,t%> -> 4 -element ;

proof end;

end;

registration

let x be Real;

cluster <%x%> -> REAL -valued ;

proof end;

end;

registration

let x, y, z, t be Real;

cluster <%x,y,z,t%> -> REAL -valued ;

proof end;

end;

theorem Th71: :: POLYNOM9:71

for i being Nat
for f being real-valued FinSequence st i > 1 & f . i >= 0 holds
(_sqrt f) . i = sqrt (f . i)

proof end;

theorem Th72: :: POLYNOM9:72

for x being object
for f being FinSequence of F_Complex
for A being set ex i being Integer st
( ( i = 1 or i = - 1 ) & (SignGen (f, the addF of F_Complex,A)) . x = i * (f . x) )

proof end;

Lm1: for x, y, z, t being Complex holds XFS2FS <%x,y,z,t%> = <*x,y,z,t*>

proof end;

theorem Th73: :: POLYNOM9:73

for M being Jpolynom of 4, F_Complex
for x1, x2, x3 being Nat st x1 is odd & x2 is odd holds
for z being Integer st eval ((Jsqrt M),(@ <%z,x1,(4 * x2),(16 * x3)%>)) = 0 holds
( x1 is square & x2 is square & x3 is square & - z <= ((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3)) )

proof end;

theorem Th74: :: POLYNOM9:74

for M being Jpolynom of 4, F_Complex
for x1, x2, x3 being Nat st x1 is square & x2 is square & x3 is square holds
ex z being Integer st
( - z = ((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3)) & eval ((Jsqrt M),(@ <%z,x1,(4 * x2),(16 * x3)%>)) = 0 )

proof end;

theorem Th75: :: POLYNOM9:75

for n, m being Nat
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of n,L ex q being Polynomial of (n + m),L st
( rng q c= (rng p) \/ {(0. L)} & ( for b being bag of n + m holds
( b in Support q iff ( b | n in Support p & ( for i being Nat st i >= n holds
b . i = 0 ) ) ) ) & ( for b being bag of n + m st b in Support q holds
q . b = p . (b | n) ) & ( for x being Function of n,L
for y being Function of (n + m),L st y | n = x holds
eval (p,x) = eval (q,y) ) )

proof end;

theorem Th76: :: POLYNOM9:76

for M being Jpolynom of 4, F_Complex ex K2 being INT -valued Polynomial of 6,F_Real st
( ( for f being Function of 6,F_Real st f . 5 <> 0 holds
eval (K2,f) = ((power F_Real) . ((f /. 5),8)) * (eval ((Jsqrt M),(@ <%((- (f . 0)) + ((f . 4) / (f . 5))),(f . 1),(f . 2),(f . 3)%>))) ) & ( for f being INT -valued Function of 6,F_Real st f . 5 <> 0 & eval (K2,f) = 0 holds
f . 5 divides f . 4 ) )

proof end;

registration

let x be Integer;

cluster <%x%> -> INT -valued ;

proof end;

end;

registration

let x, y, z, t be Integer;

cluster <%x,y,z,t%> -> INT -valued ;