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∈−101,b∈−101⟼ifb=0ab
signsv.w ⊢W=Basendx−101+ndx⨣˙
signsv.t ⊢T=f∈Wordℝ⟼n∈0..^f⟼∑Wi=0nsgn⁡f⁡i
signsv.v ⊢V=f∈Wordℝ⟼∑j∈1..^fifT⁡f⁡j≠T⁡f⁡j−110
signsvf.e ⊢φ→E∈Wordℝ∖∅
signsvf.0 ⊢φ→E⁡0≠0
signsvf.f ⊢φ→F=E++⟨“A”⟩
signsvf.a ⊢φ→A∈ℝ
signsvf.n ⊢N=E
signsvt.b ⊢B=T⁡E⁡N−1
Assertion signsvtn ⊢φ∧A⁢B<0→V⁡F−V⁡E=1

Proof

Step Hyp Ref Expression
1 signsv.p ⊢⨣˙=a∈−101,b∈−101⟼ifb=0ab
2 signsv.w ⊢W=Basendx−101+ndx⨣˙
3 signsv.t ⊢T=f∈Wordℝ⟼n∈0..^f⟼∑Wi=0nsgn⁡f⁡i
4 signsv.v ⊢V=f∈Wordℝ⟼∑j∈1..^fifT⁡f⁡j≠T⁡f⁡j−110
5 signsvf.e ⊢φ→E∈Wordℝ∖∅
6 signsvf.0 ⊢φ→E⁡0≠0
7 signsvf.f ⊢φ→F=E++⟨“A”⟩
8 signsvf.a ⊢φ→A∈ℝ
9 signsvf.n ⊢N=E
10 signsvt.b ⊢B=T⁡E⁡N−1
11 7 fveq2d ⊢φ→V⁡F=V⁡E++⟨“A”⟩
12 1 2 3 4 signsvfn ⊢E∈Wordℝ∖∅∧E⁡0≠0∧A∈ℝ→V⁡E++⟨“A”⟩=V⁡E+ifT⁡E⁡E−1⁢A<010
13 5 6 8 12 syl21anc ⊢φ→V⁡E++⟨“A”⟩=V⁡E+ifT⁡E⁡E−1⁢A<010
14 11 13 eqtrd ⊢φ→V⁡F=V⁡E+ifT⁡E⁡E−1⁢A<010
15 14 adantr ⊢φ∧A⁢B<0→V⁡F=V⁡E+ifT⁡E⁡E−1⁢A<010
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⁢A=T⁡E⁡E−1⁢A
20 5 adantr ⊢φ∧A⁢B<0→E∈Wordℝ∖∅
21 20 eldifad ⊢φ∧A⁢B<0→E∈Wordℝ
22 1 2 3 4 signstf ⊢E∈Wordℝ→T⁡E∈Wordℝ
23 wrdf ⊢T⁡E∈Wordℝ→T⁡E:0..^T⁡E⟶ℝ
24 21 22 23 3syl ⊢φ∧A⁢B<0→T⁡E:0..^T⁡E⟶ℝ
25 eldifsn ⊢E∈Wordℝ∖∅↔E∈Wordℝ∧E≠∅
26 5 25 sylib ⊢φ→E∈Wordℝ∧E≠∅
27 26 adantr ⊢φ∧A⁢B<0→E∈Wordℝ∧E≠∅
28 lennncl ⊢E∈Wordℝ∧E≠∅→E∈ℕ
29 fzo0end ⊢E∈ℕ→E−1∈0..^E
30 27 28 29 3syl ⊢φ∧A⁢B<0→E−1∈0..^E
31 1 2 3 4 signstlen ⊢E∈Wordℝ→T⁡E=E
32 21 31 syl ⊢φ∧A⁢B<0→T⁡E=E
33 32 oveq2d ⊢φ∧A⁢B<0→0..^T⁡E=0..^E
34 30 33 eleqtrrd ⊢φ∧A⁢B<0→E−1∈0..^T⁡E
35 24 34 ffvelcdmd ⊢φ∧A⁢B<0→T⁡E⁡E−1∈ℝ
36 18 35 eqeltrid ⊢φ∧A⁢B<0→B∈ℝ
37 36 recnd ⊢φ∧A⁢B<0→B∈ℂ
38 8 adantr ⊢φ∧A⁢B<0→A∈ℝ
39 38 recnd ⊢φ∧A⁢B<0→A∈ℂ
40 37 39 mulcomd ⊢φ∧A⁢B<0→B⁢A=A⁢B
41 simpr ⊢φ∧A⁢B<0→A⁢B<0
42 40 41 eqbrtrd ⊢φ∧A⁢B<0→B⁢A<0
43 19 42 eqbrtrrid ⊢φ∧A⁢B<0→T⁡E⁡E−1⁢A<0
44 43 iftrued ⊢φ∧A⁢B<0→ifT⁡E⁡E−1⁢A<010=1
45 44 oveq2d ⊢φ∧A⁢B<0→V⁡E+ifT⁡E⁡E−1⁢A<010=V⁡E+1
46 15 45 eqtr2d ⊢φ∧A⁢B<0→V⁡E+1=V⁡F
47 1 2 3 4 signsvvf ⊢V:Wordℝ⟶ℕ0
48 47 a1i ⊢φ∧A⁢B<0→V:Wordℝ⟶ℕ0
49 7 adantr ⊢φ∧A⁢B<0→F=E++⟨“A”⟩
50 38 s1cld ⊢φ∧A⁢B<0→⟨“A”⟩∈Wordℝ
51 ccatcl ⊢E∈Wordℝ∧⟨“A”⟩∈Wordℝ→E++⟨“A”⟩∈Wordℝ
52 21 50 51 syl2anc ⊢φ∧A⁢B<0→E++⟨“A”⟩∈Wordℝ
53 49 52 eqeltrd ⊢φ∧A⁢B<0→F∈Wordℝ
54 48 53 ffvelcdmd ⊢φ∧A⁢B<0→V⁡F∈ℕ0
55 54 nn0cnd ⊢φ∧A⁢B<0→V⁡F∈ℂ
56 48 21 ffvelcdmd ⊢φ∧A⁢B<0→V⁡E∈ℕ0
57 56 nn0cnd ⊢φ∧A⁢B<0→V⁡E∈ℂ
58 1cnd ⊢φ∧A⁢B<0→1∈ℂ
59 55 57 58 subaddd ⊢φ∧A⁢B<0→V⁡F−V⁡E=1↔V⁡E+1=V⁡F
60 46 59 mpbird ⊢φ∧A⁢B<0→V⁡F−V⁡E=1