Step | Hyp | Ref
| Expression |
1 | | simpll 790 |
. . 3
Word
..^
Word |
2 | 1 | eldifad 3586 |
. 2
Word
..^
Word |
3 | | eldifsni 4320 |
. . . 4
Word |
4 | 3 | ad2antrr 762 |
. . 3
Word
..^ |
5 | | simplr 792 |
. . 3
Word
..^ |
6 | 4, 5 | jca 554 |
. 2
Word
..^ |
7 | | simpr 477 |
. 2
Word
..^
..^ |
8 | | simprr 796 |
. . 3
Word
..^ ..^ |
9 | | neeq1 2856 |
. . . . . . . 8
|
10 | | fveq1 6190 |
. . . . . . . . 9
|
11 | 10 | neeq1d 2853 |
. . . . . . . 8
|
12 | 9, 11 | anbi12d 747 |
. . . . . . 7
|
13 | | fveq2 6191 |
. . . . . . . . 9
|
14 | 13 | oveq2d 6666 |
. . . . . . . 8
..^ ..^ |
15 | | fveq2 6191 |
. . . . . . . . . 10
|
16 | 15 | fveq1d 6193 |
. . . . . . . . 9
|
17 | 16 | neeq1d 2853 |
. . . . . . . 8
|
18 | 14, 17 | raleqbidv 3152 |
. . . . . . 7
..^ ..^ |
19 | 12, 18 | imbi12d 334 |
. . . . . 6
..^
..^ |
20 | | neeq1 2856 |
. . . . . . . 8
|
21 | | fveq1 6190 |
. . . . . . . . 9
|
22 | 21 | neeq1d 2853 |
. . . . . . . 8
|
23 | 20, 22 | anbi12d 747 |
. . . . . . 7
|
24 | | fveq2 6191 |
. . . . . . . . 9
|
25 | 24 | oveq2d 6666 |
. . . . . . . 8
..^ ..^ |
26 | | fveq2 6191 |
. . . . . . . . . 10
|
27 | 26 | fveq1d 6193 |
. . . . . . . . 9
|
28 | 27 | neeq1d 2853 |
. . . . . . . 8
|
29 | 25, 28 | raleqbidv 3152 |
. . . . . . 7
..^ ..^ |
30 | 23, 29 | imbi12d 334 |
. . . . . 6
..^
..^ |
31 | | neeq1 2856 |
. . . . . . . 8
++
++ |
32 | | fveq1 6190 |
. . . . . . . . 9
++ ++ |
33 | 32 | neeq1d 2853 |
. . . . . . . 8
++ ++ |
34 | 31, 33 | anbi12d 747 |
. . . . . . 7
++ ++ ++ |
35 | | fveq2 6191 |
. . . . . . . . 9
++ ++ |
36 | 35 | oveq2d 6666 |
. . . . . . . 8
++ ..^ ..^ ++ |
37 | | fveq2 6191 |
. . . . . . . . . 10
++ ++ |
38 | 37 | fveq1d 6193 |
. . . . . . . . 9
++ ++ |
39 | 38 | neeq1d 2853 |
. . . . . . . 8
++ ++ |
40 | 36, 39 | raleqbidv 3152 |
. . . . . . 7
++ ..^
..^ ++ ++
|
41 | 34, 40 | imbi12d 334 |
. . . . . 6
++ ..^
++ ++ ..^ ++ ++
|
42 | | neeq1 2856 |
. . . . . . . 8
|
43 | | fveq1 6190 |
. . . . . . . . 9
|
44 | 43 | neeq1d 2853 |
. . . . . . . 8
|
45 | 42, 44 | anbi12d 747 |
. . . . . . 7
|
46 | | fveq2 6191 |
. . . . . . . . 9
|
47 | 46 | oveq2d 6666 |
. . . . . . . 8
..^ ..^ |
48 | | fveq2 6191 |
. . . . . . . . . 10
|
49 | 48 | fveq1d 6193 |
. . . . . . . . 9
|
50 | 49 | neeq1d 2853 |
. . . . . . . 8
|
51 | 47, 50 | raleqbidv 3152 |
. . . . . . 7
..^ ..^ |
52 | 45, 51 | imbi12d 334 |
. . . . . 6
..^
..^ |
53 | | neirr 2803 |
. . . . . . . 8
|
54 | 53 | intnanr 961 |
. . . . . . 7
|
55 | 54 | pm2.21i 116 |
. . . . . 6
..^ |
56 | | fveq2 6191 |
. . . . . . . . . . . 12
|
57 | 56 | neeq1d 2853 |
. . . . . . . . . . 11
|
58 | 57 | cbvralv 3171 |
. . . . . . . . . 10
..^ ..^ |
59 | 58 | imbi2i 326 |
. . . . . . . . 9
..^
..^ |
60 | 59 | anbi2i 730 |
. . . . . . . 8
Word ..^
Word
..^ |
61 | | simplr 792 |
. . . . . . . . . . . 12
Word ..^ ++ ++ ..^ ++ ..^ ..^ |
62 | | noel 3919 |
. . . . . . . . . . . . . 14
|
63 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
64 | | hash0 13158 |
. . . . . . . . . . . . . . . . . 18
|
65 | 63, 64 | syl6eq 2672 |
. . . . . . . . . . . . . . . . 17
|
66 | 65 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
67 | | fzo0 12492 |
. . . . . . . . . . . . . . . 16
..^ |
68 | 66, 67 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
..^ |
69 | 68 | eleq2d 2687 |
. . . . . . . . . . . . . 14
..^
|
70 | 62, 69 | mtbiri 317 |
. . . . . . . . . . . . 13
..^ |
71 | 70 | adantl 482 |
. . . . . . . . . . . 12
Word ..^ ++ ++ ..^ ++ ..^
..^ |
72 | 61, 71 | pm2.21dd 186 |
. . . . . . . . . . 11
Word ..^ ++ ++ ..^ ++ ..^ ++ |
73 | | simp-6l 810 |
. . . . . . . . . . . . 13
Word ..^ ++ ++ ..^ ++ ..^ Word
|
74 | | simp-6r 811 |
. . . . . . . . . . . . 13
Word ..^ ++ ++ ..^ ++ ..^ |
75 | | simplr 792 |
. . . . . . . . . . . . 13
Word ..^ ++ ++ ..^ ++ ..^
..^ |
76 | | signsv.p |
. . . . . . . . . . . . . 14
|
77 | | signsv.w |
. . . . . . . . . . . . . 14
|
78 | | signsv.t |
. . . . . . . . . . . . . 14
Word
..^ g sgn |
79 | | signsv.v |
. . . . . . . . . . . . . 14
Word ..^ |
80 | 76, 77, 78, 79 | signstfvp 30648 |
. . . . . . . . . . . . 13
Word
..^ ++ |
81 | 73, 74, 75, 80 | syl3anc 1326 |
. . . . . . . . . . . 12
Word ..^ ++ ++ ..^ ++ ..^ ++
|
82 | | simpr 477 |
. . . . . . . . . . . . . 14
Word ..^ ++ ++ ..^ ++ ..^ |
83 | | simplll 798 |
. . . . . . . . . . . . . . . 16
Word
..^ ++ ++ ..^ ++
Word |
84 | 83 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
Word ..^ ++ ++ ..^ ++ ..^ Word |
85 | | simplrr 801 |
. . . . . . . . . . . . . . . 16
Word
..^ ++ ++ ..^ ++
..^ ++ |
86 | 85 | 3anassrs 1290 |
. . . . . . . . . . . . . . 15
Word ..^ ++ ++ ..^ ++ ..^ ++ |
87 | | simpll 790 |
. . . . . . . . . . . . . . . . . 18
Word Word
|
88 | | simplr 792 |
. . . . . . . . . . . . . . . . . . 19
Word |
89 | 88 | s1cld 13383 |
. . . . . . . . . . . . . . . . . 18
Word Word |
90 | | lennncl 13325 |
. . . . . . . . . . . . . . . . . . . 20
Word |
91 | 90 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
Word |
92 | | fzo0end 12560 |
. . . . . . . . . . . . . . . . . . 19
..^ |
93 | | elfzolt3b 12482 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ |
94 | 91, 92, 93 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
Word ..^ |
95 | | ccatval1 13361 |
. . . . . . . . . . . . . . . . . 18
Word Word ..^ ++ |
96 | 87, 89, 94, 95 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
Word ++ |
97 | 96 | neeq1d 2853 |
. . . . . . . . . . . . . . . 16
Word ++
|
98 | 97 | biimpa 501 |
. . . . . . . . . . . . . . 15
Word ++ |
99 | 84, 82, 86, 98 | syl21anc 1325 |
. . . . . . . . . . . . . 14
Word ..^ ++ ++ ..^ ++ ..^ |
100 | | simp-5r 809 |
. . . . . . . . . . . . . 14
Word ..^ ++ ++ ..^ ++ ..^
..^ |
101 | 82, 99, 100 | mp2and 715 |
. . . . . . . . . . . . 13
Word ..^ ++ ++ ..^ ++ ..^
..^ |
102 | 57 | rspcva 3307 |
. . . . . . . . . . . . 13
..^
..^ |
103 | 75, 101, 102 | syl2anc 693 |
. . . . . . . . . . . 12
Word ..^ ++ ++ ..^ ++ ..^ |
104 | 81, 103 | eqnetrd 2861 |
. . . . . . . . . . 11
Word ..^ ++ ++ ..^ ++ ..^ ++
|
105 | 72, 104 | pm2.61dane 2881 |
. . . . . . . . . 10
Word
..^ ++ ++ ..^ ++ ..^ ++ |
106 | | simpr 477 |
. . . . . . . . . . . 12
Word
..^ ++ ++ ..^ ++ |
107 | 106 | fveq2d 6195 |
. . . . . . . . . . 11
Word
..^ ++ ++ ..^ ++ ++ ++ |
108 | | simpr 477 |
. . . . . . . . . . . . . . 15
Word
..^ ++ ++ ..^ ++ |
109 | | simp-4r 807 |
. . . . . . . . . . . . . . 15
Word
..^ ++ ++ ..^ ++ |
110 | | simplrl 800 |
. . . . . . . . . . . . . . . 16
Word
..^ ++ ++ ..^ ++ ++ ++ |
111 | 110 | simprd 479 |
. . . . . . . . . . . . . . 15
Word
..^ ++ ++ ..^ ++ ++ |
112 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . 22
++
++ |
113 | | s1cl 13382 |
. . . . . . . . . . . . . . . . . . . . . . 23
Word
|
114 | | ccatlid 13369 |
. . . . . . . . . . . . . . . . . . . . . . 23
Word
++ |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
++
|
116 | 112, 115 | sylan9eq 2676 |
. . . . . . . . . . . . . . . . . . . . 21
++ |
117 | 116 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
++ |
118 | 117 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
++ ++ |
119 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . 20
++ |
120 | 76, 77, 78, 79 | signstf0 30645 |
. . . . . . . . . . . . . . . . . . . 20
sgn |
121 | 119, 120 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
++ sgn |
122 | 118, 121 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
++ ++ sgn |
123 | 65 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
++ |
124 | 122, 123 | fveq12d 6197 |
. . . . . . . . . . . . . . . . 17
++ ++ sgn |
125 | | sgnclre 30601 |
. . . . . . . . . . . . . . . . . 18
sgn |
126 | | s1fv 13390 |
. . . . . . . . . . . . . . . . . 18
sgn
sgn sgn |
127 | 119, 125,
126 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
++ sgn sgn |
128 | 124, 127 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
++ ++ sgn |
129 | 116 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . 20
++ |
130 | | s1fv 13390 |
. . . . . . . . . . . . . . . . . . . . 21
|
131 | 130 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
132 | 129, 131 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
++ |
133 | 132 | neeq1d 2853 |
. . . . . . . . . . . . . . . . . 18
++ |
134 | 133 | biimpa 501 |
. . . . . . . . . . . . . . . . 17
++ |
135 | | rexr 10085 |
. . . . . . . . . . . . . . . . . . . 20
|
136 | | sgn0bi 30609 |
. . . . . . . . . . . . . . . . . . . 20
sgn |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
sgn
|
138 | 137 | necon3bid 2838 |
. . . . . . . . . . . . . . . . . 18
sgn
|
139 | 138 | biimpar 502 |
. . . . . . . . . . . . . . . . 17
sgn |
140 | 119, 134,
139 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
++ sgn |
141 | 128, 140 | eqnetrd 2861 |
. . . . . . . . . . . . . . 15
++ ++ |
142 | 108, 109,
111, 141 | syl21anc 1325 |
. . . . . . . . . . . . . 14
Word
..^ ++ ++ ..^ ++ ++ |
143 | | simplll 798 |
. . . . . . . . . . . . . . . . . 18
Word ++ ++ ..^ ++
Word
|
144 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
Word ++ ++ ..^ ++
|
145 | | velsn 4193 |
. . . . . . . . . . . . . . . . . . 19
|
146 | 144, 145 | sylnibr 319 |
. . . . . . . . . . . . . . . . . 18
Word ++ ++ ..^ ++
|
147 | 143, 146 | eldifd 3585 |
. . . . . . . . . . . . . . . . 17
Word ++ ++ ..^ ++
Word |
148 | | simpllr 799 |
. . . . . . . . . . . . . . . . 17
Word ++ ++ ..^ ++
|
149 | 76, 77, 78, 79 | signstfvn 30646 |
. . . . . . . . . . . . . . . . 17
Word
++
sgn |
150 | 147, 148,
149 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
Word ++ ++ ..^ ++
++
sgn |
151 | 150 | adantllr 755 |
. . . . . . . . . . . . . . 15
Word
..^ ++ ++ ..^ ++
++
sgn |
152 | 144 | neqned 2801 |
. . . . . . . . . . . . . . . . . . . 20
Word ++ ++ ..^ ++
|
153 | 143, 152,
90 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
Word ++ ++ ..^ ++
|
154 | 153, 92 | syl 17 |
. . . . . . . . . . . . . . . . . 18
Word ++ ++ ..^ ++
..^ |
155 | 76, 77, 78, 79 | signstcl 30642 |
. . . . . . . . . . . . . . . . . 18
Word ..^ |
156 | 143, 154,
155 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
Word ++ ++ ..^ ++
|
157 | 156 | adantllr 755 |
. . . . . . . . . . . . . . . 16
Word
..^ ++ ++ ..^ ++
|
158 | 148 | rexrd 10089 |
. . . . . . . . . . . . . . . . . 18
Word ++ ++ ..^ ++
|
159 | | sgncl 30600 |
. . . . . . . . . . . . . . . . . 18
sgn |
160 | 158, 159 | syl 17 |
. . . . . . . . . . . . . . . . 17
Word ++ ++ ..^ ++
sgn |
161 | 160 | adantllr 755 |
. . . . . . . . . . . . . . . 16
Word
..^ ++ ++ ..^ ++
sgn |
162 | 154 | adantllr 755 |
. . . . . . . . . . . . . . . . 17
Word
..^ ++ ++ ..^ ++
..^ |
163 | 152 | adantllr 755 |
. . . . . . . . . . . . . . . . . 18
Word
..^ ++ ++ ..^ ++
|
164 | | simplll 798 |
. . . . . . . . . . . . . . . . . . 19
Word
..^ ++ ++ ..^ ++
Word |
165 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . 20
Word
..^ ++ ++ ..^ ++
++ ++ |
166 | 165 | simprd 479 |
. . . . . . . . . . . . . . . . . . 19
Word
..^ ++ ++ ..^ ++
++ |
167 | 164, 163,
166, 98 | syl21anc 1325 |
. . . . . . . . . . . . . . . . . 18
Word
..^ ++ ++ ..^ ++
|
168 | | simpllr 799 |
. . . . . . . . . . . . . . . . . 18
Word
..^ ++ ++ ..^ ++
..^ |
169 | 163, 167,
168 | mp2and 715 |
. . . . . . . . . . . . . . . . 17
Word
..^ ++ ++ ..^ ++
..^ |
170 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
|
171 | 170 | neeq1d 2853 |
. . . . . . . . . . . . . . . . . 18
|
172 | 171 | rspcva 3307 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
173 | 162, 169,
172 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
Word
..^ ++ ++ ..^ ++
|
174 | 76, 77 | signswn0 30637 |
. . . . . . . . . . . . . . . 16
sgn
sgn |
175 | 157, 161,
173, 174 | syl21anc 1325 |
. . . . . . . . . . . . . . 15
Word
..^ ++ ++ ..^ ++
sgn |
176 | 151, 175 | eqnetrd 2861 |
. . . . . . . . . . . . . 14
Word
..^ ++ ++ ..^ ++
++
|
177 | 142, 176 | pm2.61dan 832 |
. . . . . . . . . . . . 13
Word ..^ ++ ++ ..^ ++ ++ |
178 | 177 | anassrs 680 |
. . . . . . . . . . . 12
Word
..^ ++ ++ ..^ ++
++ |
179 | 178 | adantr 481 |
. . . . . . . . . . 11
Word
..^ ++ ++ ..^ ++ ++ |
180 | 107, 179 | eqnetrd 2861 |
. . . . . . . . . 10
Word
..^ ++ ++ ..^ ++ ++ |
181 | | lencl 13324 |
. . . . . . . . . . . . 13
Word
|
182 | | nn0uz 11722 |
. . . . . . . . . . . . 13
|
183 | 181, 182 | syl6eleq 2711 |
. . . . . . . . . . . 12
Word
|
184 | 183 | ad4antr 768 |
. . . . . . . . . . 11
Word
..^ ++ ++ ..^ ++
|
185 | | simpr 477 |
. . . . . . . . . . . 12
Word
..^ ++ ++ ..^ ++
..^ ++ |
186 | | ccatws1len 13398 |
. . . . . . . . . . . . . . 15
Word
++ |
187 | 186 | oveq2d 6666 |
. . . . . . . . . . . . . 14
Word
..^ ++ ..^ |
188 | 187 | eleq2d 2687 |
. . . . . . . . . . . . 13
Word
..^ ++ ..^ |
189 | 188 | biimpa 501 |
. . . . . . . . . . . 12
Word ..^ ++
..^ |
190 | 83, 185, 189 | syl2anc 693 |
. . . . . . . . . . 11
Word
..^ ++ ++ ..^ ++
..^ |
191 | | fzosplitsni 12579 |
. . . . . . . . . . . 12
..^
..^ |
192 | 191 | biimpa 501 |
. . . . . . . . . . 11
..^
..^ |
193 | 184, 190,
192 | syl2anc 693 |
. . . . . . . . . 10
Word
..^ ++ ++ ..^ ++
..^ |
194 | 105, 180,
193 | mpjaodan 827 |
. . . . . . . . 9
Word
..^ ++ ++ ..^ ++
++ |
195 | 194 | ralrimiva 2966 |
. . . . . . . 8
Word ..^ ++ ++
..^ ++ ++
|
196 | 60, 195 | sylanbr 490 |
. . . . . . 7
Word ..^ ++ ++
..^ ++ ++
|
197 | 196 | exp31 630 |
. . . . . 6
Word
..^ ++ ++ ..^ ++ ++
|
198 | 19, 30, 41, 52, 55, 197 | wrdind 13476 |
. . . . 5
Word
..^ |
199 | 198 | imp 445 |
. . . 4
Word
..^ |
200 | 199 | adantrr 753 |
. . 3
Word
..^ ..^ |
201 | | fveq2 6191 |
. . . . 5
|
202 | 201 | neeq1d 2853 |
. . . 4
|
203 | 202 | rspcva 3307 |
. . 3
..^
..^ |
204 | 8, 200, 203 | syl2anc 693 |
. 2
Word
..^ |
205 | 2, 6, 7, 204 | syl12anc 1324 |
1
Word
..^ |