Metamath Proof Explorer

Theorem signsvfnn

Description: Adding a letter of a different sign as the highest coefficient changes 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 signsvfnn 
|- ( ( ph /\ ( B x. A ) < 0 ) -> ( ( V ` F ) - ( V ` E ) ) = 1 )

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 5 adantr 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> E e. ( Word RR \ { (/) } ) )
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 24 adantr 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> B e. CC )
26 8 recnd 
 |-  ( ph -> A e. CC )
27 26 adantr 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> A e. CC )
28 simpr 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> ( B x. A ) < 0 )
29 28 lt0ne0d 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> ( B x. A ) =/= 0 )
30 25 27 29 mulne0bad 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> B =/= 0 )
31 10 30 eqnetrrid 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> ( E ` ( N - 1 ) ) =/= 0 )
32 1 2 3 4 9 signsvtn0 
 |-  ( ( E e. ( Word RR \ { (/) } ) /\ ( E ` ( N - 1 ) ) =/= 0 ) -> ( ( T ` E ) ` ( N - 1 ) ) = ( sgn ` ( E ` ( N - 1 ) ) ) )
33 10 fveq2i 
 |-  ( sgn ` B ) = ( sgn ` ( E ` ( N - 1 ) ) )
34 32 33 eqtr4di 
 |-  ( ( E e. ( Word RR \ { (/) } ) /\ ( E ` ( N - 1 ) ) =/= 0 ) -> ( ( T ` E ) ` ( N - 1 ) ) = ( sgn ` B ) )
35 11 31 34 syl2anc 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> ( ( T ` E ) ` ( N - 1 ) ) = ( sgn ` B ) )
36 35 fveq2d 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> ( sgn ` ( ( T ` E ) ` ( N - 1 ) ) ) = ( sgn ` ( sgn ` B ) ) )
37 10 22 eqeltrid 
 |-  ( ph -> B e. RR )
38 37 adantr 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> B e. RR )
39 38 rexrd 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> B e. RR* )
40 sgnsgn 
 |-  ( B e. RR* -> ( sgn ` ( sgn ` B ) ) = ( sgn ` B ) )
41 39 40 syl 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> ( sgn ` ( sgn ` B ) ) = ( sgn ` B ) )
42 36 41 eqtrd 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> ( sgn ` ( ( T ` E ) ` ( N - 1 ) ) ) = ( sgn ` B ) )
43 42 oveq2d 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> ( ( sgn ` A ) x. ( sgn ` ( ( T ` E ) ` ( N - 1 ) ) ) ) = ( ( sgn ` A ) x. ( sgn ` B ) ) )
44 26 24 mulcomd 
 |-  ( ph -> ( A x. B ) = ( B x. A ) )
45 44 breq1d 
 |-  ( ph -> ( ( A x. B ) < 0 <-> ( B x. A ) < 0 ) )
46 sgnmulsgn 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A x. B ) < 0 <-> ( ( sgn ` A ) x. ( sgn ` B ) ) < 0 ) )
47 8 37 46 syl2anc 
 |-  ( ph -> ( ( A x. B ) < 0 <-> ( ( sgn ` A ) x. ( sgn ` B ) ) < 0 ) )
48 45 47 bitr3d 
 |-  ( ph -> ( ( B x. A ) < 0 <-> ( ( sgn ` A ) x. ( sgn ` B ) ) < 0 ) )
49 48 biimpa 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> ( ( sgn ` A ) x. ( sgn ` B ) ) < 0 )
50 43 49 eqbrtrd 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> ( ( sgn ` A ) x. ( sgn ` ( ( T ` E ) ` ( N - 1 ) ) ) ) < 0 )
51 8 adantr 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> A e. RR )
52 sgnclre 
 |-  ( B e. RR -> ( sgn ` B ) e. RR )
53 38 52 syl 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> ( sgn ` B ) e. RR )
54 35 53 eqeltrd 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> ( ( T ` E ) ` ( N - 1 ) ) e. RR )
55 sgnmulsgn 
 |-  ( ( A e. RR /\ ( ( T ` E ) ` ( N - 1 ) ) e. RR ) -> ( ( A x. ( ( T ` E ) ` ( N - 1 ) ) ) < 0 <-> ( ( sgn ` A ) x. ( sgn ` ( ( T ` E ) ` ( N - 1 ) ) ) ) < 0 ) )
56 51 54 55 syl2anc 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> ( ( A x. ( ( T ` E ) ` ( N - 1 ) ) ) < 0 <-> ( ( sgn ` A ) x. ( sgn ` ( ( T ` E ) ` ( N - 1 ) ) ) ) < 0 ) )
57 50 56 mpbird 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> ( A x. ( ( T ` E ) ` ( N - 1 ) ) ) < 0 )
58 eqid 
 |-  ( ( T ` E ) ` ( N - 1 ) ) = ( ( T ` E ) ` ( N - 1 ) )
59 1 2 3 4 5 6 7 8 9 58 signsvtn 
 |-  ( ( ph /\ ( A x. ( ( T ` E ) ` ( N - 1 ) ) ) < 0 ) -> ( ( V ` F ) - ( V ` E ) ) = 1 )
60 57 59 syldan 
 |-  ( ( ph /\ ( B x. A ) < 0 ) -> ( ( V ` F ) - ( V ` E ) ) = 1 )