Metamath Proof Explorer


Theorem signsvfpn

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 )
signsvf.b
|- B = ( E ` ( N - 1 ) )
Assertion signsvfpn
|- ( ( ph /\ 0 < ( B x. A ) ) -> ( 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 signsvf.b
 |-  B = ( E ` ( N - 1 ) )
11 8 recnd
 |-  ( ph -> A e. CC )
12 5 eldifad
 |-  ( ph -> E e. Word RR )
13 wrdf
 |-  ( E e. Word RR -> E : ( 0 ..^ ( # ` E ) ) --> RR )
14 12 13 syl
 |-  ( ph -> E : ( 0 ..^ ( # ` E ) ) --> RR )
15 9 oveq1i
 |-  ( N - 1 ) = ( ( # ` E ) - 1 )
16 eldifsn
 |-  ( E e. ( Word RR \ { (/) } ) <-> ( E e. Word RR /\ E =/= (/) ) )
17 5 16 sylib
 |-  ( ph -> ( E e. Word RR /\ E =/= (/) ) )
18 lennncl
 |-  ( ( E e. Word RR /\ E =/= (/) ) -> ( # ` E ) e. NN )
19 fzo0end
 |-  ( ( # ` E ) e. NN -> ( ( # ` E ) - 1 ) e. ( 0 ..^ ( # ` E ) ) )
20 17 18 19 3syl
 |-  ( ph -> ( ( # ` E ) - 1 ) e. ( 0 ..^ ( # ` E ) ) )
21 15 20 eqeltrid
 |-  ( ph -> ( N - 1 ) e. ( 0 ..^ ( # ` E ) ) )
22 14 21 ffvelrnd
 |-  ( ph -> ( E ` ( N - 1 ) ) e. RR )
23 22 recnd
 |-  ( ph -> ( E ` ( N - 1 ) ) e. CC )
24 10 23 eqeltrid
 |-  ( ph -> B e. CC )
25 11 24 mulcomd
 |-  ( ph -> ( A x. B ) = ( B x. A ) )
26 25 breq2d
 |-  ( ph -> ( 0 < ( A x. B ) <-> 0 < ( B x. A ) ) )
27 10 22 eqeltrid
 |-  ( ph -> B e. RR )
28 sgnmulsgp
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 < ( A x. B ) <-> 0 < ( ( sgn ` A ) x. ( sgn ` B ) ) ) )
29 8 27 28 syl2anc
 |-  ( ph -> ( 0 < ( A x. B ) <-> 0 < ( ( sgn ` A ) x. ( sgn ` B ) ) ) )
30 26 29 bitr3d
 |-  ( ph -> ( 0 < ( B x. A ) <-> 0 < ( ( sgn ` A ) x. ( sgn ` B ) ) ) )
31 30 biimpa
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> 0 < ( ( sgn ` A ) x. ( sgn ` B ) ) )
32 5 adantr
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> E e. ( Word RR \ { (/) } ) )
33 24 adantr
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> B e. CC )
34 11 adantr
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> A e. CC )
35 simpr
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> 0 < ( B x. A ) )
36 35 gt0ne0d
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( B x. A ) =/= 0 )
37 33 34 36 mulne0bad
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> B =/= 0 )
38 10 37 eqnetrrid
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( E ` ( N - 1 ) ) =/= 0 )
39 1 2 3 4 9 signsvtn0
 |-  ( ( E e. ( Word RR \ { (/) } ) /\ ( E ` ( N - 1 ) ) =/= 0 ) -> ( ( T ` E ) ` ( N - 1 ) ) = ( sgn ` ( E ` ( N - 1 ) ) ) )
40 10 fveq2i
 |-  ( sgn ` B ) = ( sgn ` ( E ` ( N - 1 ) ) )
41 39 40 eqtr4di
 |-  ( ( E e. ( Word RR \ { (/) } ) /\ ( E ` ( N - 1 ) ) =/= 0 ) -> ( ( T ` E ) ` ( N - 1 ) ) = ( sgn ` B ) )
42 32 38 41 syl2anc
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( ( T ` E ) ` ( N - 1 ) ) = ( sgn ` B ) )
43 42 fveq2d
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( sgn ` ( ( T ` E ) ` ( N - 1 ) ) ) = ( sgn ` ( sgn ` B ) ) )
44 27 adantr
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> B e. RR )
45 44 rexrd
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> B e. RR* )
46 sgnsgn
 |-  ( B e. RR* -> ( sgn ` ( sgn ` B ) ) = ( sgn ` B ) )
47 45 46 syl
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( sgn ` ( sgn ` B ) ) = ( sgn ` B ) )
48 43 47 eqtrd
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( sgn ` ( ( T ` E ) ` ( N - 1 ) ) ) = ( sgn ` B ) )
49 48 oveq2d
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( ( sgn ` A ) x. ( sgn ` ( ( T ` E ) ` ( N - 1 ) ) ) ) = ( ( sgn ` A ) x. ( sgn ` B ) ) )
50 31 49 breqtrrd
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> 0 < ( ( sgn ` A ) x. ( sgn ` ( ( T ` E ) ` ( N - 1 ) ) ) ) )
51 8 adantr
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> A e. RR )
52 sgnclre
 |-  ( B e. RR -> ( sgn ` B ) e. RR )
53 44 52 syl
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( sgn ` B ) e. RR )
54 42 53 eqeltrd
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( ( T ` E ) ` ( N - 1 ) ) e. RR )
55 sgnmulsgp
 |-  ( ( A e. RR /\ ( ( T ` E ) ` ( N - 1 ) ) e. RR ) -> ( 0 < ( A x. ( ( T ` E ) ` ( N - 1 ) ) ) <-> 0 < ( ( sgn ` A ) x. ( sgn ` ( ( T ` E ) ` ( N - 1 ) ) ) ) ) )
56 51 54 55 syl2anc
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( 0 < ( A x. ( ( T ` E ) ` ( N - 1 ) ) ) <-> 0 < ( ( sgn ` A ) x. ( sgn ` ( ( T ` E ) ` ( N - 1 ) ) ) ) ) )
57 50 56 mpbird
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> 0 < ( A x. ( ( T ` E ) ` ( N - 1 ) ) ) )
58 eqid
 |-  ( ( T ` E ) ` ( N - 1 ) ) = ( ( T ` E ) ` ( N - 1 ) )
59 1 2 3 4 5 6 7 8 9 58 signsvtp
 |-  ( ( ph /\ 0 < ( A x. ( ( T ` E ) ` ( N - 1 ) ) ) ) -> ( V ` F ) = ( V ` E ) )
60 57 59 syldan
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( V ` F ) = ( V ` E ) )