Metamath Proof Explorer

Theorem signlem0

Description: Adding a zero as the highest coefficient does not change the parity of the sign changes. (Contributed by Thierry Arnoux, 12-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 ) )
Assertion signlem0 
|- ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) -> ( V ` ( F ++ <" 0 "> ) ) = ( V ` F ) )

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 0re 
 |-  0 e. RR
6 1 2 3 4 signsvfn 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ 0 e. RR ) -> ( V ` ( F ++ <" 0 "> ) ) = ( ( V ` F ) + if ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. 0 ) < 0 , 1 , 0 ) ) )
7 5 6 mpan2 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) -> ( V ` ( F ++ <" 0 "> ) ) = ( ( V ` F ) + if ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. 0 ) < 0 , 1 , 0 ) ) )
8 5 ltnri 
 |-  -. 0 < 0
9 neg1cn 
 |-  -u 1 e. CC
10 ax-1cn 
 |-  1 e. CC
11 prssi 
 |-  ( ( -u 1 e. CC /\ 1 e. CC ) -> { -u 1 , 1 } C_ CC )
12 9 10 11 mp2an 
 |-  { -u 1 , 1 } C_ CC
13 simpl 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) -> F e. ( Word RR \ { (/) } ) )
14 eldifsn 
 |-  ( F e. ( Word RR \ { (/) } ) <-> ( F e. Word RR /\ F =/= (/) ) )
15 13 14 sylib 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) -> ( F e. Word RR /\ F =/= (/) ) )
16 lennncl 
 |-  ( ( F e. Word RR /\ F =/= (/) ) -> ( # ` F ) e. NN )
17 fzo0end 
 |-  ( ( # ` F ) e. NN -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
18 15 16 17 3syl 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
19 1 2 3 4 signstfvcl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) e. { -u 1 , 1 } )
20 18 19 mpdan 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) -> ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) e. { -u 1 , 1 } )
21 12 20 sselid 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) -> ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) e. CC )
22 21 mul01d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) -> ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. 0 ) = 0 )
23 22 breq1d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) -> ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. 0 ) < 0 <-> 0 < 0 ) )
24 8 23 mtbiri 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) -> -. ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. 0 ) < 0 )
25 24 iffalsed 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) -> if ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. 0 ) < 0 , 1 , 0 ) = 0 )
26 25 oveq2d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) -> ( ( V ` F ) + if ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. 0 ) < 0 , 1 , 0 ) ) = ( ( V ` F ) + 0 ) )
27 1 2 3 4 signsvvf 
 |-  V : Word RR --> NN0
28 27 a1i 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) -> V : Word RR --> NN0 )
29 13 eldifad 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) -> F e. Word RR )
30 28 29 ffvelrnd 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) -> ( V ` F ) e. NN0 )
31 30 nn0cnd 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) -> ( V ` F ) e. CC )
32 31 addid1d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) -> ( ( V ` F ) + 0 ) = ( V ` F ) )
33 7 26 32 3eqtrd 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) -> ( V ` ( F ++ <" 0 "> ) ) = ( V ` F ) )