Metamath Proof Explorer

Theorem signstfveq0a

Description: Lemma for signstfveq0 . (Contributed by Thierry Arnoux, 11-Oct-2018)

Ref Expression
Hypotheses 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 gsum ( 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 ) )
signstfveq0.1 
|- N = ( # ` F )
Assertion signstfveq0a 
|- ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> N e. ( ZZ>= ` 2 ) )

Proof

Step Hyp Ref Expression
1 signsv.p 
 |-  .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
2 signsv.w 
 |-  W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }
3 signsv.t 
 |-  T = ( f e. Word RR |-> ( n e. ( 0 ..^ ( # ` f ) ) |-> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( f ` i ) ) ) ) ) )
4 signsv.v 
 |-  V = ( f e. Word RR |-> sum_ j e. ( 1 ..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )
5 signstfveq0.1 
 |-  N = ( # ` F )
6 simpll 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> F e. ( Word RR \ { (/) } ) )
7 6 eldifad 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> F e. Word RR )
8 lencl 
 |-  ( F e. Word RR -> ( # ` F ) e. NN0 )
9 5 8 eqeltrid 
 |-  ( F e. Word RR -> N e. NN0 )
10 7 9 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> N e. NN0 )
11 eldifsn 
 |-  ( F e. ( Word RR \ { (/) } ) <-> ( F e. Word RR /\ F =/= (/) ) )
12 6 11 sylib 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( F e. Word RR /\ F =/= (/) ) )
13 hasheq0 
 |-  ( F e. Word RR -> ( ( # ` F ) = 0 <-> F = (/) ) )
14 13 necon3bid 
 |-  ( F e. Word RR -> ( ( # ` F ) =/= 0 <-> F =/= (/) ) )
15 14 biimpar 
 |-  ( ( F e. Word RR /\ F =/= (/) ) -> ( # ` F ) =/= 0 )
16 5 neeq1i 
 |-  ( N =/= 0 <-> ( # ` F ) =/= 0 )
17 15 16 sylibr 
 |-  ( ( F e. Word RR /\ F =/= (/) ) -> N =/= 0 )
18 12 17 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> N =/= 0 )
19 elnnne0 
 |-  ( N e. NN <-> ( N e. NN0 /\ N =/= 0 ) )
20 10 18 19 sylanbrc 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> N e. NN )
21 simplr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( F ` 0 ) =/= 0 )
22 simpr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( F ` ( N - 1 ) ) = 0 )
23 21 22 neeqtrrd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( F ` 0 ) =/= ( F ` ( N - 1 ) ) )
24 23 necomd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( F ` ( N - 1 ) ) =/= ( F ` 0 ) )
25 oveq1 
 |-  ( N = 1 -> ( N - 1 ) = ( 1 - 1 ) )
26 1m1e0 
 |-  ( 1 - 1 ) = 0
27 25 26 eqtrdi 
 |-  ( N = 1 -> ( N - 1 ) = 0 )
28 27 fveq2d 
 |-  ( N = 1 -> ( F ` ( N - 1 ) ) = ( F ` 0 ) )
29 28 necon3i 
 |-  ( ( F ` ( N - 1 ) ) =/= ( F ` 0 ) -> N =/= 1 )
30 24 29 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> N =/= 1 )
31 eluz2b3 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ N =/= 1 ) )
32 20 30 31 sylanbrc 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> N e. ( ZZ>= ` 2 ) )