Metamath Proof Explorer

Theorem signsvtn

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 )
signsvt.b 
|- B = ( ( T ` E ) ` ( N - 1 ) )
Assertion signsvtn 
|- ( ( ph /\ ( A x. B ) < 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 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 /\ ( A x. B ) < 0 ) -> ( V ` F ) = ( ( V ` E ) + if ( ( ( ( T ` E ) ` ( ( # ` E ) - 1 ) ) x. A ) < 0 , 1 , 0 ) ) )
16 9 oveq1i 
 |-  ( N - 1 ) = ( ( # ` E ) - 1 )
17 16 fveq2i 
 |-  ( ( T ` E ) ` ( N - 1 ) ) = ( ( T ` E ) ` ( ( # ` E ) - 1 ) )
18 10 17 eqtri 
 |-  B = ( ( T ` E ) ` ( ( # ` E ) - 1 ) )
19 18 oveq1i 
 |-  ( B x. A ) = ( ( ( T ` E ) ` ( ( # ` E ) - 1 ) ) x. A )
20 5 adantr 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> E e. ( Word RR \ { (/) } ) )
21 20 eldifad 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> E e. Word RR )
22 1 2 3 4 signstf 
 |-  ( E e. Word RR -> ( T ` E ) e. Word RR )
23 wrdf 
 |-  ( ( T ` E ) e. Word RR -> ( T ` E ) : ( 0 ..^ ( # ` ( T ` E ) ) ) --> RR )
24 21 22 23 3syl 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( T ` E ) : ( 0 ..^ ( # ` ( T ` E ) ) ) --> RR )
25 eldifsn 
 |-  ( E e. ( Word RR \ { (/) } ) <-> ( E e. Word RR /\ E =/= (/) ) )
26 5 25 sylib 
 |-  ( ph -> ( E e. Word RR /\ E =/= (/) ) )
27 26 adantr 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( E e. Word RR /\ E =/= (/) ) )
28 lennncl 
 |-  ( ( E e. Word RR /\ E =/= (/) ) -> ( # ` E ) e. NN )
29 fzo0end 
 |-  ( ( # ` E ) e. NN -> ( ( # ` E ) - 1 ) e. ( 0 ..^ ( # ` E ) ) )
30 27 28 29 3syl 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( ( # ` E ) - 1 ) e. ( 0 ..^ ( # ` E ) ) )
31 1 2 3 4 signstlen 
 |-  ( E e. Word RR -> ( # ` ( T ` E ) ) = ( # ` E ) )
32 21 31 syl 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( # ` ( T ` E ) ) = ( # ` E ) )
33 32 oveq2d 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( 0 ..^ ( # ` ( T ` E ) ) ) = ( 0 ..^ ( # ` E ) ) )
34 30 33 eleqtrrd 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( ( # ` E ) - 1 ) e. ( 0 ..^ ( # ` ( T ` E ) ) ) )
35 24 34 ffvelrnd 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( ( T ` E ) ` ( ( # ` E ) - 1 ) ) e. RR )
36 18 35 eqeltrid 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> B e. RR )
37 36 recnd 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> B e. CC )
38 8 adantr 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> A e. RR )
39 38 recnd 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> A e. CC )
40 37 39 mulcomd 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( B x. A ) = ( A x. B ) )
41 simpr 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( A x. B ) < 0 )
42 40 41 eqbrtrd 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( B x. A ) < 0 )
43 19 42 eqbrtrrid 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( ( ( T ` E ) ` ( ( # ` E ) - 1 ) ) x. A ) < 0 )
44 43 iftrued 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> if ( ( ( ( T ` E ) ` ( ( # ` E ) - 1 ) ) x. A ) < 0 , 1 , 0 ) = 1 )
45 44 oveq2d 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( ( V ` E ) + if ( ( ( ( T ` E ) ` ( ( # ` E ) - 1 ) ) x. A ) < 0 , 1 , 0 ) ) = ( ( V ` E ) + 1 ) )
46 15 45 eqtr2d 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( ( V ` E ) + 1 ) = ( V ` F ) )
47 1 2 3 4 signsvvf 
 |-  V : Word RR --> NN0
48 47 a1i 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> V : Word RR --> NN0 )
49 7 adantr 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> F = ( E ++ <" A "> ) )
50 38 s1cld 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> <" A "> e. Word RR )
51 ccatcl 
 |-  ( ( E e. Word RR /\ <" A "> e. Word RR ) -> ( E ++ <" A "> ) e. Word RR )
52 21 50 51 syl2anc 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( E ++ <" A "> ) e. Word RR )
53 49 52 eqeltrd 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> F e. Word RR )
54 48 53 ffvelrnd 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( V ` F ) e. NN0 )
55 54 nn0cnd 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( V ` F ) e. CC )
56 48 21 ffvelrnd 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( V ` E ) e. NN0 )
57 56 nn0cnd 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( V ` E ) e. CC )
58 1cnd 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> 1 e. CC )
59 55 57 58 subaddd 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( ( ( V ` F ) - ( V ` E ) ) = 1 <-> ( ( V ` E ) + 1 ) = ( V ` F ) ) )
60 46 59 mpbird 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( ( V ` F ) - ( V ` E ) ) = 1 )