signsvfpn

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	$⊢ \underset{˙}{⨣} = (a \in \{- 1, 0, 1\}, b \in \{- 1, 0, 1\} ⟼ if (b = 0, a, b))$
	signsv.w	$⊢ W = \{⟨{Base}_{ndx}, \{- 1, 0, 1\}⟩, ⟨+_{ndx}, \underset{˙}{⨣}⟩\}$
	signsv.t	$⊢ T = (f \in Word ℝ ⟼ (n \in (0 ..^\|f\|) ⟼ {\sum_{W}}_{i = 0}^{n} sgn (f (i))))$
	signsv.v	$⊢ V = (f \in Word ℝ ⟼ \sum_{j \in (1 ..^\|f\|)} if (T (f) (j) \neq T (f) (j - 1), 1, 0))$
	signsvf.e	$⊢ φ \to E \in (Word ℝ ∖ \{\emptyset\})$
	signsvf.0	$⊢ φ \to E (0) \neq 0$
	signsvf.f	$⊢ φ \to F = E ++ ⟨“ A ”⟩$
	signsvf.a	$⊢ φ \to A \in ℝ$
	signsvf.n	$⊢ N = \|E\|$
	signsvf.b	$⊢ B = E (N - 1)$
Assertion	signsvfpn	$⊢ (φ \land 0 < B A) \to V (F) = V (E)$

Proof

