signstfvneq0

Description: In case the first letter is not zero, the zero skipping sign is never zero. (Contributed by Thierry Arnoux, 10-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))$
Assertion	signstfvneq0	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land N \in (0 ..^\|F\|)) \to T (F) (N) \neq 0$

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		simpll	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land N \in (0 ..^\|F\|)) \to F \in (Word ℝ ∖ \{\emptyset\})$
6	5	eldifad	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land N \in (0 ..^\|F\|)) \to F \in Word ℝ$
7		eldifsni	$⊢ F \in (Word ℝ ∖ \{\emptyset\}) \to F \neq \emptyset$
8	7	ad2antrr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land N \in (0 ..^\|F\|)) \to F \neq \emptyset$
9		simplr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land N \in (0 ..^\|F\|)) \to F (0) \neq 0$
10	8 9	jca	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land N \in (0 ..^\|F\|)) \to (F \neq \emptyset \land F (0) \neq 0)$
11		simpr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land N \in (0 ..^\|F\|)) \to N \in (0 ..^\|F\|)$
12		fveq2	$⊢ m = N \to T (F) (m) = T (F) (N)$
13	12	neeq1d	$⊢ m = N \to (T (F) (m) \neq 0 \leftrightarrow T (F) (N) \neq 0)$
14		neeq1	$⊢ g = \emptyset \to (g \neq \emptyset \leftrightarrow \emptyset \neq \emptyset)$
15		fveq1	$⊢ g = \emptyset \to g (0) = \emptyset (0)$
16	15	neeq1d	$⊢ g = \emptyset \to (g (0) \neq 0 \leftrightarrow \emptyset (0) \neq 0)$
17	14 16	anbi12d	$⊢ g = \emptyset \to ((g \neq \emptyset \land g (0) \neq 0) \leftrightarrow (\emptyset \neq \emptyset \land \emptyset (0) \neq 0))$
18		fveq2	$⊢ g = \emptyset \to \|g\| = \|\emptyset\|$
19	18	oveq2d	$⊢ g = \emptyset \to (0 ..^\|g\|) = (0 ..^\|\emptyset\|)$
20		fveq2	$⊢ g = \emptyset \to T (g) = T (\emptyset)$
21	20	fveq1d	$⊢ g = \emptyset \to T (g) (m) = T (\emptyset) (m)$
22	21	neeq1d	$⊢ g = \emptyset \to (T (g) (m) \neq 0 \leftrightarrow T (\emptyset) (m) \neq 0)$
23	19 22	raleqbidv	$⊢ g = \emptyset \to (\forall m \in (0 ..^\|g\|) T (g) (m) \neq 0 \leftrightarrow \forall m \in (0 ..^\|\emptyset\|) T (\emptyset) (m) \neq 0)$
24	17 23	imbi12d	$⊢ g = \emptyset \to (((g \neq \emptyset \land g (0) \neq 0) \to \forall m \in (0 ..^\|g\|) T (g) (m) \neq 0) \leftrightarrow ((\emptyset \neq \emptyset \land \emptyset (0) \neq 0) \to \forall m \in (0 ..^\|\emptyset\|) T (\emptyset) (m) \neq 0))$
25		neeq1	$⊢ g = e \to (g \neq \emptyset \leftrightarrow e \neq \emptyset)$
26		fveq1	$⊢ g = e \to g (0) = e (0)$
27	26	neeq1d	$⊢ g = e \to (g (0) \neq 0 \leftrightarrow e (0) \neq 0)$
28	25 27	anbi12d	$⊢ g = e \to ((g \neq \emptyset \land g (0) \neq 0) \leftrightarrow (e \neq \emptyset \land e (0) \neq 0))$
29		fveq2	$⊢ g = e \to \|g\| = \|e\|$
30	29	oveq2d	$⊢ g = e \to (0 ..^\|g\|) = (0 ..^\|e\|)$
31		fveq2	$⊢ g = e \to T (g) = T (e)$
32	31	fveq1d	$⊢ g = e \to T (g) (m) = T (e) (m)$
33	32	neeq1d	$⊢ g = e \to (T (g) (m) \neq 0 \leftrightarrow T (e) (m) \neq 0)$
34	30 33	raleqbidv	$⊢ g = e \to (\forall m \in (0 ..^\|g\|) T (g) (m) \neq 0 \leftrightarrow \forall m \in (0 ..^\|e\|) T (e) (m) \neq 0)$
35	28 34	imbi12d	$⊢ g = e \to (((g \neq \emptyset \land g (0) \neq 0) \to \forall m \in (0 ..^\|g\|) T (g) (m) \neq 0) \leftrightarrow ((e \neq \emptyset \land e (0) \neq 0) \to \forall m \in (0 ..^\|e\|) T (e) (m) \neq 0))$
36		neeq1	$⊢ g = e ++ ⟨“ k ”⟩ \to (g \neq \emptyset \leftrightarrow e ++ ⟨“ k ”⟩ \neq \emptyset)$
37		fveq1	$⊢ g = e ++ ⟨“ k ”⟩ \to g (0) = (e ++ ⟨“ k ”⟩) (0)$
38	37	neeq1d	$⊢ g = e ++ ⟨“ k ”⟩ \to (g (0) \neq 0 \leftrightarrow (e ++ ⟨“ k ”⟩) (0) \neq 0)$
39	36 38	anbi12d	$⊢ g = e ++ ⟨“ k ”⟩ \to ((g \neq \emptyset \land g (0) \neq 0) \leftrightarrow (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0))$
40		fveq2	$⊢ g = e ++ ⟨“ k ”⟩ \to \|g\| = \|e ++ ⟨“ k ”⟩\|$
41	40	oveq2d	$⊢ g = e ++ ⟨“ k ”⟩ \to (0 ..^\|g\|) = (0 ..^\|e ++ ⟨“ k ”⟩\|)$
42		fveq2	$⊢ g = e ++ ⟨“ k ”⟩ \to T (g) = T (e ++ ⟨“ k ”⟩)$
43	42	fveq1d	$⊢ g = e ++ ⟨“ k ”⟩ \to T (g) (m) = T (e ++ ⟨“ k ”⟩) (m)$
44	43	neeq1d	$⊢ g = e ++ ⟨“ k ”⟩ \to (T (g) (m) \neq 0 \leftrightarrow T (e ++ ⟨“ k ”⟩) (m) \neq 0)$
45	41 44	raleqbidv	$⊢ g = e ++ ⟨“ k ”⟩ \to (\forall m \in (0 ..^\|g\|) T (g) (m) \neq 0 \leftrightarrow \forall m \in (0 ..^\|e ++ ⟨“ k ”⟩\|) T (e ++ ⟨“ k ”⟩) (m) \neq 0)$
46	39 45	imbi12d	$⊢ g = e ++ ⟨“ k ”⟩ \to (((g \neq \emptyset \land g (0) \neq 0) \to \forall m \in (0 ..^\|g\|) T (g) (m) \neq 0) \leftrightarrow ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \to \forall m \in (0 ..^\|e ++ ⟨“ k ”⟩\|) T (e ++ ⟨“ k ”⟩) (m) \neq 0))$
47		neeq1	$⊢ g = F \to (g \neq \emptyset \leftrightarrow F \neq \emptyset)$
48		fveq1	$⊢ g = F \to g (0) = F (0)$
49	48	neeq1d	$⊢ g = F \to (g (0) \neq 0 \leftrightarrow F (0) \neq 0)$
50	47 49	anbi12d	$⊢ g = F \to ((g \neq \emptyset \land g (0) \neq 0) \leftrightarrow (F \neq \emptyset \land F (0) \neq 0))$
51		fveq2	$⊢ g = F \to \|g\| = \|F\|$
52	51	oveq2d	$⊢ g = F \to (0 ..^\|g\|) = (0 ..^\|F\|)$
53		fveq2	$⊢ g = F \to T (g) = T (F)$
54	53	fveq1d	$⊢ g = F \to T (g) (m) = T (F) (m)$
55	54	neeq1d	$⊢ g = F \to (T (g) (m) \neq 0 \leftrightarrow T (F) (m) \neq 0)$
56	52 55	raleqbidv	$⊢ g = F \to (\forall m \in (0 ..^\|g\|) T (g) (m) \neq 0 \leftrightarrow \forall m \in (0 ..^\|F\|) T (F) (m) \neq 0)$
57	50 56	imbi12d	$⊢ g = F \to (((g \neq \emptyset \land g (0) \neq 0) \to \forall m \in (0 ..^\|g\|) T (g) (m) \neq 0) \leftrightarrow ((F \neq \emptyset \land F (0) \neq 0) \to \forall m \in (0 ..^\|F\|) T (F) (m) \neq 0))$
58		neirr	$⊢ \neg \emptyset \neq \emptyset$
59	58	intnanr	$⊢ \neg (\emptyset \neq \emptyset \land \emptyset (0) \neq 0)$
60	59	pm2.21i	$⊢ (\emptyset \neq \emptyset \land \emptyset (0) \neq 0) \to \forall m \in (0 ..^\|\emptyset\|) T (\emptyset) (m) \neq 0$
61		fveq2	$⊢ n = m \to T (e) (n) = T (e) (m)$
62	61	neeq1d	$⊢ n = m \to (T (e) (n) \neq 0 \leftrightarrow T (e) (m) \neq 0)$
63	62	cbvralvw	$⊢ \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0 \leftrightarrow \forall m \in (0 ..^\|e\|) T (e) (m) \neq 0$
64	63	imbi2i	$⊢ ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0) \leftrightarrow ((e \neq \emptyset \land e (0) \neq 0) \to \forall m \in (0 ..^\|e\|) T (e) (m) \neq 0)$
65	64	anbi2i	$⊢ ((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \leftrightarrow ((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall m \in (0 ..^\|e\|) T (e) (m) \neq 0))$
66		simplr	$⊢ ((((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \land m \in (0 ..^\|e\|)) \land e = \emptyset) \to m \in (0 ..^\|e\|)$
67		noel	$⊢ \neg m \in \emptyset$
68		fveq2	$⊢ e = \emptyset \to \|e\| = \|\emptyset\|$
69		hash0	$⊢ \|\emptyset\| = 0$
70	68 69	eqtrdi	$⊢ e = \emptyset \to \|e\| = 0$
71	70	oveq2d	$⊢ e = \emptyset \to (0 ..^\|e\|) = (0 ..^0)$
72		fzo0	$⊢ (0 ..^0) = \emptyset$
73	71 72	eqtrdi	$⊢ e = \emptyset \to (0 ..^\|e\|) = \emptyset$
74	73	eleq2d	$⊢ e = \emptyset \to (m \in (0 ..^\|e\|) \leftrightarrow m \in \emptyset)$
75	67 74	mtbiri	$⊢ e = \emptyset \to \neg m \in (0 ..^\|e\|)$
76	75	adantl	$⊢ ((((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \land m \in (0 ..^\|e\|)) \land e = \emptyset) \to \neg m \in (0 ..^\|e\|)$
77	66 76	pm2.21dd	$⊢ ((((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \land m \in (0 ..^\|e\|)) \land e = \emptyset) \to T (e ++ ⟨“ k ”⟩) (m) \neq 0$
78		simp-6l	$⊢ ((((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \land m \in (0 ..^\|e\|)) \land e \neq \emptyset) \to e \in Word ℝ$
79		simp-6r	$⊢ ((((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \land m \in (0 ..^\|e\|)) \land e \neq \emptyset) \to k \in ℝ$
80		simplr	$⊢ ((((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \land m \in (0 ..^\|e\|)) \land e \neq \emptyset) \to m \in (0 ..^\|e\|)$
81	1 2 3 4	signstfvp	$⊢ (e \in Word ℝ \land k \in ℝ \land m \in (0 ..^\|e\|)) \to T (e ++ ⟨“ k ”⟩) (m) = T (e) (m)$
82	78 79 80 81	syl3anc	$⊢ ((((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \land m \in (0 ..^\|e\|)) \land e \neq \emptyset) \to T (e ++ ⟨“ k ”⟩) (m) = T (e) (m)$
83		simpr	$⊢ ((((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \land m \in (0 ..^\|e\|)) \land e \neq \emptyset) \to e \neq \emptyset$
84		simp-5l	$⊢ ((((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \land m \in (0 ..^\|e\|)) \land e \neq \emptyset) \to (e \in Word ℝ \land k \in ℝ)$
85		simplrr	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land (m \in (0 ..^\|e ++ ⟨“ k ”⟩\|) \land m \in (0 ..^\|e\|) \land e \neq \emptyset)) \to (e ++ ⟨“ k ”⟩) (0) \neq 0$
86	85	3anassrs	$⊢ ((((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \land m \in (0 ..^\|e\|)) \land e \neq \emptyset) \to (e ++ ⟨“ k ”⟩) (0) \neq 0$
87		simpll	$⊢ ((e \in Word ℝ \land k \in ℝ) \land e \neq \emptyset) \to e \in Word ℝ$
88		s1cl	$⊢ k \in ℝ \to ⟨“ k ”⟩ \in Word ℝ$
89	88	ad2antlr	$⊢ ((e \in Word ℝ \land k \in ℝ) \land e \neq \emptyset) \to ⟨“ k ”⟩ \in Word ℝ$
90		lennncl	$⊢ (e \in Word ℝ \land e \neq \emptyset) \to \|e\| \in ℕ$
91	90	adantlr	$⊢ ((e \in Word ℝ \land k \in ℝ) \land e \neq \emptyset) \to \|e\| \in ℕ$
92		fzo0end	$⊢ \|e\| \in ℕ \to \|e\| - 1 \in (0 ..^\|e\|)$
93		elfzolt3b	$⊢ \|e\| - 1 \in (0 ..^\|e\|) \to 0 \in (0 ..^\|e\|)$
94	91 92 93	3syl	$⊢ ((e \in Word ℝ \land k \in ℝ) \land e \neq \emptyset) \to 0 \in (0 ..^\|e\|)$
95		ccatval1	$⊢ (e \in Word ℝ \land ⟨“ k ”⟩ \in Word ℝ \land 0 \in (0 ..^\|e\|)) \to (e ++ ⟨“ k ”⟩) (0) = e (0)$
96	87 89 94 95	syl3anc	$⊢ ((e \in Word ℝ \land k \in ℝ) \land e \neq \emptyset) \to (e ++ ⟨“ k ”⟩) (0) = e (0)$
97	96	neeq1d	$⊢ ((e \in Word ℝ \land k \in ℝ) \land e \neq \emptyset) \to ((e ++ ⟨“ k ”⟩) (0) \neq 0 \leftrightarrow e (0) \neq 0)$
98	97	biimpa	$⊢ (((e \in Word ℝ \land k \in ℝ) \land e \neq \emptyset) \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \to e (0) \neq 0$
99	84 83 86 98	syl21anc	$⊢ ((((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \land m \in (0 ..^\|e\|)) \land e \neq \emptyset) \to e (0) \neq 0$
100		simp-5r	$⊢ ((((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \land m \in (0 ..^\|e\|)) \land e \neq \emptyset) \to ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)$
101	83 99 100	mp2and	$⊢ ((((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \land m \in (0 ..^\|e\|)) \land e \neq \emptyset) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0$
102	62 101 80	rspcdva	$⊢ ((((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \land m \in (0 ..^\|e\|)) \land e \neq \emptyset) \to T (e) (m) \neq 0$
103	82 102	eqnetrd	$⊢ ((((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \land m \in (0 ..^\|e\|)) \land e \neq \emptyset) \to T (e ++ ⟨“ k ”⟩) (m) \neq 0$
104	77 103	pm2.61dane	$⊢ (((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \land m \in (0 ..^\|e\|)) \to T (e ++ ⟨“ k ”⟩) (m) \neq 0$
105		simpr	$⊢ (((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \land m = \|e\|) \to m = \|e\|$
106	105	fveq2d	$⊢ (((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \land m = \|e\|) \to T (e ++ ⟨“ k ”⟩) (m) = T (e ++ ⟨“ k ”⟩) (\|e\|)$
107		simpr	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e = \emptyset) \to e = \emptyset$
108		simp-4r	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e = \emptyset) \to k \in ℝ$
109		simplrl	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e = \emptyset) \to (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)$
110	109	simprd	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e = \emptyset) \to (e ++ ⟨“ k ”⟩) (0) \neq 0$
111		oveq1	$⊢ e = \emptyset \to e ++ ⟨“ k ”⟩ = \emptyset ++ ⟨“ k ”⟩$
112		ccatlid	$⊢ ⟨“ k ”⟩ \in Word ℝ \to \emptyset ++ ⟨“ k ”⟩ = ⟨“ k ”⟩$
113	88 112	syl	$⊢ k \in ℝ \to \emptyset ++ ⟨“ k ”⟩ = ⟨“ k ”⟩$
114	111 113	sylan9eq	$⊢ (e = \emptyset \land k \in ℝ) \to e ++ ⟨“ k ”⟩ = ⟨“ k ”⟩$
115	114	fveq2d	$⊢ (e = \emptyset \land k \in ℝ) \to T (e ++ ⟨“ k ”⟩) = T (⟨“ k ”⟩)$
116	115	adantr	$⊢ ((e = \emptyset \land k \in ℝ) \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \to T (e ++ ⟨“ k ”⟩) = T (⟨“ k ”⟩)$
117	1 2 3 4	signstf0	$⊢ k \in ℝ \to T (⟨“ k ”⟩) = ⟨“ sgn (k) ”⟩$
118	117	ad2antlr	$⊢ ((e = \emptyset \land k \in ℝ) \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \to T (⟨“ k ”⟩) = ⟨“ sgn (k) ”⟩$
119	116 118	eqtrd	$⊢ ((e = \emptyset \land k \in ℝ) \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \to T (e ++ ⟨“ k ”⟩) = ⟨“ sgn (k) ”⟩$
120	70	ad2antrr	$⊢ ((e = \emptyset \land k \in ℝ) \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \to \|e\| = 0$
121	119 120	fveq12d	$⊢ ((e = \emptyset \land k \in ℝ) \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \to T (e ++ ⟨“ k ”⟩) (\|e\|) = ⟨“ sgn (k) ”⟩ (0)$
122		sgnclre	$⊢ k \in ℝ \to sgn (k) \in ℝ$
123		s1fv	$⊢ sgn (k) \in ℝ \to ⟨“ sgn (k) ”⟩ (0) = sgn (k)$
124	122 123	syl	$⊢ k \in ℝ \to ⟨“ sgn (k) ”⟩ (0) = sgn (k)$
125	124	ad2antlr	$⊢ ((e = \emptyset \land k \in ℝ) \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \to ⟨“ sgn (k) ”⟩ (0) = sgn (k)$
126	121 125	eqtrd	$⊢ ((e = \emptyset \land k \in ℝ) \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \to T (e ++ ⟨“ k ”⟩) (\|e\|) = sgn (k)$
127		simplr	$⊢ ((e = \emptyset \land k \in ℝ) \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \to k \in ℝ$
128	114	fveq1d	$⊢ (e = \emptyset \land k \in ℝ) \to (e ++ ⟨“ k ”⟩) (0) = ⟨“ k ”⟩ (0)$
129		s1fv	$⊢ k \in ℝ \to ⟨“ k ”⟩ (0) = k$
130	129	adantl	$⊢ (e = \emptyset \land k \in ℝ) \to ⟨“ k ”⟩ (0) = k$
131	128 130	eqtrd	$⊢ (e = \emptyset \land k \in ℝ) \to (e ++ ⟨“ k ”⟩) (0) = k$
132	131	neeq1d	$⊢ (e = \emptyset \land k \in ℝ) \to ((e ++ ⟨“ k ”⟩) (0) \neq 0 \leftrightarrow k \neq 0)$
133	132	biimpa	$⊢ ((e = \emptyset \land k \in ℝ) \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \to k \neq 0$
134		rexr	$⊢ k \in ℝ \to k \in ℝ^{*}$
135		sgn0bi	$⊢ k \in ℝ^{*} \to (sgn (k) = 0 \leftrightarrow k = 0)$
136	134 135	syl	$⊢ k \in ℝ \to (sgn (k) = 0 \leftrightarrow k = 0)$
137	136	necon3bid	$⊢ k \in ℝ \to (sgn (k) \neq 0 \leftrightarrow k \neq 0)$
138	137	biimpar	$⊢ (k \in ℝ \land k \neq 0) \to sgn (k) \neq 0$
139	127 133 138	syl2anc	$⊢ ((e = \emptyset \land k \in ℝ) \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \to sgn (k) \neq 0$
140	126 139	eqnetrd	$⊢ ((e = \emptyset \land k \in ℝ) \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \to T (e ++ ⟨“ k ”⟩) (\|e\|) \neq 0$
141	107 108 110 140	syl21anc	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e = \emptyset) \to T (e ++ ⟨“ k ”⟩) (\|e\|) \neq 0$
142		eldifsn	$⊢ e \in (Word ℝ ∖ \{\emptyset\}) \leftrightarrow (e \in Word ℝ \land e \neq \emptyset)$
143	142	biimpri	$⊢ (e \in Word ℝ \land e \neq \emptyset) \to e \in (Word ℝ ∖ \{\emptyset\})$
144	143	adantlr	$⊢ ((e \in Word ℝ \land k \in ℝ) \land e \neq \emptyset) \to e \in (Word ℝ ∖ \{\emptyset\})$
145		simplr	$⊢ ((e \in Word ℝ \land k \in ℝ) \land e \neq \emptyset) \to k \in ℝ$
146	1 2 3 4	signstfvn	$⊢ (e \in (Word ℝ ∖ \{\emptyset\}) \land k \in ℝ) \to T (e ++ ⟨“ k ”⟩) (\|e\|) = T (e) (\|e\| - 1) \underset{˙}{⨣} sgn (k)$
147	144 145 146	syl2anc	$⊢ ((e \in Word ℝ \land k \in ℝ) \land e \neq \emptyset) \to T (e ++ ⟨“ k ”⟩) (\|e\|) = T (e) (\|e\| - 1) \underset{˙}{⨣} sgn (k)$
148	147	ad4ant14	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e \neq \emptyset) \to T (e ++ ⟨“ k ”⟩) (\|e\|) = T (e) (\|e\| - 1) \underset{˙}{⨣} sgn (k)$
149	90 92	syl	$⊢ (e \in Word ℝ \land e \neq \emptyset) \to \|e\| - 1 \in (0 ..^\|e\|)$
150	1 2 3 4	signstcl	$⊢ (e \in Word ℝ \land \|e\| - 1 \in (0 ..^\|e\|)) \to T (e) (\|e\| - 1) \in \{- 1, 0, 1\}$
151	149 150	syldan	$⊢ (e \in Word ℝ \land e \neq \emptyset) \to T (e) (\|e\| - 1) \in \{- 1, 0, 1\}$
152	151	ad5ant15	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e \neq \emptyset) \to T (e) (\|e\| - 1) \in \{- 1, 0, 1\}$
153		sgncl	$⊢ k \in ℝ^{*} \to sgn (k) \in \{- 1, 0, 1\}$
154	134 153	syl	$⊢ k \in ℝ \to sgn (k) \in \{- 1, 0, 1\}$
155	154	ad4antlr	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e \neq \emptyset) \to sgn (k) \in \{- 1, 0, 1\}$
156		fveq2	$⊢ n = \|e\| - 1 \to T (e) (n) = T (e) (\|e\| - 1)$
157	156	neeq1d	$⊢ n = \|e\| - 1 \to (T (e) (n) \neq 0 \leftrightarrow T (e) (\|e\| - 1) \neq 0)$
158		simpr	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e \neq \emptyset) \to e \neq \emptyset$
159		simplll	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e \neq \emptyset) \to (e \in Word ℝ \land k \in ℝ)$
160		simplrl	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e \neq \emptyset) \to (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)$
161	160	simprd	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e \neq \emptyset) \to (e ++ ⟨“ k ”⟩) (0) \neq 0$
162	159 158 161 98	syl21anc	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e \neq \emptyset) \to e (0) \neq 0$
163		simpllr	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e \neq \emptyset) \to ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)$
164	158 162 163	mp2and	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e \neq \emptyset) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0$
165	90	ad4ant14	$⊢ (((e \in Word ℝ \land k \in ℝ) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e \neq \emptyset) \to \|e\| \in ℕ$
166	165 92	syl	$⊢ (((e \in Word ℝ \land k \in ℝ) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e \neq \emptyset) \to \|e\| - 1 \in (0 ..^\|e\|)$
167	166	adantllr	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e \neq \emptyset) \to \|e\| - 1 \in (0 ..^\|e\|)$
168	157 164 167	rspcdva	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e \neq \emptyset) \to T (e) (\|e\| - 1) \neq 0$
169	1 2	signswn0	$⊢ ((T (e) (\|e\| - 1) \in \{- 1, 0, 1\} \land sgn (k) \in \{- 1, 0, 1\}) \land T (e) (\|e\| - 1) \neq 0) \to T (e) (\|e\| - 1) \underset{˙}{⨣} sgn (k) \neq 0$
170	152 155 168 169	syl21anc	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e \neq \emptyset) \to T (e) (\|e\| - 1) \underset{˙}{⨣} sgn (k) \neq 0$
171	148 170	eqnetrd	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \land e \neq \emptyset) \to T (e ++ ⟨“ k ”⟩) (\|e\|) \neq 0$
172	141 171	pm2.61dane	$⊢ (((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|))) \to T (e ++ ⟨“ k ”⟩) (\|e\|) \neq 0$
173	172	anassrs	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \to T (e ++ ⟨“ k ”⟩) (\|e\|) \neq 0$
174	173	adantr	$⊢ (((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \land m = \|e\|) \to T (e ++ ⟨“ k ”⟩) (\|e\|) \neq 0$
175	106 174	eqnetrd	$⊢ (((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \land m = \|e\|) \to T (e ++ ⟨“ k ”⟩) (m) \neq 0$
176		lencl	$⊢ e \in Word ℝ \to \|e\| \in ℕ_{0}$
177		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
178	176 177	eleqtrdi	$⊢ e \in Word ℝ \to \|e\| \in ℤ_{\geq 0}$
179	178	ad4antr	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \to \|e\| \in ℤ_{\geq 0}$
180		ccatws1len	$⊢ e \in Word ℝ \to \|e ++ ⟨“ k ”⟩\| = \|e\| + 1$
181	180	adantr	$⊢ (e \in Word ℝ \land k \in ℝ) \to \|e ++ ⟨“ k ”⟩\| = \|e\| + 1$
182	181	oveq2d	$⊢ (e \in Word ℝ \land k \in ℝ) \to (0 ..^\|e ++ ⟨“ k ”⟩\|) = (0 ..^\|e\| + 1)$
183	182	eleq2d	$⊢ (e \in Word ℝ \land k \in ℝ) \to (m \in (0 ..^\|e ++ ⟨“ k ”⟩\|) \leftrightarrow m \in (0 ..^\|e\| + 1))$
184	183	biimpa	$⊢ ((e \in Word ℝ \land k \in ℝ) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \to m \in (0 ..^\|e\| + 1)$
185	184	ad4ant14	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \to m \in (0 ..^\|e\| + 1)$
186		fzosplitsni	$⊢ \|e\| \in ℤ_{\geq 0} \to (m \in (0 ..^\|e\| + 1) \leftrightarrow (m \in (0 ..^\|e\|) \lor m = \|e\|))$
187	186	biimpa	$⊢ (\|e\| \in ℤ_{\geq 0} \land m \in (0 ..^\|e\| + 1)) \to (m \in (0 ..^\|e\|) \lor m = \|e\|)$
188	179 185 187	syl2anc	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \to (m \in (0 ..^\|e\|) \lor m = \|e\|)$
189	104 175 188	mpjaodan	$⊢ ((((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \land m \in (0 ..^\|e ++ ⟨“ k ”⟩\|)) \to T (e ++ ⟨“ k ”⟩) (m) \neq 0$
190	189	ralrimiva	$⊢ (((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall n \in (0 ..^\|e\|) T (e) (n) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \to \forall m \in (0 ..^\|e ++ ⟨“ k ”⟩\|) T (e ++ ⟨“ k ”⟩) (m) \neq 0$
191	65 190	sylanbr	$⊢ (((e \in Word ℝ \land k \in ℝ) \land ((e \neq \emptyset \land e (0) \neq 0) \to \forall m \in (0 ..^\|e\|) T (e) (m) \neq 0)) \land (e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0)) \to \forall m \in (0 ..^\|e ++ ⟨“ k ”⟩\|) T (e ++ ⟨“ k ”⟩) (m) \neq 0$
192	191	exp31	$⊢ (e \in Word ℝ \land k \in ℝ) \to (((e \neq \emptyset \land e (0) \neq 0) \to \forall m \in (0 ..^\|e\|) T (e) (m) \neq 0) \to ((e ++ ⟨“ k ”⟩ \neq \emptyset \land (e ++ ⟨“ k ”⟩) (0) \neq 0) \to \forall m \in (0 ..^\|e ++ ⟨“ k ”⟩\|) T (e ++ ⟨“ k ”⟩) (m) \neq 0))$
193	24 35 46 57 60 192	wrdind	$⊢ F \in Word ℝ \to ((F \neq \emptyset \land F (0) \neq 0) \to \forall m \in (0 ..^\|F\|) T (F) (m) \neq 0)$
194	193	imp	$⊢ (F \in Word ℝ \land (F \neq \emptyset \land F (0) \neq 0)) \to \forall m \in (0 ..^\|F\|) T (F) (m) \neq 0$
195	194	adantr	$⊢ ((F \in Word ℝ \land (F \neq \emptyset \land F (0) \neq 0)) \land N \in (0 ..^\|F\|)) \to \forall m \in (0 ..^\|F\|) T (F) (m) \neq 0$
196		simpr	$⊢ ((F \in Word ℝ \land (F \neq \emptyset \land F (0) \neq 0)) \land N \in (0 ..^\|F\|)) \to N \in (0 ..^\|F\|)$
197	13 195 196	rspcdva	$⊢ ((F \in Word ℝ \land (F \neq \emptyset \land F (0) \neq 0)) \land N \in (0 ..^\|F\|)) \to T (F) (N) \neq 0$
198	6 10 11 197	syl21anc	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land N \in (0 ..^\|F\|)) \to T (F) (N) \neq 0$

Metamath Proof Explorer

Theorem signstfvneq0

Proof