Theorem signsvfn 26998

Description: Number of changes in a word compared to a shorter word. (Contributed by Thierry Arnoux, 12-Oct-2018.)

Hypotheses

Ref	Expression
signsv.p	|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
signsv.w	|- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }
signsv.t	|- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )
signsv.v	|- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )

Assertion

Ref	Expression
signsvfn	|- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( V ` ( F concat <" K "> ) ) = ( ( V ` F ) + if ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. K ) < 0 , 1 , 0 ) ) )

Distinct variable groups:   a, b, .+^   f, i, n, F   f, K, i, n   f, W, i, n   i, a, j, n, F, b   K, a, b, j, f   T, a   f, b, T, j, n

Allowed substitution hints:   .+^ ( f, i, j, n)   T( i)   V( f, i, j, n, a, b)   W( j, a, b)

Proof of Theorem signsvfn

Step	Hyp	Ref	Expression
1		simpl 457	. . . . . . 7 |- ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) -> F e. (Word RR \ { (/) } ) )
2	1	eldifad 3355	. . . . . 6 |- ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) -> F e. Word RR )
3		simpr 461	. . . . . . 7 |- ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) -> K e. RR )
4	3	s1cld 12309	. . . . . 6 |- ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) -> <" K "> e. Word RR )
5		ccatcl 12289	. . . . . 6 |- ( ( F e. Word RR /\ <" K "> e. Word RR ) -> ( F concat <" K "> ) e. Word RR )
6	2, 4, 5	syl2anc 661	. . . . 5 |- ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) -> ( F concat <" K "> ) e. Word RR )
7		signsv.p	. . . . . 6 |- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
8		signsv.w	. . . . . 6 |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }
9		signsv.t	. . . . . 6 |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )
10		signsv.v	. . . . . 6 |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )
11	7, 8, 9, 10	signsvvfval 26994	. . . . 5 |- ( ( F concat <" K "> ) e. Word RR -> ( V ` ( F concat <" K "> ) ) = sum_ j e. ( 1..^ ( # ` ( F concat <" K "> ) ) ) if ( ( ( T ` ( F concat <" K "> ) ) ` j ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) )
12	6, 11	syl 16	. . . 4 |- ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) -> ( V ` ( F concat <" K "> ) ) = sum_ j e. ( 1..^ ( # ` ( F concat <" K "> ) ) ) if ( ( ( T ` ( F concat <" K "> ) ) ` j ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) )
13		ccatlen 12290	. . . . . . . 8 |- ( ( F e. Word RR /\ <" K "> e. Word RR ) -> ( # ` ( F concat <" K "> ) ) = ( ( # ` F ) + ( # ` <" K "> ) ) )
14	2, 4, 13	syl2anc 661	. . . . . . 7 |- ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) -> ( # ` ( F concat <" K "> ) ) = ( ( # ` F ) + ( # ` <" K "> ) ) )
15		s1len 12311	. . . . . . . 8 |- ( # ` <" K "> ) = 1
16	15	oveq2i 6117	. . . . . . 7 |- ( ( # ` F ) + ( # ` <" K "> ) ) = ( ( # ` F ) + 1 )
17	14, 16	syl6eq 2491	. . . . . 6 |- ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) -> ( # ` ( F concat <" K "> ) ) = ( ( # ` F ) + 1 ) )
18	17	oveq2d 6122	. . . . 5 |- ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) -> ( 1..^ ( # ` ( F concat <" K "> ) ) ) = ( 1..^ ( ( # ` F ) + 1 ) ) )
19	18	sumeq1d 13193	. . . 4 |- ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) -> sum_ j e. ( 1..^ ( # ` ( F concat <" K "> ) ) ) if ( ( ( T ` ( F concat <" K "> ) ) ` j ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) = sum_ j e. ( 1..^ ( ( # ` F ) + 1 ) ) if ( ( ( T ` ( F concat <" K "> ) ) ` j ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) )
20		eldifsn 4015	. . . . . . . 8 |- ( F e. (Word RR \ { (/) } ) <-> ( F e. Word RR /\ F =/= (/) ) )
21		lennncl 12265	. . . . . . . 8 |- ( ( F e. Word RR /\ F =/= (/) ) -> ( # ` F ) e. NN )
22	20, 21	sylbi 195	. . . . . . 7 |- ( F e. (Word RR \ { (/) } ) -> ( # ` F ) e. NN )
23		nnuz 10911	. . . . . . 7 |- NN = ( ZZ>= ` 1 )
24	22, 23	syl6eleq 2533	. . . . . 6 |- ( F e. (Word RR \ { (/) } ) -> ( # ` F ) e. ( ZZ>= ` 1 ) )
25	24	adantr 465	. . . . 5 |- ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) -> ( # ` F ) e. ( ZZ>= ` 1 ) )
26		ax-1cn 9355	. . . . . . 7 |- 1 e. CC
27	26	a1i 11	. . . . . 6 |- ( ( ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1 ... ( # ` F ) ) ) /\ ( ( T ` ( F concat <" K "> ) ) ` j ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) ) -> 1 e. CC )
28		0cnd 9394	. . . . . 6 |- ( ( ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1 ... ( # ` F ) ) ) /\ -. ( ( T ` ( F concat <" K "> ) ) ` j ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) ) -> 0 e. CC )
29	27, 28	ifclda 3836	. . . . 5 |- ( ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1 ... ( # ` F ) ) ) -> if ( ( ( T ` ( F concat <" K "> ) ) ` j ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) e. CC )
30		fveq2 5706	. . . . . . 7 |- ( j = ( # ` F ) -> ( ( T ` ( F concat <" K "> ) ) ` j ) = ( ( T ` ( F concat <" K "> ) ) ` ( # ` F ) ) )
31		oveq1 6113	. . . . . . . 8 |- ( j = ( # ` F ) -> ( j - 1 ) = ( ( # ` F ) - 1 ) )
32	31	fveq2d 5710	. . . . . . 7 |- ( j = ( # ` F ) -> ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) = ( ( T ` ( F concat <" K "> ) ) ` ( ( # ` F ) - 1 ) ) )
33	30, 32	neeq12d 2638	. . . . . 6 |- ( j = ( # ` F ) -> ( ( ( T ` ( F concat <" K "> ) ) ` j ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) <-> ( ( T ` ( F concat <" K "> ) ) ` ( # ` F ) ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( ( # ` F ) - 1 ) ) ) )
34	33	ifbid 3826	. . . . 5 |- ( j = ( # ` F ) -> if ( ( ( T ` ( F concat <" K "> ) ) ` j ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) = if ( ( ( T ` ( F concat <" K "> ) ) ` ( # ` F ) ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( ( # ` F ) - 1 ) ) , 1 , 0 ) )
35	25, 29, 34	fzosump1 13236	. . . 4 |- ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) -> sum_ j e. ( 1..^ ( ( # ` F ) + 1 ) ) if ( ( ( T ` ( F concat <" K "> ) ) ` j ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) = ( sum_ j e. ( 1..^ ( # ` F ) ) if ( ( ( T ` ( F concat <" K "> ) ) ` j ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) + if ( ( ( T ` ( F concat <" K "> ) ) ` ( # ` F ) ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( ( # ` F ) - 1 ) ) , 1 , 0 ) ) )
36	12, 19, 35	3eqtrd 2479	. . 3 |- ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) -> ( V ` ( F concat <" K "> ) ) = ( sum_ j e. ( 1..^ ( # ` F ) ) if ( ( ( T ` ( F concat <" K "> ) ) ` j ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) + if ( ( ( T ` ( F concat <" K "> ) ) ` ( # ` F ) ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( ( # ` F ) - 1 ) ) , 1 , 0 ) ) )
37	36	adantlr 714	. 2 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( V ` ( F concat <" K "> ) ) = ( sum_ j e. ( 1..^ ( # ` F ) ) if ( ( ( T ` ( F concat <" K "> ) ) ` j ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) + if ( ( ( T ` ( F concat <" K "> ) ) ` ( # ` F ) ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( ( # ` F ) - 1 ) ) , 1 , 0 ) ) )
38	2	adantr 465	. . . . . . . . 9 |- ( ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1..^ ( # ` F ) ) ) -> F e. Word RR )
39	3	adantr 465	. . . . . . . . 9 |- ( ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1..^ ( # ` F ) ) ) -> K e. RR )
40		1nn0 10610	. . . . . . . . . . . . 13 |- 1 e. NN0
41		nn0uz 10910	. . . . . . . . . . . . 13 |- NN0 = ( ZZ>= ` 0 )
42	40, 41	eleqtri 2515	. . . . . . . . . . . 12 |- 1 e. ( ZZ>= ` 0 )
43		fzoss1 11591	. . . . . . . . . . . 12 |- ( 1 e. ( ZZ>= ` 0 ) -> ( 1..^ ( # ` F ) ) C_ ( 0..^ ( # ` F ) ) )
44	42, 43	ax-mp 5	. . . . . . . . . . 11 |- ( 1..^ ( # ` F ) ) C_ ( 0..^ ( # ` F ) )
45	44	a1i 11	. . . . . . . . . 10 |- ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) -> ( 1..^ ( # ` F ) ) C_ ( 0..^ ( # ` F ) ) )
46	45	sselda 3371	. . . . . . . . 9 |- ( ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1..^ ( # ` F ) ) ) -> j e. ( 0..^ ( # ` F ) ) )
47	7, 8, 9, 10	signstfvp 26987	. . . . . . . . 9 |- ( ( F e. Word RR /\ K e. RR /\ j e. ( 0..^ ( # ` F ) ) ) -> ( ( T ` ( F concat <" K "> ) ) ` j ) = ( ( T ` F ) ` j ) )
48	38, 39, 46, 47	syl3anc 1218	. . . . . . . 8 |- ( ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1..^ ( # ` F ) ) ) -> ( ( T ` ( F concat <" K "> ) ) ` j ) = ( ( T ` F ) ` j ) )
49		elfzoel2 11567	. . . . . . . . . . . . 13 |- ( j e. ( 1..^ ( # ` F ) ) -> ( # ` F ) e. ZZ )
50	49	adantl 466	. . . . . . . . . . . 12 |- ( ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1..^ ( # ` F ) ) ) -> ( # ` F ) e. ZZ )
51		eluzmn 26950	. . . . . . . . . . . 12 |- ( ( ( # ` F ) e. ZZ /\ 1 e. NN0 ) -> ( # ` F ) e. ( ZZ>= ` ( ( # ` F ) - 1 ) ) )
52	50, 40, 51	sylancl 662	. . . . . . . . . . 11 |- ( ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1..^ ( # ` F ) ) ) -> ( # ` F ) e. ( ZZ>= ` ( ( # ` F ) - 1 ) ) )
53		fzoss2 11592	. . . . . . . . . . 11 |- ( ( # ` F ) e. ( ZZ>= ` ( ( # ` F ) - 1 ) ) -> ( 0..^ ( ( # ` F ) - 1 ) ) C_ ( 0..^ ( # ` F ) ) )
54	52, 53	syl 16	. . . . . . . . . 10 |- ( ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1..^ ( # ` F ) ) ) -> ( 0..^ ( ( # ` F ) - 1 ) ) C_ ( 0..^ ( # ` F ) ) )
55		simpr 461	. . . . . . . . . . 11 |- ( ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1..^ ( # ` F ) ) ) -> j e. ( 1..^ ( # ` F ) ) )
56		elfzoelz 11568	. . . . . . . . . . . . 13 |- ( j e. ( 1..^ ( # ` F ) ) -> j e. ZZ )
57	56	adantl 466	. . . . . . . . . . . 12 |- ( ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1..^ ( # ` F ) ) ) -> j e. ZZ )
58		elfzom1b 11641	. . . . . . . . . . . 12 |- ( ( j e. ZZ /\ ( # ` F ) e. ZZ ) -> ( j e. ( 1..^ ( # ` F ) ) <-> ( j - 1 ) e. ( 0..^ ( ( # ` F ) - 1 ) ) ) )
59	57, 50, 58	syl2anc 661	. . . . . . . . . . 11 |- ( ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1..^ ( # ` F ) ) ) -> ( j e. ( 1..^ ( # ` F ) ) <-> ( j - 1 ) e. ( 0..^ ( ( # ` F ) - 1 ) ) ) )
60	55, 59	mpbid 210	. . . . . . . . . 10 |- ( ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1..^ ( # ` F ) ) ) -> ( j - 1 ) e. ( 0..^ ( ( # ` F ) - 1 ) ) )
61	54, 60	sseldd 3372	. . . . . . . . 9 |- ( ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1..^ ( # ` F ) ) ) -> ( j - 1 ) e. ( 0..^ ( # ` F ) ) )
62	7, 8, 9, 10	signstfvp 26987	. . . . . . . . 9 |- ( ( F e. Word RR /\ K e. RR /\ ( j - 1 ) e. ( 0..^ ( # ` F ) ) ) -> ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) = ( ( T ` F ) ` ( j - 1 ) ) )
63	38, 39, 61, 62	syl3anc 1218	. . . . . . . 8 |- ( ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1..^ ( # ` F ) ) ) -> ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) = ( ( T ` F ) ` ( j - 1 ) ) )
64	48, 63	neeq12d 2638	. . . . . . 7 |- ( ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1..^ ( # ` F ) ) ) -> ( ( ( T ` ( F concat <" K "> ) ) ` j ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) <-> ( ( T ` F ) ` j ) =/= ( ( T ` F ) ` ( j - 1 ) ) ) )
65	64	ifbid 3826	. . . . . 6 |- ( ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1..^ ( # ` F ) ) ) -> if ( ( ( T ` ( F concat <" K "> ) ) ` j ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) = if ( ( ( T ` F ) ` j ) =/= ( ( T ` F ) ` ( j - 1 ) ) , 1 , 0 ) )
66	65	sumeq2dv 13195	. . . . 5 |- ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) -> sum_ j e. ( 1..^ ( # ` F ) ) if ( ( ( T ` ( F concat <" K "> ) ) ` j ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) = sum_ j e. ( 1..^ ( # ` F ) ) if ( ( ( T ` F ) ` j ) =/= ( ( T ` F ) ` ( j - 1 ) ) , 1 , 0 ) )
67	7, 8, 9, 10	signsvvfval 26994	. . . . . 6 |- ( F e. Word RR -> ( V ` F ) = sum_ j e. ( 1..^ ( # ` F ) ) if ( ( ( T ` F ) ` j ) =/= ( ( T ` F ) ` ( j - 1 ) ) , 1 , 0 ) )
68	2, 67	syl 16	. . . . 5 |- ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) -> ( V ` F ) = sum_ j e. ( 1..^ ( # ` F ) ) if ( ( ( T ` F ) ` j ) =/= ( ( T ` F ) ` ( j - 1 ) ) , 1 , 0 ) )
69	66, 68	eqtr4d 2478	. . . 4 |- ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) -> sum_ j e. ( 1..^ ( # ` F ) ) if ( ( ( T ` ( F concat <" K "> ) ) ` j ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) = ( V ` F ) )
70	69	adantlr 714	. . 3 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> sum_ j e. ( 1..^ ( # ` F ) ) if ( ( ( T ` ( F concat <" K "> ) ) ` j ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) = ( V ` F ) )
71	7, 8, 9, 10	signstfvn 26985	. . . . . . 7 |- ( ( F e. (Word RR \ { (/) } ) /\ K e. RR ) -> ( ( T ` ( F concat <" K "> ) ) ` ( # ` F ) ) = ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) .+^ (sgn ` K ) ) )
72	71	adantlr 714	. . . . . 6 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( T ` ( F concat <" K "> ) ) ` ( # ` F ) ) = ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) .+^ (sgn ` K ) ) )
73	2	adantlr 714	. . . . . . 7 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> F e. Word RR )
74		simpr 461	. . . . . . 7 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> K e. RR )
75	22	ad2antrr 725	. . . . . . . 8 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( # ` F ) e. NN )
76		fzo0end 11634	. . . . . . . 8 |- ( ( # ` F ) e. NN -> ( ( # ` F ) - 1 ) e. ( 0..^ ( # ` F ) ) )
77	75, 76	syl 16	. . . . . . 7 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( # ` F ) - 1 ) e. ( 0..^ ( # ` F ) ) )
78	7, 8, 9, 10	signstfvp 26987	. . . . . . 7 |- ( ( F e. Word RR /\ K e. RR /\ ( ( # ` F ) - 1 ) e. ( 0..^ ( # ` F ) ) ) -> ( ( T ` ( F concat <" K "> ) ) ` ( ( # ` F ) - 1 ) ) = ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) )
79	73, 74, 77, 78	syl3anc 1218	. . . . . 6 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( T ` ( F concat <" K "> ) ) ` ( ( # ` F ) - 1 ) ) = ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) )
80	72, 79	neeq12d 2638	. . . . 5 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( ( T ` ( F concat <" K "> ) ) ` ( # ` F ) ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( ( # ` F ) - 1 ) ) <-> ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) .+^ (sgn ` K ) ) =/= ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) ) )
81	7, 8, 9, 10	signstfvcl 26989	. . . . . . 7 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( ( # ` F ) - 1 ) e. ( 0..^ ( # ` F ) ) ) -> ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) e. { -u 1 , 1 } )
82	77, 81	syldan 470	. . . . . 6 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) e. { -u 1 , 1 } )
83	74	rexrd 9448	. . . . . . 7 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> K e. RR* )
84		sgncl 26936	. . . . . . 7 |- ( K e. RR* -> (sgn ` K ) e. { -u 1 , 0 , 1 } )
85	83, 84	syl 16	. . . . . 6 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> (sgn ` K ) e. { -u 1 , 0 , 1 } )
86	7, 8	signswch 26977	. . . . . 6 |- ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) e. { -u 1 , 1 } /\ (sgn ` K ) e. { -u 1 , 0 , 1 } ) -> ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) .+^ (sgn ` K ) ) =/= ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) <-> ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. (sgn ` K ) ) < 0 ) )
87	82, 85, 86	syl2anc 661	. . . . 5 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) .+^ (sgn ` K ) ) =/= ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) <-> ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. (sgn ` K ) ) < 0 ) )
88		sgnsgn 26946	. . . . . . . . 9 |- ( K e. RR* -> (sgn ` (sgn ` K ) ) = (sgn ` K ) )
89	83, 88	syl 16	. . . . . . . 8 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> (sgn ` (sgn ` K ) ) = (sgn ` K ) )
90	89	oveq2d 6122	. . . . . . 7 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( (sgn ` ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) ) x. (sgn ` (sgn ` K ) ) ) = ( (sgn ` ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) ) x. (sgn ` K ) ) )
91	90	breq1d 4317	. . . . . 6 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( (sgn ` ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) ) x. (sgn ` (sgn ` K ) ) ) < 0 <-> ( (sgn ` ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) ) x. (sgn ` K ) ) < 0 ) )
92		neg1rr 10441	. . . . . . . . 9 |- -u 1 e. RR
93		1re 9400	. . . . . . . . 9 |- 1 e. RR
94		prssi 4044	. . . . . . . . 9 |- ( ( -u 1 e. RR /\ 1 e. RR ) -> { -u 1 , 1 } C_ RR )
95	92, 93, 94	mp2an 672	. . . . . . . 8 |- { -u 1 , 1 } C_ RR
96	95, 82	sseldi 3369	. . . . . . 7 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) e. RR )
97		sgnclre 26937	. . . . . . . 8 |- ( K e. RR -> (sgn ` K ) e. RR )
98	74, 97	syl 16	. . . . . . 7 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> (sgn ` K ) e. RR )
99		sgnmulsgn 26947	. . . . . . 7 |- ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) e. RR /\ (sgn ` K ) e. RR ) -> ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. (sgn ` K ) ) < 0 <-> ( (sgn ` ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) ) x. (sgn ` (sgn ` K ) ) ) < 0 ) )
100	96, 98, 99	syl2anc 661	. . . . . 6 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. (sgn ` K ) ) < 0 <-> ( (sgn ` ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) ) x. (sgn ` (sgn ` K ) ) ) < 0 ) )
101		sgnmulsgn 26947	. . . . . . 7 |- ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) e. RR /\ K e. RR ) -> ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. K ) < 0 <-> ( (sgn ` ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) ) x. (sgn ` K ) ) < 0 ) )
102	96, 74, 101	syl2anc 661	. . . . . 6 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. K ) < 0 <-> ( (sgn ` ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) ) x. (sgn ` K ) ) < 0 ) )
103	91, 100, 102	3bitr4d 285	. . . . 5 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. (sgn ` K ) ) < 0 <-> ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. K ) < 0 ) )
104	80, 87, 103	3bitrd 279	. . . 4 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( ( T ` ( F concat <" K "> ) ) ` ( # ` F ) ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( ( # ` F ) - 1 ) ) <-> ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. K ) < 0 ) )
105	104	ifbid 3826	. . 3 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> if ( ( ( T ` ( F concat <" K "> ) ) ` ( # ` F ) ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( ( # ` F ) - 1 ) ) , 1 , 0 ) = if ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. K ) < 0 , 1 , 0 ) )
106	70, 105	oveq12d 6124	. 2 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( sum_ j e. ( 1..^ ( # ` F ) ) if ( ( ( T ` ( F concat <" K "> ) ) ` j ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) + if ( ( ( T ` ( F concat <" K "> ) ) ` ( # ` F ) ) =/= ( ( T ` ( F concat <" K "> ) ) ` ( ( # ` F ) - 1 ) ) , 1 , 0 ) ) = ( ( V ` F ) + if ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. K ) < 0 , 1 , 0 ) ) )
107	37, 106	eqtrd 2475	1 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( V ` ( F concat <" K "> ) ) = ( ( V ` F ) + if ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. K ) < 0 , 1 , 0 ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1369   e. wcel 1756   =/= wne 2620   \ cdif 3340   C_ wss 3343   (/)c0 3652   ifcif 3806   {csn 3892   {cpr 3894   {ctp 3896   <.cop 3898   class class class wbr 4307   e. cmpt 4365   ` cfv 5433  (class class class)co 6106   e. cmpt2 6108   CCcc 9295   RRcr 9296   0cc0 9297   1c1 9298   + caddc 9300   x. cmul 9302   RR*cxr 9432   < clt 9433   - cmin 9610   -ucneg 9611   NNcn 10337   NN0cn0 10594   ZZcz 10661   ZZ>=cuz 10876   ...cfz 11452  ..^cfzo 11563   #chash 12118  Word cword 12236   concat cconcat 12238   <"cs1 12239  sgncsgn 12590   sum_csu 13178   ndxcnx 14186   Basecbs 14189   +g cplusg 14253   gsum_g cgsu 14394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4418  ax-sep 4428  ax-nul 4436  ax-pow 4485  ax-pr 4546  ax-un 6387  ax-inf2 7862  ax-cnex 9353  ax-resscn 9354  ax-1cn 9355  ax-icn 9356  ax-addcl 9357  ax-addrcl 9358  ax-mulcl 9359  ax-mulrcl 9360  ax-mulcom 9361  ax-addass 9362  ax-mulass 9363  ax-distr 9364  ax-i2m1 9365  ax-1ne0 9366  ax-1rid 9367  ax-rnegex 9368  ax-rrecex 9369  ax-cnre 9370  ax-pre-lttri 9371  ax-pre-lttrn 9372  ax-pre-ltadd 9373  ax-pre-mulgt0 9374  ax-pre-sup 9375

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2735  df-rex 2736  df-reu 2737  df-rmo 2738  df-rab 2739  df-v 2989  df-sbc 3202  df-csb 3304  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-pss 3359  df-nul 3653  df-if 3807  df-pw 3877  df-sn 3893  df-pr 3895  df-tp 3897  df-op 3899  df-uni 4107  df-int 4144  df-iun 4188  df-br 4308  df-opab 4366  df-mpt 4367  df-tr 4401  df-eprel 4647  df-id 4651  df-po 4656  df-so 4657  df-fr 4694  df-se 4695  df-we 4696  df-ord 4737  df-on 4738  df-lim 4739  df-suc 4740  df-xp 4861  df-rel 4862  df-cnv 4863  df-co 4864  df-dm 4865  df-rn 4866  df-res 4867  df-ima 4868  df-iota 5396  df-fun 5435  df-fn 5436  df-f 5437  df-f1 5438  df-fo 5439  df-f1o 5440  df-fv 5441  df-isom 5442  df-riota 6067  df-ov 6109  df-oprab 6110  df-mpt2 6111  df-om 6492  df-1st 6592  df-2nd 6593  df-supp 6706  df-recs 6847  df-rdg 6881  df-1o 6935  df-oadd 6939  df-er 7116  df-en 7326  df-dom 7327  df-sdom 7328  df-fin 7329  df-sup 7706  df-oi 7739  df-card 8124  df-pnf 9435  df-mnf 9436  df-xr 9437  df-ltxr 9438  df-le 9439  df-sub 9612  df-neg 9613  df-div 10009  df-nn 10338  df-2 10395  df-3 10396  df-n0 10595  df-z 10662  df-uz 10877  df-rp 11007  df-fz 11453  df-fzo 11564  df-seq 11822  df-exp 11881  df-hash 12119  df-word 12244  df-concat 12246  df-s1 12247  df-substr 12248  df-sgn 12591  df-cj 12603  df-re 12604  df-im 12605  df-sqr 12739  df-abs 12740  df-clim 12981  df-sum 13179  df-struct 14191  df-ndx 14192  df-slot 14193  df-base 14194  df-plusg 14266  df-0g 14395  df-gsum 14396  df-mnd 15430  df-mulg 15563  df-cntz 15850

This theorem is referenced by:  signsvtp  26999  signsvtn  27000  signlem0  27003