Step	Hyp	Ref	Expression
1		signsv.p	$⊢ \underset{˙}{⨣} = (a \in \{- 1, 0, 1\}, b \in \{- 1, 0, 1\} ⟼ if (b = 0, a, b))$
2		signsv.w	$⊢ W = \{⟨{Base}_{ndx}, \{- 1, 0, 1\}⟩, ⟨+_{ndx}, \underset{˙}{⨣}⟩\}$
3		signsv.t	$⊢ T = (f \in Word ℝ ⟼ (n \in (0 ..^\|f\|) ⟼ {\sum_{W}}_{i = 0}^{n} sgn (f (i))))$
4		signsv.v	$⊢ V = (f \in Word ℝ ⟼ \sum_{j \in (1 ..^\|f\|)} if (T (f) (j) \neq T (f) (j - 1), 1, 0))$
5		signsvf.e	$⊢ φ \to E \in (Word ℝ ∖ \{\emptyset\})$
6		signsvf.0	$⊢ φ \to E (0) \neq 0$
7		signsvf.f	$⊢ φ \to F = E ++ ⟨“ A ”⟩$
8		signsvf.a	$⊢ φ \to A \in ℝ$
9		signsvf.n	$⊢ N = \|E\|$
10		signsvf.b	$⊢ B = E (N - 1)$
11	8	recnd	$⊢ φ \to A \in ℂ$
12	5	eldifad	$⊢ φ \to E \in Word ℝ$
13		wrdf	$⊢ E \in Word ℝ \to E : (0 ..^\|E\|) ⟶ ℝ$
14	12 13	syl	$⊢ φ \to E : (0 ..^\|E\|) ⟶ ℝ$
15	9	oveq1i	$⊢ N - 1 = \|E\| - 1$
16		eldifsn	$⊢ E \in (Word ℝ ∖ \{\emptyset\}) \leftrightarrow (E \in Word ℝ \land E \neq \emptyset)$
17	5 16	sylib	$⊢ φ \to (E \in Word ℝ \land E \neq \emptyset)$
18		lennncl	$⊢ (E \in Word ℝ \land E \neq \emptyset) \to \|E\| \in ℕ$
19		fzo0end	$⊢ \|E\| \in ℕ \to \|E\| - 1 \in (0 ..^\|E\|)$
20	17 18 19	3syl	$⊢ φ \to \|E\| - 1 \in (0 ..^\|E\|)$
21	15 20	eqeltrid	$⊢ φ \to N - 1 \in (0 ..^\|E\|)$
22	14 21	ffvelcdmd	$⊢ φ \to E (N - 1) \in ℝ$
23	22	recnd	$⊢ φ \to E (N - 1) \in ℂ$
24	10 23	eqeltrid	$⊢ φ \to B \in ℂ$
25	11 24	mulcomd	$⊢ φ \to A B = B A$
26	25	breq2d	$⊢ φ \to (0 < A B \leftrightarrow 0 < B A)$
27	10 22	eqeltrid	$⊢ φ \to B \in ℝ$
28		sgnmulsgp	$⊢ (A \in ℝ \land B \in ℝ) \to (0 < A B \leftrightarrow 0 < sgn (A) sgn (B))$
29	8 27 28	syl2anc	$⊢ φ \to (0 < A B \leftrightarrow 0 < sgn (A) sgn (B))$
30	26 29	bitr3d	$⊢ φ \to (0 < B A \leftrightarrow 0 < sgn (A) sgn (B))$
31	30	biimpa	$⊢ (φ \land 0 < B A) \to 0 < sgn (A) sgn (B)$
32	5	adantr	$⊢ (φ \land 0 < B A) \to E \in (Word ℝ ∖ \{\emptyset\})$
33	24	adantr	$⊢ (φ \land 0 < B A) \to B \in ℂ$
34	11	adantr	$⊢ (φ \land 0 < B A) \to A \in ℂ$
35		simpr	$⊢ (φ \land 0 < B A) \to 0 < B A$
36	35	gt0ne0d	$⊢ (φ \land 0 < B A) \to B A \neq 0$
37	33 34 36	mulne0bad	$⊢ (φ \land 0 < B A) \to B \neq 0$
38	10 37	eqnetrrid	$⊢ (φ \land 0 < B A) \to E (N - 1) \neq 0$
39	1 2 3 4 9	signsvtn0	$⊢ (E \in (Word ℝ ∖ \{\emptyset\}) \land E (N - 1) \neq 0) \to T (E) (N - 1) = sgn (E (N - 1))$
40	10	fveq2i	$⊢ sgn (B) = sgn (E (N - 1))$
41	39 40	eqtr4di	$⊢ (E \in (Word ℝ ∖ \{\emptyset\}) \land E (N - 1) \neq 0) \to T (E) (N - 1) = sgn (B)$
42	32 38 41	syl2anc	$⊢ (φ \land 0 < B A) \to T (E) (N - 1) = sgn (B)$
43	42	fveq2d	$⊢ (φ \land 0 < B A) \to sgn (T (E) (N - 1)) = sgn (sgn (B))$
44	27	adantr	$⊢ (φ \land 0 < B A) \to B \in ℝ$
45	44	rexrd	$⊢ (φ \land 0 < B A) \to B \in ℝ^{*}$
46		sgnsgn	$⊢ B \in ℝ^{*} \to sgn (sgn (B)) = sgn (B)$
47	45 46	syl	$⊢ (φ \land 0 < B A) \to sgn (sgn (B)) = sgn (B)$
48	43 47	eqtrd	$⊢ (φ \land 0 < B A) \to sgn (T (E) (N - 1)) = sgn (B)$
49	48	oveq2d	$⊢ (φ \land 0 < B A) \to sgn (A) sgn (T (E) (N - 1)) = sgn (A) sgn (B)$
50	31 49	breqtrrd	$⊢ (φ \land 0 < B A) \to 0 < sgn (A) sgn (T (E) (N - 1))$
51	8	adantr	$⊢ (φ \land 0 < B A) \to A \in ℝ$
52		sgnclre	$⊢ B \in ℝ \to sgn (B) \in ℝ$
53	44 52	syl	$⊢ (φ \land 0 < B A) \to sgn (B) \in ℝ$
54	42 53	eqeltrd	$⊢ (φ \land 0 < B A) \to T (E) (N - 1) \in ℝ$
55		sgnmulsgp	$⊢ (A \in ℝ \land T (E) (N - 1) \in ℝ) \to (0 < A T (E) (N - 1) \leftrightarrow 0 < sgn (A) sgn (T (E) (N - 1)))$
56	51 54 55	syl2anc	$⊢ (φ \land 0 < B A) \to (0 < A T (E) (N - 1) \leftrightarrow 0 < sgn (A) sgn (T (E) (N - 1)))$
57	50 56	mpbird	$⊢ (φ \land 0 < B A) \to 0 < A T (E) (N - 1)$
58		eqid	$⊢ T (E) (N - 1) = T (E) (N - 1)$
59	1 2 3 4 5 6 7 8 9 58	signsvtp	$⊢ (φ \land 0 < A T (E) (N - 1)) \to V (F) = V (E)$
60	57 59	syldan	$⊢ (φ \land 0 < B A) \to V (F) = V (E)$

Metamath Proof Explorer

Theorem signsvfpn

Proof