Theorem signsvtn0 28343

Description: If the last letter is non zero, then this is the zero-skipping sign. (Contributed by Thierry Arnoux, 8-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 ) )
signsvtn0.1	|- N = ( # ` F )

Assertion

Ref	Expression
signsvtn0	|- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( ( T ` F ) ` ( N - 1 ) ) = (sgn ` ( F ` ( N - 1 ) ) ) )

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

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

Proof of Theorem signsvtn0

Step	Hyp	Ref	Expression
1		eldifsn 4158	. . . . . . . . . . . 12 |- ( F e. (Word RR \ { (/) } ) <-> ( F e. Word RR /\ F =/= (/) ) )
2	1	biimpi 194	. . . . . . . . . . 11 |- ( F e. (Word RR \ { (/) } ) -> ( F e. Word RR /\ F =/= (/) ) )
3	2	adantr 465	. . . . . . . . . 10 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F e. Word RR /\ F =/= (/) ) )
4	3	simpld 459	. . . . . . . . 9 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> F e. Word RR )
5	4	adantr 465	. . . . . . . 8 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> F e. Word RR )
6		wrdf 12534	. . . . . . . 8 |- ( F e. Word RR -> F : ( 0..^ ( # ` F ) ) --> RR )
7	5, 6	syl 16	. . . . . . 7 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> F : ( 0..^ ( # ` F ) ) --> RR )
8		lennncl 12544	. . . . . . . . . 10 |- ( ( F e. Word RR /\ F =/= (/) ) -> ( # ` F ) e. NN )
9	3, 8	syl 16	. . . . . . . . 9 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( # ` F ) e. NN )
10	9	adantr 465	. . . . . . . 8 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( # ` F ) e. NN )
11		lbfzo0 11842	. . . . . . . 8 |- ( 0 e. ( 0..^ ( # ` F ) ) <-> ( # ` F ) e. NN )
12	10, 11	sylibr 212	. . . . . . 7 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> 0 e. ( 0..^ ( # ` F ) ) )
13	7, 12	ffvelrnd 6033	. . . . . 6 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( F ` 0 ) e. RR )
14		signsv.p	. . . . . . 7 |- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
15		signsv.w	. . . . . . 7 |- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }
16		signsv.t	. . . . . . 7 |- T = ( f e. Word RR |-> ( n e. ( 0..^ ( # ` f ) ) |-> ( W gsumg ( i e. ( 0 ... n ) |-> (sgn ` ( f ` i ) ) ) ) ) )
17		signsv.v	. . . . . . 7 |- V = ( f e. Word RR |-> sum_ j e. ( 1..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )
18	14, 15, 16, 17	signstf0 28341	. . . . . 6 |- ( ( F ` 0 ) e. RR -> ( T ` <" ( F ` 0 ) "> ) = <" (sgn ` ( F ` 0 ) ) "> )
19	13, 18	syl 16	. . . . 5 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( T ` <" ( F ` 0 ) "> ) = <" (sgn ` ( F ` 0 ) ) "> )
20		signsvtn0.1	. . . . . . . 8 |- N = ( # ` F )
21		simpr 461	. . . . . . . 8 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> N = 1 )
22	20, 21	syl5eqr 2522	. . . . . . 7 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( # ` F ) = 1 )
23		eqs1 12601	. . . . . . 7 |- ( ( F e. Word RR /\ ( # ` F ) = 1 ) -> F = <" ( F ` 0 ) "> )
24	5, 22, 23	syl2anc 661	. . . . . 6 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> F = <" ( F ` 0 ) "> )
25	24	fveq2d 5876	. . . . 5 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( T ` F ) = ( T ` <" ( F ` 0 ) "> ) )
26		oveq1 6302	. . . . . . . . . 10 |- ( N = 1 -> ( N - 1 ) = ( 1 - 1 ) )
27		1m1e0 10616	. . . . . . . . . 10 |- ( 1 - 1 ) = 0
28	26, 27	syl6eq 2524	. . . . . . . . 9 |- ( N = 1 -> ( N - 1 ) = 0 )
29	28	fveq2d 5876	. . . . . . . 8 |- ( N = 1 -> ( F ` ( N - 1 ) ) = ( F ` 0 ) )
30	29	fveq2d 5876	. . . . . . 7 |- ( N = 1 -> (sgn ` ( F ` ( N - 1 ) ) ) = (sgn ` ( F ` 0 ) ) )
31	30	s1eqd 12593	. . . . . 6 |- ( N = 1 -> <" (sgn ` ( F ` ( N - 1 ) ) ) "> = <" (sgn ` ( F ` 0 ) ) "> )
32	21, 31	syl 16	. . . . 5 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> <" (sgn ` ( F ` ( N - 1 ) ) ) "> = <" (sgn ` ( F ` 0 ) ) "> )
33	19, 25, 32	3eqtr4d 2518	. . . 4 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( T ` F ) = <" (sgn ` ( F ` ( N - 1 ) ) ) "> )
34	21, 28	syl 16	. . . 4 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( N - 1 ) = 0 )
35	33, 34	fveq12d 5878	. . 3 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( ( T ` F ) ` ( N - 1 ) ) = ( <" (sgn ` ( F ` ( N - 1 ) ) ) "> ` 0 ) )
36	4, 6	syl 16	. . . . . . . 8 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> F : ( 0..^ ( # ` F ) ) --> RR )
37	20	oveq1i 6305	. . . . . . . . 9 |- ( N - 1 ) = ( ( # ` F ) - 1 )
38		fzo0end 11884	. . . . . . . . . 10 |- ( ( # ` F ) e. NN -> ( ( # ` F ) - 1 ) e. ( 0..^ ( # ` F ) ) )
39	3, 8, 38	3syl 20	. . . . . . . . 9 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( ( # ` F ) - 1 ) e. ( 0..^ ( # ` F ) ) )
40	37, 39	syl5eqel 2559	. . . . . . . 8 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( N - 1 ) e. ( 0..^ ( # ` F ) ) )
41	36, 40	ffvelrnd 6033	. . . . . . 7 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F ` ( N - 1 ) ) e. RR )
42	41	rexrd 9655	. . . . . 6 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F ` ( N - 1 ) ) e. RR* )
43		sgncl 28293	. . . . . 6 |- ( ( F ` ( N - 1 ) ) e. RR* -> (sgn ` ( F ` ( N - 1 ) ) ) e. { -u 1 , 0 , 1 } )
44	42, 43	syl 16	. . . . 5 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> (sgn ` ( F ` ( N - 1 ) ) ) e. { -u 1 , 0 , 1 } )
45	44	adantr 465	. . . 4 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> (sgn ` ( F ` ( N - 1 ) ) ) e. { -u 1 , 0 , 1 } )
46		s1fv 12599	. . . 4 |- ( (sgn ` ( F ` ( N - 1 ) ) ) e. { -u 1 , 0 , 1 } -> ( <" (sgn ` ( F ` ( N - 1 ) ) ) "> ` 0 ) = (sgn ` ( F ` ( N - 1 ) ) ) )
47	45, 46	syl 16	. . 3 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( <" (sgn ` ( F ` ( N - 1 ) ) ) "> ` 0 ) = (sgn ` ( F ` ( N - 1 ) ) ) )
48	35, 47	eqtrd 2508	. 2 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( ( T ` F ) ` ( N - 1 ) ) = (sgn ` ( F ` ( N - 1 ) ) ) )
49		fzossfz 11826	. . . . . . . . . 10 |- ( 0..^ ( # ` F ) ) C_ ( 0 ... ( # ` F ) )
50	49, 39	sseldi 3507	. . . . . . . . 9 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( ( # ` F ) - 1 ) e. ( 0 ... ( # ` F ) ) )
51		swrd0val 12628	. . . . . . . . 9 |- ( ( F e. Word RR /\ ( ( # ` F ) - 1 ) e. ( 0 ... ( # ` F ) ) ) -> ( F substr <. 0 , ( ( # ` F ) - 1 ) >. ) = ( F |` ( 0..^ ( ( # ` F ) - 1 ) ) ) )
52	4, 50, 51	syl2anc 661	. . . . . . . 8 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F substr <. 0 , ( ( # ` F ) - 1 ) >. ) = ( F |` ( 0..^ ( ( # ` F ) - 1 ) ) ) )
53	52	oveq1d 6310	. . . . . . 7 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( ( F substr <. 0 , ( ( # ` F ) - 1 ) >. ) concat <" ( F ` ( ( # ` F ) - 1 ) ) "> ) = ( ( F |` ( 0..^ ( ( # ` F ) - 1 ) ) ) concat <" ( F ` ( ( # ` F ) - 1 ) ) "> ) )
54		wrdeqcats1 12679	. . . . . . . 8 |- ( ( F e. Word RR /\ F =/= (/) ) -> F = ( ( F substr <. 0 , ( ( # ` F ) - 1 ) >. ) concat <" ( F ` ( ( # ` F ) - 1 ) ) "> ) )
55	3, 54	syl 16	. . . . . . 7 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> F = ( ( F substr <. 0 , ( ( # ` F ) - 1 ) >. ) concat <" ( F ` ( ( # ` F ) - 1 ) ) "> ) )
56	37	oveq2i 6306	. . . . . . . . . 10 |- ( 0..^ ( N - 1 ) ) = ( 0..^ ( ( # ` F ) - 1 ) )
57	56	a1i 11	. . . . . . . . 9 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( 0..^ ( N - 1 ) ) = ( 0..^ ( ( # ` F ) - 1 ) ) )
58	57	reseq2d 5279	. . . . . . . 8 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F |` ( 0..^ ( N - 1 ) ) ) = ( F |` ( 0..^ ( ( # ` F ) - 1 ) ) ) )
59	37	a1i 11	. . . . . . . . . 10 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( N - 1 ) = ( ( # ` F ) - 1 ) )
60	59	fveq2d 5876	. . . . . . . . 9 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F ` ( N - 1 ) ) = ( F ` ( ( # ` F ) - 1 ) ) )
61	60	s1eqd 12593	. . . . . . . 8 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> <" ( F ` ( N - 1 ) ) "> = <" ( F ` ( ( # ` F ) - 1 ) ) "> )
62	58, 61	oveq12d 6313	. . . . . . 7 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( ( F |` ( 0..^ ( N - 1 ) ) ) concat <" ( F ` ( N - 1 ) ) "> ) = ( ( F |` ( 0..^ ( ( # ` F ) - 1 ) ) ) concat <" ( F ` ( ( # ` F ) - 1 ) ) "> ) )
63	53, 55, 62	3eqtr4d 2518	. . . . . 6 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> F = ( ( F |` ( 0..^ ( N - 1 ) ) ) concat <" ( F ` ( N - 1 ) ) "> ) )
64	63	fveq2d 5876	. . . . 5 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( T ` F ) = ( T ` ( ( F |` ( 0..^ ( N - 1 ) ) ) concat <" ( F ` ( N - 1 ) ) "> ) ) )
65		ffn 5737	. . . . . . . . . . 11 |- ( F : ( 0..^ ( # ` F ) ) --> RR -> F Fn ( 0..^ ( # ` F ) ) )
66	4, 6, 65	3syl 20	. . . . . . . . . 10 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> F Fn ( 0..^ ( # ` F ) ) )
67	20	a1i 11	. . . . . . . . . . . 12 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> N = ( # ` F ) )
68	67	oveq2d 6311	. . . . . . . . . . 11 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( 0..^ N ) = ( 0..^ ( # ` F ) ) )
69	68	fneq2d 5678	. . . . . . . . . 10 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F Fn ( 0..^ N ) <-> F Fn ( 0..^ ( # ` F ) ) ) )
70	66, 69	mpbird 232	. . . . . . . . 9 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> F Fn ( 0..^ N ) )
71	20, 9	syl5eqel 2559	. . . . . . . . . . 11 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> N e. NN )
72	71	nnnn0d 10864	. . . . . . . . . 10 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> N e. NN0 )
73		nn0z 10899	. . . . . . . . . 10 |- ( N e. NN0 -> N e. ZZ )
74		fzossrbm1 11834	. . . . . . . . . 10 |- ( N e. ZZ -> ( 0..^ ( N - 1 ) ) C_ ( 0..^ N ) )
75	72, 73, 74	3syl 20	. . . . . . . . 9 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( 0..^ ( N - 1 ) ) C_ ( 0..^ N ) )
76		fnssres 5700	. . . . . . . . 9 |- ( ( F Fn ( 0..^ N ) /\ ( 0..^ ( N - 1 ) ) C_ ( 0..^ N ) ) -> ( F |` ( 0..^ ( N - 1 ) ) ) Fn ( 0..^ ( N - 1 ) ) )
77	70, 75, 76	syl2anc 661	. . . . . . . 8 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F |` ( 0..^ ( N - 1 ) ) ) Fn ( 0..^ ( N - 1 ) ) )
78		hashfn 12423	. . . . . . . 8 |- ( ( F |` ( 0..^ ( N - 1 ) ) ) Fn ( 0..^ ( N - 1 ) ) -> ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) = ( # ` ( 0..^ ( N - 1 ) ) ) )
79	77, 78	syl 16	. . . . . . 7 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) = ( # ` ( 0..^ ( N - 1 ) ) ) )
80		nnm1nn0 10849	. . . . . . . 8 |- ( N e. NN -> ( N - 1 ) e. NN0 )
81		hashfzo0 12468	. . . . . . . 8 |- ( ( N - 1 ) e. NN0 -> ( # ` ( 0..^ ( N - 1 ) ) ) = ( N - 1 ) )
82	71, 80, 81	3syl 20	. . . . . . 7 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( # ` ( 0..^ ( N - 1 ) ) ) = ( N - 1 ) )
83	79, 82	eqtrd 2508	. . . . . 6 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) = ( N - 1 ) )
84	83	eqcomd 2475	. . . . 5 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( N - 1 ) = ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) )
85	64, 84	fveq12d 5878	. . . 4 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( ( T ` F ) ` ( N - 1 ) ) = ( ( T ` ( ( F |` ( 0..^ ( N - 1 ) ) ) concat <" ( F ` ( N - 1 ) ) "> ) ) ` ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) ) )
86	85	adantr 465	. . 3 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( ( T ` F ) ` ( N - 1 ) ) = ( ( T ` ( ( F |` ( 0..^ ( N - 1 ) ) ) concat <" ( F ` ( N - 1 ) ) "> ) ) ` ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) ) )
87	52, 58	eqtr4d 2511	. . . . . . . . 9 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F substr <. 0 , ( ( # ` F ) - 1 ) >. ) = ( F |` ( 0..^ ( N - 1 ) ) ) )
88		swrdcl 12626	. . . . . . . . . 10 |- ( F e. Word RR -> ( F substr <. 0 , ( ( # ` F ) - 1 ) >. ) e. Word RR )
89	4, 88	syl 16	. . . . . . . . 9 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F substr <. 0 , ( ( # ` F ) - 1 ) >. ) e. Word RR )
90	87, 89	eqeltrrd 2556	. . . . . . . 8 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F |` ( 0..^ ( N - 1 ) ) ) e. Word RR )
91	90	adantr 465	. . . . . . 7 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( F |` ( 0..^ ( N - 1 ) ) ) e. Word RR )
92	83	adantr 465	. . . . . . . . 9 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) = ( N - 1 ) )
93	71	adantr 465	. . . . . . . . . . 11 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> N e. NN )
94	93	nncnd 10564	. . . . . . . . . 10 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> N e. CC )
95		1cnd 9624	. . . . . . . . . 10 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> 1 e. CC )
96		simpr 461	. . . . . . . . . 10 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> N =/= 1 )
97	94, 95, 96	subne0d 9951	. . . . . . . . 9 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( N - 1 ) =/= 0 )
98	92, 97	eqnetrd 2760	. . . . . . . 8 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) =/= 0 )
99		fveq2 5872	. . . . . . . . . 10 |- ( ( F |` ( 0..^ ( N - 1 ) ) ) = (/) -> ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) = ( # ` (/) ) )
100		hash0 12417	. . . . . . . . . 10 |- ( # ` (/) ) = 0
101	99, 100	syl6eq 2524	. . . . . . . . 9 |- ( ( F |` ( 0..^ ( N - 1 ) ) ) = (/) -> ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) = 0 )
102	101	necon3i 2707	. . . . . . . 8 |- ( ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) =/= 0 -> ( F |` ( 0..^ ( N - 1 ) ) ) =/= (/) )
103	98, 102	syl 16	. . . . . . 7 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( F |` ( 0..^ ( N - 1 ) ) ) =/= (/) )
104	91, 103	jca 532	. . . . . 6 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( ( F |` ( 0..^ ( N - 1 ) ) ) e. Word RR /\ ( F |` ( 0..^ ( N - 1 ) ) ) =/= (/) ) )
105		eldifsn 4158	. . . . . 6 |- ( ( F |` ( 0..^ ( N - 1 ) ) ) e. (Word RR \ { (/) } ) <-> ( ( F |` ( 0..^ ( N - 1 ) ) ) e. Word RR /\ ( F |` ( 0..^ ( N - 1 ) ) ) =/= (/) ) )
106	104, 105	sylibr 212	. . . . 5 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( F |` ( 0..^ ( N - 1 ) ) ) e. (Word RR \ { (/) } ) )
107	41	adantr 465	. . . . 5 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( F ` ( N - 1 ) ) e. RR )
108	14, 15, 16, 17	signstfvn 28342	. . . . 5 |- ( ( ( F |` ( 0..^ ( N - 1 ) ) ) e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) e. RR ) -> ( ( T ` ( ( F |` ( 0..^ ( N - 1 ) ) ) concat <" ( F ` ( N - 1 ) ) "> ) ) ` ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) ) = ( ( ( T ` ( F |` ( 0..^ ( N - 1 ) ) ) ) ` ( ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) - 1 ) ) .+^ (sgn ` ( F ` ( N - 1 ) ) ) ) )
109	106, 107, 108	syl2anc 661	. . . 4 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( ( T ` ( ( F |` ( 0..^ ( N - 1 ) ) ) concat <" ( F ` ( N - 1 ) ) "> ) ) ` ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) ) = ( ( ( T ` ( F |` ( 0..^ ( N - 1 ) ) ) ) ` ( ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) - 1 ) ) .+^ (sgn ` ( F ` ( N - 1 ) ) ) ) )
110		lennncl 12544	. . . . . . 7 |- ( ( ( F |` ( 0..^ ( N - 1 ) ) ) e. Word RR /\ ( F |` ( 0..^ ( N - 1 ) ) ) =/= (/) ) -> ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) e. NN )
111		fzo0end 11884	. . . . . . 7 |- ( ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) e. NN -> ( ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) - 1 ) e. ( 0..^ ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) ) )
112	104, 110, 111	3syl 20	. . . . . 6 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) - 1 ) e. ( 0..^ ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) ) )
113	14, 15, 16, 17	signstcl 28338	. . . . . 6 |- ( ( ( F |` ( 0..^ ( N - 1 ) ) ) e. Word RR /\ ( ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) - 1 ) e. ( 0..^ ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) ) ) -> ( ( T ` ( F |` ( 0..^ ( N - 1 ) ) ) ) ` ( ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) - 1 ) ) e. { -u 1 , 0 , 1 } )
114	91, 112, 113	syl2anc 661	. . . . 5 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( ( T ` ( F |` ( 0..^ ( N - 1 ) ) ) ) ` ( ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) - 1 ) ) e. { -u 1 , 0 , 1 } )
115	44	adantr 465	. . . . 5 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> (sgn ` ( F ` ( N - 1 ) ) ) e. { -u 1 , 0 , 1 } )
116		simpr 461	. . . . . . 7 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F ` ( N - 1 ) ) =/= 0 )
117		sgn0bi 28302	. . . . . . . . 9 |- ( ( F ` ( N - 1 ) ) e. RR* -> ( (sgn ` ( F ` ( N - 1 ) ) ) = 0 <-> ( F ` ( N - 1 ) ) = 0 ) )
118	117	necon3bid 2725	. . . . . . . 8 |- ( ( F ` ( N - 1 ) ) e. RR* -> ( (sgn ` ( F ` ( N - 1 ) ) ) =/= 0 <-> ( F ` ( N - 1 ) ) =/= 0 ) )
119	118	biimpar 485	. . . . . . 7 |- ( ( ( F ` ( N - 1 ) ) e. RR* /\ ( F ` ( N - 1 ) ) =/= 0 ) -> (sgn ` ( F ` ( N - 1 ) ) ) =/= 0 )
120	42, 116, 119	syl2anc 661	. . . . . 6 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> (sgn ` ( F ` ( N - 1 ) ) ) =/= 0 )
121	120	adantr 465	. . . . 5 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> (sgn ` ( F ` ( N - 1 ) ) ) =/= 0 )
122	14, 15	signswlid 28332	. . . . 5 |- ( ( ( ( ( T ` ( F |` ( 0..^ ( N - 1 ) ) ) ) ` ( ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) - 1 ) ) e. { -u 1 , 0 , 1 } /\ (sgn ` ( F ` ( N - 1 ) ) ) e. { -u 1 , 0 , 1 } ) /\ (sgn ` ( F ` ( N - 1 ) ) ) =/= 0 ) -> ( ( ( T ` ( F |` ( 0..^ ( N - 1 ) ) ) ) ` ( ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) - 1 ) ) .+^ (sgn ` ( F ` ( N - 1 ) ) ) ) = (sgn ` ( F ` ( N - 1 ) ) ) )
123	114, 115, 121, 122	syl21anc 1227	. . . 4 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( ( ( T ` ( F |` ( 0..^ ( N - 1 ) ) ) ) ` ( ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) - 1 ) ) .+^ (sgn ` ( F ` ( N - 1 ) ) ) ) = (sgn ` ( F ` ( N - 1 ) ) ) )
124	109, 123	eqtrd 2508	. . 3 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( ( T ` ( ( F |` ( 0..^ ( N - 1 ) ) ) concat <" ( F ` ( N - 1 ) ) "> ) ) ` ( # ` ( F |` ( 0..^ ( N - 1 ) ) ) ) ) = (sgn ` ( F ` ( N - 1 ) ) ) )
125	86, 124	eqtrd 2508	. 2 |- ( ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( ( T ` F ) ` ( N - 1 ) ) = (sgn ` ( F ` ( N - 1 ) ) ) )
126	48, 125	pm2.61dane 2785	1 |- ( ( F e. (Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( ( T ` F ) ` ( N - 1 ) ) = (sgn ` ( F ` ( N - 1 ) ) ) )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1379   e. wcel 1767   =/= wne 2662   \ cdif 3478   C_ wss 3481   (/)c0 3790   ifcif 3945   {csn 4033   {cpr 4035   {ctp 4037   <.cop 4039   |-> cmpt 4511   |` cres 5007   Fn wfn 5589   -->wf 5590   ` cfv 5594  (class class class)co 6295   |-> cmpt2 6297   RRcr 9503   0cc0 9504   1c1 9505   RR*cxr 9639   - cmin 9817   -ucneg 9818   NNcn 10548   NN0cn0 10807   ZZcz 10876   ...cfz 11684  ..^cfzo 11804   #chash 12385  Word cword 12515   concat cconcat 12517   <"cs1 12518   substr csubstr 12519  sgncsgn 12899   sum_csu 13488   ndxcnx 14504   Basecbs 14507   +g cplusg 14572   gsum_g cgsu 14713

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-inf2 8070  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-se 4845  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6696  df-1st 6795  df-2nd 6796  df-supp 6914  df-recs 7054  df-rdg 7088  df-1o 7142  df-oadd 7146  df-er 7323  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-oi 7947  df-card 8332  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-nn 10549  df-2 10606  df-n0 10808  df-z 10877  df-uz 11095  df-fz 11685  df-fzo 11805  df-seq 12088  df-hash 12386  df-word 12523  df-concat 12525  df-s1 12526  df-substr 12527  df-sgn 12900  df-struct 14509  df-ndx 14510  df-slot 14511  df-base 14512  df-plusg 14585  df-0g 14714  df-gsum 14715  df-mgm 15746  df-sgrp 15785  df-mnd 15795  df-mulg 15932  df-cntz 16227

This theorem is referenced by:  signsvfpn  28358  signsvfnn  28359