P. 307 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30601-30700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sgnclre 30601	Closure of the signum. (Contributed by Thierry Arnoux, 28-Sep-2018.)
|- ( A e. RR -> (sgn ` A ) e. RR )
Theorem	sgnneg 30602	Negation of the signum. (Contributed by Thierry Arnoux, 1-Oct-2018.)
|- ( A e. RR -> (sgn ` -u A ) = -u (sgn ` A ) )
Theorem	sgn3da 30603	A conditional containing a signum is true if it is true in all three possible cases. (Contributed by Thierry Arnoux, 1-Oct-2018.)
|- ( ph -> A e. RR* )   &    |- ( (sgn ` A ) = 0 -> ( ps <-> ch ) )   &    |- ( (sgn ` A ) = 1 -> ( ps <-> th ) )   &    |- ( (sgn ` A ) = -u 1 -> ( ps <-> ta ) )   &    |- ( ( ph /\ A = 0 ) -> ch )   &    |- ( ( ph /\ 0 < A ) -> th )   &    |- ( ( ph /\ A < 0 ) -> ta )   =>    |- ( ph -> ps )
Theorem	sgnmul 30604	Signum of a product. (Contributed by Thierry Arnoux, 2-Oct-2018.)
|- ( ( A e. RR /\ B e. RR ) -> (sgn ` ( A x. B ) ) = ( (sgn ` A ) x. (sgn ` B ) ) )
Theorem	sgnmulrp2 30605	Multiplication by a positive number does not affect signum. (Contributed by Thierry Arnoux, 2-Oct-2018.)
|- ( ( A e. RR /\ B e. RR+ ) -> (sgn ` ( A x. B ) ) = (sgn ` A ) )
Theorem	sgnsub 30606	Subtraction of a number of opposite sign. (Contributed by Thierry Arnoux, 2-Oct-2018.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) -> (sgn ` ( A - B ) ) = (sgn ` A ) )
Theorem	sgnnbi 30607	Negative signum. (Contributed by Thierry Arnoux, 2-Oct-2018.)
|- ( A e. RR* -> ( (sgn ` A ) = -u 1 <-> A < 0 ) )
Theorem	sgnpbi 30608	Positive signum. (Contributed by Thierry Arnoux, 2-Oct-2018.)
|- ( A e. RR* -> ( (sgn ` A ) = 1 <-> 0 < A ) )
Theorem	sgn0bi 30609	Zero signum. (Contributed by Thierry Arnoux, 10-Oct-2018.)
|- ( A e. RR* -> ( (sgn ` A ) = 0 <-> A = 0 ) )
Theorem	sgnsgn 30610	Signum is idempotent. (Contributed by Thierry Arnoux, 2-Oct-2018.)
|- ( A e. RR* -> (sgn ` (sgn ` A ) ) = (sgn ` A ) )
Theorem	sgnmulsgn 30611	If two real numbers are of different signs, so are their signs. (Contributed by Thierry Arnoux, 12-Oct-2018.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( A x. B ) < 0 <-> ( (sgn ` A ) x. (sgn ` B ) ) < 0 ) )
Theorem	sgnmulsgp 30612	If two real numbers are of different signs, so are their signs. (Contributed by Thierry Arnoux, 12-Oct-2018.)
|- ( ( A e. RR /\ B e. RR ) -> ( 0 < ( A x. B ) <-> 0 < ( (sgn ` A ) x. (sgn ` B ) ) ) )
Theorem	fzssfzo 30613	Condition for an integer interval to be a subset of an half-open integer interval. (Contributed by Thierry Arnoux, 8-Oct-2018.)
|- ( K e. ( M..^ N ) -> ( M ... K ) C_ ( M..^ N ) )
Theorem	gsumncl 30614*	Closure of a group sum in a non-commutative monoid. (Contributed by Thierry Arnoux, 8-Oct-2018.)
|- K = ( Base ` M )   &    |- ( ph -> M e. Mnd )   &    |- ( ph -> P e. ( ZZ>= ` N ) )   &    |- ( ( ph /\ k e. ( N ... P ) ) -> B e. K )   =>    |- ( ph -> ( M gsumg ( k e. ( N ... P ) |-> B ) ) e. K )
Theorem	gsumnunsn 30615*	Closure of a group sum in a non-commutative monoid. (Contributed by Thierry Arnoux, 8-Oct-2018.)
|- K = ( Base ` M )   &    |- ( ph -> M e. Mnd )   &    |- ( ph -> P e. ( ZZ>= ` N ) )   &    |- ( ( ph /\ k e. ( N ... P ) ) -> B e. K )   &    |- .+ = ( +g ` M )   &    |- ( ph -> C e. K )   &    |- ( ( ph /\ k = ( P + 1 ) ) -> B = C )   =>    |- ( ph -> ( M gsumg ( k e. ( N ... ( P + 1 ) ) |-> B ) ) = ( ( M gsumg ( k e. ( N ... P ) |-> B ) ) .+ C ) )
20.3.23  Words over a set - misc additions
Theorem	wrdfd 30616	A word is a zero-based sequence with a recoverable upper limit, deduction version. (Contributed by Thierry Arnoux, 22-Dec-2021.)
|- ( ph -> N = ( # ` W ) )   &    |- ( ph -> W e. Word S )   =>    |- ( ph -> W : ( 0..^ N ) --> S )
Theorem	wrdres 30617	Condition for the restriction of a word to be a word itself. (Contributed by Thierry Arnoux, 5-Oct-2018.)
|- ( ( W e. Word S /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W |` ( 0..^ N ) ) e. Word S )
Theorem	wrdsplex 30618*	Existence of a split of a word at a given index. (Contributed by Thierry Arnoux, 11-Oct-2018.)
|- ( ( W e. Word S /\ N e. ( 0 ... ( # ` W ) ) ) -> E. v e. Word S W = ( ( W |` ( 0..^ N ) ) ++ v ) )
20.3.23.1  Operations on words
Theorem	ccatmulgnn0dir 30619	Concatenation of words follow the rule mulgnn0dir 17571 (although applying mulgnn0dir 17571 would require S to be a set). In this case A is <" K "> to the power M in the free monoid. (Contributed by Thierry Arnoux, 5-Oct-2018.)
|- A = ( ( 0..^ M ) X. { K } )   &    |- B = ( ( 0..^ N ) X. { K } )   &    |- C = ( ( 0..^ ( M + N ) ) X. { K } )   &    |- ( ph -> K e. S )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( A ++ B ) = C )
Theorem	ofcccat 30620	Letterwise operations on word concatenations. (Contributed by Thierry Arnoux, 5-Oct-2018.)
|- ( ph -> F e. Word S )   &    |- ( ph -> G e. Word S )   &    |- ( ph -> K e. T )   =>    |- ( ph -> ( ( F ++ G )∘𝑓/𝑐 R K ) = ( ( F∘𝑓/𝑐 R K ) ++ ( G∘𝑓/𝑐 R K ) ) )
Theorem	ofcs1 30621	Letterwise operations on a single letter word. (Contributed by Thierry Arnoux, 7-Oct-2018.)
|- ( ( A e. S /\ B e. T ) -> ( <" A ">∘𝑓/𝑐 R B ) = <" ( A R B ) "> )
Theorem	ofcs2 30622	Letterwise operations on a double letter word. (Contributed by Thierry Arnoux, 9-Oct-2018.)
|- ( ( A e. S /\ B e. S /\ C e. T ) -> ( <" A B ">∘𝑓/𝑐 R C ) = <" ( A R C ) ( B R C ) "> )
20.3.24  Polynomials with real coefficients - misc additions
Theorem	plymul02 30623	Product of a polynomial with the zero polynomial. (Contributed by Thierry Arnoux, 26-Sep-2018.)
|- ( F e. (Poly ` S ) -> ( 0p oF x. F ) = 0p )
Theorem	plymulx0 30624*	Coefficients of a polynomial multiplyed by Xp. (Contributed by Thierry Arnoux, 25-Sep-2018.)
|- ( F e. ( (Poly ` RR ) \ { 0p } ) -> (coeff ` ( F oF x. Xp ) ) = ( n e. NN0 |-> if ( n = 0 , 0 , ( (coeff ` F ) ` ( n - 1 ) ) ) ) )
Theorem	plymulx 30625*	Coefficients of a polynomial multiplyed by Xp. (Contributed by Thierry Arnoux, 25-Sep-2018.)
|- ( F e. (Poly ` RR ) -> (coeff ` ( F oF x. Xp ) ) = ( n e. NN0 |-> if ( n = 0 , 0 , ( (coeff ` F ) ` ( n - 1 ) ) ) ) )
Theorem	plyrecld 30626	Closure of a polynomial with real coefficients. (Contributed by Thierry Arnoux, 18-Sep-2018.)
|- ( ph -> F e. (Poly ` RR ) )   &    |- ( ph -> X e. RR )   =>    |- ( ph -> ( F ` X ) e. RR )
Theorem	signsplypnf 30627*	The quotient of a polynomial F by a monic monomial of same degree G converges to the highest coefficient of F. (Contributed by Thierry Arnoux, 18-Sep-2018.)
|- D = (deg ` F )   &    |- C = (coeff ` F )   &    |- B = ( C ` D )   &    |- G = ( x e. RR+ |-> ( x ^ D ) )   =>    |- ( F e. (Poly ` RR ) -> ( F oF / G ) ~~> r B )
Theorem	signsply0 30628*	Lemma for the rule of signs, based on Bolzano's intermediate value theorem for polynomials : If the lowest and highest coefficient A and B are of opposite signs, the polynomial admits a positive root. (Contributed by Thierry Arnoux, 19-Sep-2018.)
|- D = (deg ` F )   &    |- C = (coeff ` F )   &    |- B = ( C ` D )   &    |- A = ( C ` 0 )   &    |- ( ph -> F e. (Poly ` RR ) )   &    |- ( ph -> F =/= 0p )   &    |- ( ph -> ( A x. B ) < 0 )   =>    |- ( ph -> E. z e. RR+ ( F ` z ) = 0 )
20.3.25  Descartes's rule of signs
20.3.25.1  Sign changes in a word over real numbers
Theorem	signspval 30629*	The value of the skipping 0 sign operation. (Contributed by Thierry Arnoux, 9-Sep-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   =>    |- ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) -> ( X .+^ Y ) = if ( Y = 0 , X , Y ) )
Theorem	signsw0glem 30630*	Neutral element property of .+^. (Contributed by Thierry Arnoux, 9-Sep-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   =>    |- A. u e. { -u 1 , 0 , 1 } ( ( 0 .+^ u ) = u /\ ( u .+^ 0 ) = u )
Theorem	signswbase 30631	The base of W is the triplet reprensenting the possible signs. (Contributed by Thierry Arnoux, 9-Sep-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   =>    |- { -u 1 , 0 , 1 } = ( Base ` W )
Theorem	signswplusg 30632*	The operation of W. (Contributed by Thierry Arnoux, 9-Sep-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   =>    |- .+^ = ( +g ` W )
Theorem	signsw0g 30633*	The neutral element of W. (Contributed by Thierry Arnoux, 9-Sep-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   =>    |- 0 = ( 0g ` W )
Theorem	signswmnd 30634*	W is a monoid structure on { -u 1 , 0 , 1 } which operation retains the right side, but skips zeroes. This will be used for skipping zeroes when counting sign changes. (Contributed by Thierry Arnoux, 9-Sep-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   =>    |- W e. Mnd
Theorem	signswrid 30635*	The zero-skipping operation propagages nonzeros. (Contributed by Thierry Arnoux, 11-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   =>    |- ( X e. { -u 1 , 0 , 1 } -> ( X .+^ 0 ) = X )
Theorem	signswlid 30636*	The zero-skipping operation keeps nonzeros. (Contributed by Thierry Arnoux, 12-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   =>    |- ( ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ Y =/= 0 ) -> ( X .+^ Y ) = Y )
Theorem	signswn0 30637*	The zero-skipping operation propagages nonzeros. (Contributed by Thierry Arnoux, 11-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   =>    |- ( ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ X =/= 0 ) -> ( X .+^ Y ) =/= 0 )
Theorem	signswch 30638*	The zero-skipping operation changes value when the operands change signs. (Contributed by Thierry Arnoux, 9-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   =>    |- ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) -> ( ( X .+^ Y ) =/= X <-> ( X x. Y ) < 0 ) )
20.3.25.2  Counting sign changes in a word over real numbers
Theorem	signslema 30639	Computational part of signwlemn . (Contributed by Thierry Arnoux, 29-Sep-2018.)
|- ( ph -> E e. NN0 )   &    |- ( ph -> F e. NN0 )   &    |- ( ph -> G e. NN0 )   &    |- ( ph -> H e. NN0 )   &    |- ( ph -> ( E < G /\ -. 2 || ( G - E ) ) )   &    |- ( ph -> ( ( H - G ) - ( F - E ) ) e. { 0 , 2 } )   =>    |- ( ph -> ( F < H /\ -. 2 || ( H - F ) ) )
Theorem	signstfv 30640*	Value of the zero-skipping sign word. (Contributed by Thierry Arnoux, 8-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   =>    |- ( F e. Word RR -> ( T ` F ) = ( n e. ( 0..^ ( # ` F ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( F ` i ) ) ) ) ) )
Theorem	signstfval 30641*	Value of the zero-skipping sign word. (Contributed by Thierry Arnoux, 8-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   =>    |- ( ( F e. Word RR /\ N e. ( 0..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) = ( W gsumg ( i e. ( 0 ... N ) |-> (sgn ` ( F ` i ) ) ) ) )
Theorem	signstcl 30642*	Closure of the zero skipping sign word. (Contributed by Thierry Arnoux, 9-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   =>    |- ( ( F e. Word RR /\ N e. ( 0..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) e. { -u 1 , 0 , 1 } )
Theorem	signstf 30643*	The zero skipping sign word is a word. (Contributed by Thierry Arnoux, 8-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   =>    |- ( F e. Word RR -> ( T ` F ) e. Word RR )
Theorem	signstlen 30644*	Length of the zero skipping sign word. (Contributed by Thierry Arnoux, 8-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   =>    |- ( F e. Word RR -> ( # ` ( T ` F ) ) = ( # ` F ) )
Theorem	signstf0 30645*	Sign of a single letter word. (Contributed by Thierry Arnoux, 8-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   =>    |- ( K e. RR -> ( T ` <" K "> ) = <" (sgn ` K ) "> )
Theorem	signstfvn 30646*	Zero-skipping sign in a word compared to a shorter word. (Contributed by Thierry Arnoux, 8-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   =>    |- ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) -> ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) = ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) .+^ (sgn ` K ) ) )
Theorem	signsvtn0 30647*	If the last letter is non zero, then this is the zero-skipping sign. (Contributed by Thierry Arnoux, 8-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   &    |- N = ( # ` F )   =>    |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( ( T ` F ) ` ( N - 1 ) ) = (sgn ` ( F ` ( N - 1 ) ) ) )
Theorem	signstfvp 30648*	Zero-skipping sign in a word compared to a shorter word. (Contributed by Thierry Arnoux, 8-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   =>    |- ( ( F e. Word RR /\ K e. RR /\ N e. ( 0..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ <" K "> ) ) ` N ) = ( ( T ` F ) ` N ) )
Theorem	signstfvneq0 30649*	In case the first letter is not zero, the zero skipping sign is never zero. (Contributed by Thierry Arnoux, 10-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   =>    |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ N e. ( 0..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) =/= 0 )
Theorem	signstfvcl 30650*	Closure of the zero skipping sign in case the first letter is not zero. (Contributed by Thierry Arnoux, 10-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   =>    |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ N e. ( 0..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) e. { -u 1 , 1 } )
Theorem	signstfvc 30651*	Zero-skipping sign in a word compared to a shorter word. (Contributed by Thierry Arnoux, 11-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   =>    |- ( ( F e. Word RR /\ G e. Word RR /\ N e. ( 0..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ G ) ) ` N ) = ( ( T ` F ) ` N ) )
Theorem	signstres 30652*	Restriction of a zero skipping sign to a subword. (Contributed by Thierry Arnoux, 11-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   =>    |- ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> ( ( T ` F ) |` ( 0..^ N ) ) = ( T ` ( F |` ( 0..^ N ) ) ) )
Theorem	signstfveq0a 30653*	Lemma for signstfveq0 30654. (Contributed by Thierry Arnoux, 11-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   &    |- N = ( # ` F )   =>    |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> N e. ( ZZ>= ` 2 ) )
Theorem	signstfveq0 30654*	In case the last letter is zero, the zero skipping sign is the same as the previous letter. (Contributed by Thierry Arnoux, 11-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   &    |- N = ( # ` F )   =>    |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( T ` F ) ` ( N - 1 ) ) = ( ( T ` F ) ` ( N - 2 ) ) )
Theorem	signsvvfval 30655*	The value of V, which represents the number of times the sign changes in a word. (Contributed by Thierry Arnoux, 7-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   =>    |- ( F e. Word RR -> ( V ` F ) = sum_ j e. ( 1..^ ( # ` F ) ) if ( ( ( T ` F ) ` j ) =/= ( ( T ` F ) ` ( j - 1 ) ) , 1 , 0 ) )
Theorem	signsvvf 30656*	V is a function. (Contributed by Thierry Arnoux, 8-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   =>    |- V :Word RR --> NN0
Theorem	signsvf0 30657*	There is no change of sign in the empty word. (Contributed by Thierry Arnoux, 8-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   =>    |- ( V ` (/) ) = 0
Theorem	signsvf1 30658*	In a single-letter word, which represents a constant polynomial, there is no change of sign. (Contributed by Thierry Arnoux, 8-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   =>    |- ( K e. RR -> ( V ` <" K "> ) = 0 )
Theorem	signsvfn 30659*	Number of changes in a word compared to a shorter word. (Contributed by Thierry Arnoux, 12-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   =>    |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( V ` ( F ++ <" K "> ) ) = ( ( V ` F ) + if ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. K ) < 0 , 1 , 0 ) ) )
Theorem	signsvtp 30660*	Adding a letter of the same sign as the highest coefficient does not change the sign. (Contributed by Thierry Arnoux, 12-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   &    |- ( ph -> E e. (Word RR \ { (/) } ) )   &    |- ( ph -> ( E ` 0 ) =/= 0 )   &    |- ( ph -> F = ( E ++ <" A "> ) )   &    |- ( ph -> A e. RR )   &    |- N = ( # ` E )   &    |- B = ( ( T ` E ) ` ( N - 1 ) )   =>    |- ( ( ph /\ 0 < ( A x. B ) ) -> ( V ` F ) = ( V ` E ) )
Theorem	signsvtn 30661*	Adding a letter of a different sign as the highest coefficient changes the sign. (Contributed by Thierry Arnoux, 12-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   &    |- ( ph -> E e. (Word RR \ { (/) } ) )   &    |- ( ph -> ( E ` 0 ) =/= 0 )   &    |- ( ph -> F = ( E ++ <" A "> ) )   &    |- ( ph -> A e. RR )   &    |- N = ( # ` E )   &    |- B = ( ( T ` E ) ` ( N - 1 ) )   =>    |- ( ( ph /\ ( A x. B ) < 0 ) -> ( ( V ` F ) - ( V ` E ) ) = 1 )
Theorem	signsvfpn 30662*	Adding a letter of the same sign as the highest coefficient does not change the sign. (Contributed by Thierry Arnoux, 12-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   &    |- ( ph -> E e. (Word RR \ { (/) } ) )   &    |- ( ph -> ( E ` 0 ) =/= 0 )   &    |- ( ph -> F = ( E ++ <" A "> ) )   &    |- ( ph -> A e. RR )   &    |- N = ( # ` E )   &    |- B = ( E ` ( N - 1 ) )   =>    |- ( ( ph /\ 0 < ( B x. A ) ) -> ( V ` F ) = ( V ` E ) )
Theorem	signsvfnn 30663*	Adding a letter of a different sign as the highest coefficient changes the sign. (Contributed by Thierry Arnoux, 12-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   &    |- ( ph -> E e. (Word RR \ { (/) } ) )   &    |- ( ph -> ( E ` 0 ) =/= 0 )   &    |- ( ph -> F = ( E ++ <" A "> ) )   &    |- ( ph -> A e. RR )   &    |- N = ( # ` E )   &    |- B = ( E ` ( N - 1 ) )   =>    |- ( ( ph /\ ( B x. A ) < 0 ) -> ( ( V ` F ) - ( V ` E ) ) = 1 )
Theorem	signlem0 30664*	Adding a zero as the highest coefficient does not change the parity of the sign changes. (Contributed by Thierry Arnoux, 12-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   =>    |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) -> ( V ` ( F ++ <" 0 "> ) ) = ( V ` F ) )
Theorem	signshf 30665*	H, corresponding to the word F multiplied by ( x - C ), as a function. (Contributed by Thierry Arnoux, 29-Sep-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   &    |- H = ( ( <" 0 "> ++ F ) oF - ( ( F ++ <" 0 "> )∘𝑓/𝑐 x. C ) )   =>    |- ( ( F e. Word RR /\ C e. RR+ ) -> H : ( 0..^ ( ( # ` F ) + 1 ) ) --> RR )
Theorem	signshwrd 30666*	H, corresponding to the word F multiplied by ( x - C ), is a word. (Contributed by Thierry Arnoux, 29-Sep-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   &    |- H = ( ( <" 0 "> ++ F ) oF - ( ( F ++ <" 0 "> )∘𝑓/𝑐 x. C ) )   =>    |- ( ( F e. Word RR /\ C e. RR+ ) -> H e. Word RR )
Theorem	signshlen 30667*	Length of H, corresponding to the word F multiplied by ( x - C ). (Contributed by Thierry Arnoux, 14-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   &    |- H = ( ( <" 0 "> ++ F ) oF - ( ( F ++ <" 0 "> )∘𝑓/𝑐 x. C ) )   =>    |- ( ( F e. Word RR /\ C e. RR+ ) -> ( # ` H ) = ( ( # ` F ) + 1 ) )
Theorem	signshnz 30668*	H is not the empty word. (Contributed by Thierry Arnoux, 14-Oct-2018.)
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )   &    |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }   &    |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )   &    |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )   &    |- H = ( ( <" 0 "> ++ F ) oF - ( ( F ++ <" 0 "> )∘𝑓/𝑐 x. C ) )   =>    |- ( ( F e. Word RR /\ C e. RR+ ) -> H =/= (/) )
20.3.26  Number Theory
Theorem	efcld 30669	Closure law for the exponential function, deduction version. (Contributed by Thierry Arnoux, 1-Dec-2021.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( exp ` A ) e. CC )
Theorem	iblidicc 30670*	The identity function is integrable on any closed interval. (Contributed by Thierry Arnoux, 13-Dec-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( x e. ( A [,] B ) |-> x ) e. L^1 )
Theorem	rpsqrtcn 30671	Continuity of the real positive square root function. (Contributed by Thierry Arnoux, 20-Dec-2021.)
|- ( sqr |` RR+ ) e. ( RR+ -cn-> RR+ )
Theorem	divsqrtid 30672	A real number divided by its square root. (Contributed by Thierry Arnoux, 1-Jan-2022.)
|- ( A e. RR+ -> ( A / ( sqr ` A ) ) = ( sqr ` A ) )
Theorem	cxpcncf1 30673*	The power function on complex numbers, for fixed exponent A, is continuous. Similar to cxpcn 24486. (Contributed by Thierry Arnoux, 20-Dec-2021.)
|- ( ph -> A e. CC )   &    |- ( ph -> D C_ ( CC \ ( -oo (,] 0 ) ) )   =>    |- ( ph -> ( x e. D |-> ( x ^c A ) ) e. ( D -cn-> CC ) )
Theorem	efmul2picn 30674*	Multiplying by ( _i x. ( 2 x. pi ) ) and taking the exponential preserves continuity. (Contributed by Thierry Arnoux, 13-Dec-2021.)
|- ( ph -> ( x e. A |-> B ) e. ( A -cn-> CC ) )   =>    |- ( ph -> ( x e. A |-> ( exp ` ( ( _i x. ( 2 x. pi ) ) x. B ) ) ) e. ( A -cn-> CC ) )
Theorem	fct2relem 30675	Lemma for ftc2re 30676. (Contributed by Thierry Arnoux, 20-Dec-2021.)
|- E = ( C (,) D )   &    |- ( ph -> A e. E )   &    |- ( ph -> B e. E )   =>    |- ( ph -> ( A [,] B ) C_ E )
Theorem	ftc2re 30676*	The Fundamental Theorem of Calculus, part two, for functions continuous on D. (Contributed by Thierry Arnoux, 1-Dec-2021.)
|- E = ( C (,) D )   &    |- ( ph -> A e. E )   &    |- ( ph -> B e. E )   &    |- ( ph -> A <_ B )   &    |- ( ph -> F : E --> CC )   &    |- ( ph -> ( RR _D F ) e. ( E -cn-> CC ) )   =>    |- ( ph -> S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t = ( ( F ` B ) - ( F ` A ) ) )
Theorem	fdvposlt 30677*	Functions with a positive derivative, i.e. monotonously growing functions, preserve strict ordering. (Contributed by Thierry Arnoux, 20-Dec-2021.)
|- E = ( C (,) D )   &    |- ( ph -> A e. E )   &    |- ( ph -> B e. E )   &    |- ( ph -> F : E --> RR )   &    |- ( ph -> ( RR _D F ) e. ( E -cn-> RR ) )   &    |- ( ph -> A < B )   &    |- ( ( ph /\ x e. ( A (,) B ) ) -> 0 < ( ( RR _D F ) ` x ) )   =>    |- ( ph -> ( F ` A ) < ( F ` B ) )
Theorem	fdvneggt 30678*	Functions with a negative derivative, i.e. monotonously decreasing functions, inverse strict ordering. (Contributed by Thierry Arnoux, 20-Dec-2021.)
|- E = ( C (,) D )   &    |- ( ph -> A e. E )   &    |- ( ph -> B e. E )   &    |- ( ph -> F : E --> RR )   &    |- ( ph -> ( RR _D F ) e. ( E -cn-> RR ) )   &    |- ( ph -> A < B )   &    |- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) < 0 )   =>    |- ( ph -> ( F ` B ) < ( F ` A ) )
Theorem	fdvposle 30679*	Functions with a nonnegative derivative, i.e. monotonously growing functions, preserve ordering. (Contributed by Thierry Arnoux, 20-Dec-2021.)
|- E = ( C (,) D )   &    |- ( ph -> A e. E )   &    |- ( ph -> B e. E )   &    |- ( ph -> F : E --> RR )   &    |- ( ph -> ( RR _D F ) e. ( E -cn-> RR ) )   &    |- ( ph -> A <_ B )   &    |- ( ( ph /\ x e. ( A (,) B ) ) -> 0 <_ ( ( RR _D F ) ` x ) )   =>    |- ( ph -> ( F ` A ) <_ ( F ` B ) )
Theorem	fdvnegge 30680*	Functions with a non-positive derivative, i.e. decreasing functions, preserve ordering. (Contributed by Thierry Arnoux, 20-Dec-2021.)
|- E = ( C (,) D )   &    |- ( ph -> A e. E )   &    |- ( ph -> B e. E )   &    |- ( ph -> F : E --> RR )   &    |- ( ph -> ( RR _D F ) e. ( E -cn-> RR ) )   &    |- ( ph -> A <_ B )   &    |- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) <_ 0 )   =>    |- ( ph -> ( F ` B ) <_ ( F ` A ) )
Theorem	prodfzo03 30681*	A product of three factors, indexed starting with zero. (Contributed by Thierry Arnoux, 14-Dec-2021.)
|- ( k = 0 -> D = A )   &    |- ( k = 1 -> D = B )   &    |- ( k = 2 -> D = C )   &    |- ( ( ph /\ k e. ( 0..^ 3 ) ) -> D e. CC )   =>    |- ( ph -> prod_ k e. ( 0..^ 3 ) D = ( A x. ( B x. C ) ) )
Theorem	actfunsnf1o 30682*	The action F of extending function from B to C with new values at point I is a bijection. (Contributed by Thierry Arnoux, 9-Dec-2021.)
|- ( ( ph /\ k e. C ) -> A C_ ( C ^m B ) )   &    |- ( ph -> C e. _V )   &    |- ( ph -> I e. V )   &    |- ( ph -> -. I e. B )   &    |- F = ( x e. A |-> ( x u. { <. I , k >. } ) )   =>    |- ( ( ph /\ k e. C ) -> F : A -1-1-onto-> ran F )
Theorem	actfunsnrndisj 30683*	The action F of extending function from B to C with new values at point I yields different functions. (Contributed by Thierry Arnoux, 9-Dec-2021.)
|- ( ( ph /\ k e. C ) -> A C_ ( C ^m B ) )   &    |- ( ph -> C e. _V )   &    |- ( ph -> I e. V )   &    |- ( ph -> -. I e. B )   &    |- F = ( x e. A |-> ( x u. { <. I , k >. } ) )   =>    |- ( ph -> Disj k e. C ran F )
Theorem	itgexpif 30684*	The basis for the circle method in the form of trigonometric sums. Proposition of [Nathanson] p. 123. (Contributed by Thierry Arnoux, 2-Dec-2021.)
|- ( N e. ZZ -> S. ( 0 (,) 1 ) ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( N x. x ) ) ) _d x = if ( N = 0 , 1 , 0 ) )
Theorem	fsum2dsub 30685*	Lemma for breprexp 30711- Re-index a double sum, using difference of the initial indices. (Contributed by Thierry Arnoux, 7-Dec-2021.)
|- ( ph -> M e. NN0 )   &    |- ( ph -> N e. NN0 )   &    |- ( i = ( k - j ) -> A = B )   &    |- ( ( ph /\ i e. ( ZZ>= ` -u j ) /\ j e. ( 1 ... N ) ) -> A e. CC )   &    |- ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( ( ( M + j ) + 1 ) ... ( M + N ) ) ) -> B = 0 )   &    |- ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( 0..^ j ) ) -> B = 0 )   =>    |- ( ph -> sum_ i e. ( 0 ... M ) sum_ j e. ( 1 ... N ) A = sum_ k e. ( 0 ... ( M + N ) ) sum_ j e. ( 1 ... N ) B )
20.3.26.1  Representations of a number as sums of integers
Syntax	crepr 30686	Representations of a number as a sum of nonnegative integers.
class repr
Definition	df-repr 30687*	The representations of a nonnegative m as the sum of s nonnegative integers from a set b. Cf. Definition of [Nathanson] p. 123. (Contributed by Thierry Arnoux, 1-Dec-2021.)
|- repr = ( s e. NN0 |-> ( b e. ~P NN , m e. ZZ |-> { c e. ( b ^m ( 0..^ s ) ) | sum_ a e. ( 0..^ s ) ( c ` a ) = m } ) )
Theorem	reprval 30688*	Value of the representations of M as the sum of S nonnegative integers in a given set A (Contributed by Thierry Arnoux, 1-Dec-2021.)
|- ( ph -> A C_ NN )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> S e. NN0 )   =>    |- ( ph -> ( A (repr ` S ) M ) = { c e. ( A ^m ( 0..^ S ) ) | sum_ a e. ( 0..^ S ) ( c ` a ) = M } )
Theorem	repr0 30689	There is exactly one representation with no elements (an empty sum), only for M = 0. (Contributed by Thierry Arnoux, 2-Dec-2021.)
|- ( ph -> A C_ NN )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> S e. NN0 )   =>    |- ( ph -> ( A (repr ` 0 ) M ) = if ( M = 0 , { (/) } , (/) ) )
Theorem	reprf 30690	Members of the representation of M as the sum of S nonnegative integers from set A as functions. (Contributed by Thierry Arnoux, 5-Dec-2021.)
|- ( ph -> A C_ NN )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> C e. ( A (repr ` S ) M ) )   =>    |- ( ph -> C : ( 0..^ S ) --> A )
Theorem	reprsum 30691*	Sums of values of the members of the representation of M equal M. (Contributed by Thierry Arnoux, 5-Dec-2021.)
|- ( ph -> A C_ NN )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> C e. ( A (repr ` S ) M ) )   =>    |- ( ph -> sum_ a e. ( 0..^ S ) ( C ` a ) = M )
Theorem	reprle 30692	Upper bound to the terms in the representations of M as the sum of S nonnegative integers from set A. (Contributed by Thierry Arnoux, 27-Dec-2021.)
|- ( ph -> A C_ NN )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> C e. ( A (repr ` S ) M ) )   &    |- ( ph -> X e. ( 0..^ S ) )   =>    |- ( ph -> ( C ` X ) <_ M )
Theorem	reprsuc 30693*	Express the representations recursively. (Contributed by Thierry Arnoux, 5-Dec-2021.)
|- ( ph -> A C_ NN )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> S e. NN0 )   &    |- F = ( c e. ( A (repr ` S ) ( M - b ) ) |-> ( c u. { <. S , b >. } ) )   =>    |- ( ph -> ( A (repr ` ( S + 1 ) ) M ) = U_ b e. A ran F )
Theorem	reprfi 30694	Bounded representations are finite sets. (Contributed by Thierry Arnoux, 7-Dec-2021.)
|- ( ph -> A C_ NN )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> A e. Fin )   =>    |- ( ph -> ( A (repr ` S ) M ) e. Fin )
Theorem	reprss 30695	Representations with terms in a subset. (Contributed by Thierry Arnoux, 11-Dec-2021.)
|- ( ph -> A C_ NN )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> B C_ A )   =>    |- ( ph -> ( B (repr ` S ) M ) C_ ( A (repr ` S ) M ) )
Theorem	reprinrn 30696*	Representations with term in an intersection. (Contributed by Thierry Arnoux, 11-Dec-2021.)
|- ( ph -> A C_ NN )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> S e. NN0 )   =>    |- ( ph -> ( c e. ( ( A i^i B ) (repr ` S ) M ) <-> ( c e. ( A (repr ` S ) M ) /\ ran c C_ B ) ) )
Theorem	reprlt 30697	There are no representations of M with more than M terms. Remark of [Nathanson] p. 123 (Contributed by Thierry Arnoux, 7-Dec-2021.)
|- ( ph -> A C_ NN )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> M < S )   =>    |- ( ph -> ( A (repr ` S ) M ) = (/) )
Theorem	hashreprin 30698*	Express a sum of representations over an intersection using a product of the indicator function (Contributed by Thierry Arnoux, 11-Dec-2021.)
|- ( ph -> A C_ NN )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> B C_ NN )   =>    |- ( ph -> ( # ` ( ( A i^i B ) (repr ` S ) M ) ) = sum_ c e. ( B (repr ` S ) M ) prod_ a e. ( 0..^ S ) ( ( (𝟭 ` NN ) ` A ) ` ( c ` a ) ) )
Theorem	reprgt 30699	There are no representations of more than ( S x. N ) with only S terms bounded by N. Remark of [Nathanson] p. 123 (Contributed by Thierry Arnoux, 7-Dec-2021.)
|- ( ph -> N e. NN0 )   &    |- ( ph -> A C_ ( 1 ... N ) )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> ( S x. N ) < M )   =>    |- ( ph -> ( A (repr ` S ) M ) = (/) )
Theorem	reprinfz1 30700	For the representation of N, it is sufficient to consider nonnegative integers up to N. Remark of [Nathanson] p. 123 (Contributed by Thierry Arnoux, 13-Dec-2021.)
|- ( ph -> N e. NN0 )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> A C_ NN )   =>    |- ( ph -> ( A (repr ` S ) N ) = ( ( A i^i ( 1 ... N ) ) (repr ` S ) N ) )