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 ∈ − 1 0 1 , b ∈ − 1 0 1 ⟼ if b = 0 a b
signsv.w ⊢ W = Base ndx − 1 0 1 + ndx ⨣ ˙
signsv.t ⊢ T = f ∈ Word ℝ ⟼ n ∈ 0 ..^ f ⟼ ∑ W i = 0 n sgn ⁡ f ⁡ i
signsv.v ⊢ V = f ∈ Word ℝ ⟼ ∑ j ∈ 1 ..^ f if T ⁡ f ⁡ j ≠ T ⁡ f ⁡ j − 1 1 0
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 ∈ − 1 0 1 , b ∈ − 1 0 1 ⟼ if b = 0 a b
2 signsv.w ⊢ W = Base ndx − 1 0 1 + ndx ⨣ ˙
3 signsv.t ⊢ T = f ∈ Word ℝ ⟼ n ∈ 0 ..^ f ⟼ ∑ W i = 0 n sgn ⁡ f ⁡ i
4 signsv.v ⊢ V = f ∈ Word ℝ ⟼ ∑ j ∈ 1 ..^ f if T ⁡ f ⁡ j ≠ T ⁡ f ⁡ j − 1 1 0
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 + if T ⁡ E ⁡ E − 1 ⁢ A < 0 1 0
13 5 6 8 12 syl21anc ⊢ φ → V ⁡ E ++ ⟨“ A ”⟩ = V ⁡ E + if T ⁡ E ⁡ E − 1 ⁢ A < 0 1 0
14 11 13 eqtrd ⊢ φ → V ⁡ F = V ⁡ E + if T ⁡ E ⁡ E − 1 ⁢ A < 0 1 0
15 14 adantr ⊢ φ ∧ 0 < A ⁢ B → V ⁡ F = V ⁡ E + if T ⁡ E ⁡ E − 1 ⁢ A < 0 1 0
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 → if T ⁡ E ⁡ E − 1 ⁢ A < 0 1 0 = 0
48 47 oveq2d ⊢ φ ∧ 0 < A ⁢ B → V ⁡ E + if T ⁡ E ⁡ E − 1 ⁢ A < 0 1 0 = 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