Metamath Proof Explorer


Theorem signsvtp

Description: Adding a letter of the same sign as the highest coefficient does not change the sign. (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 ) )
signsvf.e
|- ( ph -> E e. ( Word RR \ { (/) } ) )
signsvf.0
|- ( ph -> ( E ` 0 ) =/= 0 )
signsvf.f
|- ( ph -> F = ( E ++ <" A "> ) )
signsvf.a
|- ( ph -> A e. RR )
signsvf.n
|- N = ( # ` E )
signsvt.b
|- B = ( ( T ` E ) ` ( N - 1 ) )
Assertion signsvtp
|- ( ( ph /\ 0 < ( A x. B ) ) -> ( V ` F ) = ( V ` E ) )

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 signsvf.e
 |-  ( ph -> E e. ( Word RR \ { (/) } ) )
6 signsvf.0
 |-  ( ph -> ( E ` 0 ) =/= 0 )
7 signsvf.f
 |-  ( ph -> F = ( E ++ <" A "> ) )
8 signsvf.a
 |-  ( ph -> A e. RR )
9 signsvf.n
 |-  N = ( # ` E )
10 signsvt.b
 |-  B = ( ( T ` E ) ` ( N - 1 ) )
11 7 fveq2d
 |-  ( ph -> ( V ` F ) = ( V ` ( E ++ <" A "> ) ) )
12 1 2 3 4 signsvfn
 |-  ( ( ( E e. ( Word RR \ { (/) } ) /\ ( E ` 0 ) =/= 0 ) /\ A e. RR ) -> ( V ` ( E ++ <" A "> ) ) = ( ( V ` E ) + if ( ( ( ( T ` E ) ` ( ( # ` E ) - 1 ) ) x. A ) < 0 , 1 , 0 ) ) )
13 5 6 8 12 syl21anc
 |-  ( ph -> ( V ` ( E ++ <" A "> ) ) = ( ( V ` E ) + if ( ( ( ( T ` E ) ` ( ( # ` E ) - 1 ) ) x. A ) < 0 , 1 , 0 ) ) )
14 11 13 eqtrd
 |-  ( ph -> ( V ` F ) = ( ( V ` E ) + if ( ( ( ( T ` E ) ` ( ( # ` E ) - 1 ) ) x. A ) < 0 , 1 , 0 ) ) )
15 14 adantr
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( V ` F ) = ( ( V ` E ) + if ( ( ( ( T ` E ) ` ( ( # ` E ) - 1 ) ) x. A ) < 0 , 1 , 0 ) ) )
16 0red
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> 0 e. RR )
17 5 adantr
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> E e. ( Word RR \ { (/) } ) )
18 17 eldifad
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> E e. Word RR )
19 1 2 3 4 signstf
 |-  ( E e. Word RR -> ( T ` E ) e. Word RR )
20 wrdf
 |-  ( ( T ` E ) e. Word RR -> ( T ` E ) : ( 0 ..^ ( # ` ( T ` E ) ) ) --> RR )
21 18 19 20 3syl
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( T ` E ) : ( 0 ..^ ( # ` ( T ` E ) ) ) --> RR )
22 eldifsn
 |-  ( E e. ( Word RR \ { (/) } ) <-> ( E e. Word RR /\ E =/= (/) ) )
23 5 22 sylib
 |-  ( ph -> ( E e. Word RR /\ E =/= (/) ) )
24 23 adantr
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( E e. Word RR /\ E =/= (/) ) )
25 lennncl
 |-  ( ( E e. Word RR /\ E =/= (/) ) -> ( # ` E ) e. NN )
26 fzo0end
 |-  ( ( # ` E ) e. NN -> ( ( # ` E ) - 1 ) e. ( 0 ..^ ( # ` E ) ) )
27 24 25 26 3syl
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( ( # ` E ) - 1 ) e. ( 0 ..^ ( # ` E ) ) )
28 1 2 3 4 signstlen
 |-  ( E e. Word RR -> ( # ` ( T ` E ) ) = ( # ` E ) )
29 18 28 syl
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( # ` ( T ` E ) ) = ( # ` E ) )
30 29 oveq2d
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( 0 ..^ ( # ` ( T ` E ) ) ) = ( 0 ..^ ( # ` E ) ) )
31 27 30 eleqtrrd
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( ( # ` E ) - 1 ) e. ( 0 ..^ ( # ` ( T ` E ) ) ) )
32 21 31 ffvelrnd
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( ( T ` E ) ` ( ( # ` E ) - 1 ) ) e. RR )
33 8 adantr
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> A e. RR )
34 32 33 remulcld
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( ( ( T ` E ) ` ( ( # ` E ) - 1 ) ) x. A ) e. RR )
35 simpr
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> 0 < ( A x. B ) )
36 9 oveq1i
 |-  ( N - 1 ) = ( ( # ` E ) - 1 )
37 36 fveq2i
 |-  ( ( T ` E ) ` ( N - 1 ) ) = ( ( T ` E ) ` ( ( # ` E ) - 1 ) )
38 10 37 eqtri
 |-  B = ( ( T ` E ) ` ( ( # ` E ) - 1 ) )
39 38 32 eqeltrid
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> B e. RR )
40 39 recnd
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> B e. CC )
41 33 recnd
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> A e. CC )
42 40 41 mulcomd
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( B x. A ) = ( A x. B ) )
43 35 42 breqtrrd
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> 0 < ( B x. A ) )
44 38 oveq1i
 |-  ( B x. A ) = ( ( ( T ` E ) ` ( ( # ` E ) - 1 ) ) x. A )
45 43 44 breqtrdi
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> 0 < ( ( ( T ` E ) ` ( ( # ` E ) - 1 ) ) x. A ) )
46 16 34 45 ltnsymd
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> -. ( ( ( T ` E ) ` ( ( # ` E ) - 1 ) ) x. A ) < 0 )
47 46 iffalsed
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> if ( ( ( ( T ` E ) ` ( ( # ` E ) - 1 ) ) x. A ) < 0 , 1 , 0 ) = 0 )
48 47 oveq2d
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( ( V ` E ) + if ( ( ( ( T ` E ) ` ( ( # ` E ) - 1 ) ) x. A ) < 0 , 1 , 0 ) ) = ( ( V ` E ) + 0 ) )
49 1 2 3 4 signsvvf
 |-  V : Word RR --> NN0
50 49 a1i
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> V : Word RR --> NN0 )
51 50 18 ffvelrnd
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( V ` E ) e. NN0 )
52 51 nn0cnd
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( V ` E ) e. CC )
53 52 addid1d
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( ( V ` E ) + 0 ) = ( V ` E ) )
54 15 48 53 3eqtrd
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( V ` F ) = ( V ` E ) )