Metamath Proof Explorer

Theorem 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 ⊢⨣˙=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
Assertion signstfvneq0 ⊢F∈Wordℝ∖∅∧F⁡0≠0∧N∈0..^F→T⁡F⁡N≠0

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