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∈−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 signsvtp ⊢φ∧0<A⁢B→V⁡F=V⁡E

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 ⊢φ∧0<A⁢B→V⁡F=V⁡E+ifT⁡E⁡E−1⁢A<010
16 0red ⊢φ∧0<A⁢B→0∈ℝ
17 5 adantr ⊢φ∧0<A⁢B→E∈Wordℝ∖∅
18 17 eldifad ⊢φ∧0<A⁢B→E∈Wordℝ
19 1 2 3 4 signstf ⊢E∈Wordℝ→T⁡E∈Wordℝ
20 wrdf ⊢T⁡E∈Wordℝ→T⁡E:0..^T⁡E⟶ℝ
21 18 19 20 3syl ⊢φ∧0<A⁢B→T⁡E:0..^T⁡E⟶ℝ
22 eldifsn ⊢E∈Wordℝ∖∅↔E∈Wordℝ∧E≠∅
23 5 22 sylib ⊢φ→E∈Wordℝ∧E≠∅
24 23 adantr ⊢φ∧0<A⁢B→E∈Wordℝ∧E≠∅
25 lennncl ⊢E∈Wordℝ∧E≠∅→E∈ℕ
26 fzo0end ⊢E∈ℕ→E−1∈0..^E
27 24 25 26 3syl ⊢φ∧0<A⁢B→E−1∈0..^E
28 1 2 3 4 signstlen ⊢E∈Wordℝ→T⁡E=E
29 18 28 syl ⊢φ∧0<A⁢B→T⁡E=E
30 29 oveq2d ⊢φ∧0<A⁢B→0..^T⁡E=0..^E
31 27 30 eleqtrrd ⊢φ∧0<A⁢B→E−1∈0..^T⁡E
32 21 31 ffvelcdmd ⊢φ∧0<A⁢B→T⁡E⁡E−1∈ℝ
33 8 adantr ⊢φ∧0<A⁢B→A∈ℝ
34 32 33 remulcld ⊢φ∧0<A⁢B→T⁡E⁡E−1⁢A∈ℝ
35 simpr ⊢φ∧0<A⁢B→0<A⁢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 ⊢φ∧0<A⁢B→B∈ℝ
40 39 recnd ⊢φ∧0<A⁢B→B∈ℂ
41 33 recnd ⊢φ∧0<A⁢B→A∈ℂ
42 40 41 mulcomd ⊢φ∧0<A⁢B→B⁢A=A⁢B
43 35 42 breqtrrd ⊢φ∧0<A⁢B→0<B⁢A
44 38 oveq1i ⊢B⁢A=T⁡E⁡E−1⁢A
45 43 44 breqtrdi ⊢φ∧0<A⁢B→0<T⁡E⁡E−1⁢A
46 16 34 45 ltnsymd ⊢φ∧0<A⁢B→¬T⁡E⁡E−1⁢A<0
47 46 iffalsed ⊢φ∧0<A⁢B→ifT⁡E⁡E−1⁢A<010=0
48 47 oveq2d ⊢φ∧0<A⁢B→V⁡E+ifT⁡E⁡E−1⁢A<010=V⁡E+0
49 1 2 3 4 signsvvf ⊢V:Wordℝ⟶ℕ0
50 49 a1i ⊢φ∧0<A⁢B→V:Wordℝ⟶ℕ0
51 50 18 ffvelcdmd ⊢φ∧0<A⁢B→V⁡E∈ℕ0
52 51 nn0cnd ⊢φ∧0<A⁢B→V⁡E∈ℂ
53 52 addridd ⊢φ∧0<A⁢B→V⁡E+0=V⁡E
54 15 48 53 3eqtrd ⊢φ∧0<A⁢B→V⁡F=V⁡E