signsvfnn

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	$⊢ \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	signsvfnn	$⊢ (φ \land B A < 0) \to V (F) - V (E) = 1$

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	5	adantr	$⊢ (φ \land B A < 0) \to E \in (Word ℝ ∖ \{\emptyset\})$
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	ffvelrnd	$⊢ φ \to E (N - 1) \in ℝ$
23	22	recnd	$⊢ φ \to E (N - 1) \in ℂ$
24	10 23	eqeltrid	$⊢ φ \to B \in ℂ$
25	24	adantr	$⊢ (φ \land B A < 0) \to B \in ℂ$
26	8	recnd	$⊢ φ \to A \in ℂ$
27	26	adantr	$⊢ (φ \land B A < 0) \to A \in ℂ$
28		simpr	$⊢ (φ \land B A < 0) \to B A < 0$
29	28	lt0ne0d	$⊢ (φ \land B A < 0) \to B A \neq 0$
30	25 27 29	mulne0bad	$⊢ (φ \land B A < 0) \to B \neq 0$
31	10 30	eqnetrrid	$⊢ (φ \land B A < 0) \to E (N - 1) \neq 0$
32	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))$
33	10	fveq2i	$⊢ sgn (B) = sgn (E (N - 1))$
34	32 33	eqtr4di	$⊢ (E \in (Word ℝ ∖ \{\emptyset\}) \land E (N - 1) \neq 0) \to T (E) (N - 1) = sgn (B)$
35	11 31 34	syl2anc	$⊢ (φ \land B A < 0) \to T (E) (N - 1) = sgn (B)$
36	35	fveq2d	$⊢ (φ \land B A < 0) \to sgn (T (E) (N - 1)) = sgn (sgn (B))$
37	10 22	eqeltrid	$⊢ φ \to B \in ℝ$
38	37	adantr	$⊢ (φ \land B A < 0) \to B \in ℝ$
39	38	rexrd	$⊢ (φ \land B A < 0) \to B \in ℝ^{*}$
40		sgnsgn	$⊢ B \in ℝ^{*} \to sgn (sgn (B)) = sgn (B)$
41	39 40	syl	$⊢ (φ \land B A < 0) \to sgn (sgn (B)) = sgn (B)$
42	36 41	eqtrd	$⊢ (φ \land B A < 0) \to sgn (T (E) (N - 1)) = sgn (B)$
43	42	oveq2d	$⊢ (φ \land B A < 0) \to sgn (A) sgn (T (E) (N - 1)) = sgn (A) sgn (B)$
44	26 24	mulcomd	$⊢ φ \to A B = B A$
45	44	breq1d	$⊢ φ \to (A B < 0 \leftrightarrow B A < 0)$
46		sgnmulsgn	$⊢ (A \in ℝ \land B \in ℝ) \to (A B < 0 \leftrightarrow sgn (A) sgn (B) < 0)$
47	8 37 46	syl2anc	$⊢ φ \to (A B < 0 \leftrightarrow sgn (A) sgn (B) < 0)$
48	45 47	bitr3d	$⊢ φ \to (B A < 0 \leftrightarrow sgn (A) sgn (B) < 0)$
49	48	biimpa	$⊢ (φ \land B A < 0) \to sgn (A) sgn (B) < 0$
50	43 49	eqbrtrd	$⊢ (φ \land B A < 0) \to sgn (A) sgn (T (E) (N - 1)) < 0$
51	8	adantr	$⊢ (φ \land B A < 0) \to A \in ℝ$
52		sgnclre	$⊢ B \in ℝ \to sgn (B) \in ℝ$
53	38 52	syl	$⊢ (φ \land B A < 0) \to sgn (B) \in ℝ$
54	35 53	eqeltrd	$⊢ (φ \land B A < 0) \to T (E) (N - 1) \in ℝ$
55		sgnmulsgn	$⊢ (A \in ℝ \land T (E) (N - 1) \in ℝ) \to (A T (E) (N - 1) < 0 \leftrightarrow sgn (A) sgn (T (E) (N - 1)) < 0)$
56	51 54 55	syl2anc	$⊢ (φ \land B A < 0) \to (A T (E) (N - 1) < 0 \leftrightarrow sgn (A) sgn (T (E) (N - 1)) < 0)$
57	50 56	mpbird	$⊢ (φ \land B A < 0) \to A T (E) (N - 1) < 0$
58		eqid	$⊢ T (E) (N - 1) = T (E) (N - 1)$
59	1 2 3 4 5 6 7 8 9 58	signsvtn	$⊢ (φ \land A T (E) (N - 1) < 0) \to V (F) - V (E) = 1$
60	57 59	syldan	$⊢ (φ \land B A < 0) \to V (F) - V (E) = 1$

Metamath Proof Explorer

Theorem signsvfnn

Proof