Step | Hyp | Ref
| Expression |
1 | | simpl1 1064 |
. . . . . . . . 9
|
2 | | simpl3l 1116 |
. . . . . . . . 9
|
3 | | simpl21 1139 |
. . . . . . . . 9
|
4 | | simpl22 1140 |
. . . . . . . . 9
|
5 | | brcolinear 32166 |
. . . . . . . . 9
|
6 | 1, 2, 3, 4, 5 | syl13anc 1328 |
. . . . . . . 8
|
7 | 6 | biimpa 501 |
. . . . . . 7
|
8 | | simpr 477 |
. . . . . . . . . . . 12
|
9 | | brcolinear 32166 |
. . . . . . . . . . . 12
|
10 | 1, 8, 3, 4, 9 | syl13anc 1328 |
. . . . . . . . . . 11
|
11 | 10 | adantr 481 |
. . . . . . . . . 10
|
12 | | btwnconn3 32210 |
. . . . . . . . . . . . . . 15
|
13 | 1, 3, 2, 8, 4, 12 | syl122anc 1335 |
. . . . . . . . . . . . . 14
|
14 | 13 | imp 445 |
. . . . . . . . . . . . 13
|
15 | | btwncolinear3 32178 |
. . . . . . . . . . . . . . . 16
|
16 | 1, 3, 8, 2, 15 | syl13anc 1328 |
. . . . . . . . . . . . . . 15
|
17 | | btwncolinear5 32180 |
. . . . . . . . . . . . . . . 16
|
18 | 1, 3, 2, 8, 17 | syl13anc 1328 |
. . . . . . . . . . . . . . 15
|
19 | 16, 18 | jaod 395 |
. . . . . . . . . . . . . 14
|
20 | 19 | adantr 481 |
. . . . . . . . . . . . 13
|
21 | 14, 20 | mpd 15 |
. . . . . . . . . . . 12
|
22 | 21 | expr 643 |
. . . . . . . . . . 11
|
23 | | simprl 794 |
. . . . . . . . . . . . . . 15
|
24 | 1, 2, 3, 4, 23 | btwncomand 32122 |
. . . . . . . . . . . . . 14
|
25 | | simprr 796 |
. . . . . . . . . . . . . 14
|
26 | 1, 4, 2, 3, 8, 24,
25 | btwnexch3and 32128 |
. . . . . . . . . . . . 13
|
27 | | btwncolinear4 32179 |
. . . . . . . . . . . . . . 15
|
28 | 1, 2, 8, 3, 27 | syl13anc 1328 |
. . . . . . . . . . . . . 14
|
29 | 28 | adantr 481 |
. . . . . . . . . . . . 13
|
30 | 26, 29 | mpd 15 |
. . . . . . . . . . . 12
|
31 | 30 | expr 643 |
. . . . . . . . . . 11
|
32 | | simprl 794 |
. . . . . . . . . . . . . 14
|
33 | | simprr 796 |
. . . . . . . . . . . . . . 15
|
34 | 1, 4, 8, 3, 33 | btwncomand 32122 |
. . . . . . . . . . . . . 14
|
35 | 1, 3, 2, 4, 8, 32,
34 | btwnexchand 32133 |
. . . . . . . . . . . . 13
|
36 | 16 | adantr 481 |
. . . . . . . . . . . . 13
|
37 | 35, 36 | mpd 15 |
. . . . . . . . . . . 12
|
38 | 37 | expr 643 |
. . . . . . . . . . 11
|
39 | 22, 31, 38 | 3jaod 1392 |
. . . . . . . . . 10
|
40 | 11, 39 | sylbid 230 |
. . . . . . . . 9
|
41 | | brcolinear 32166 |
. . . . . . . . . . . 12
|
42 | 1, 8, 3, 2, 41 | syl13anc 1328 |
. . . . . . . . . . 11
|
43 | 42 | adantr 481 |
. . . . . . . . . 10
|
44 | | simprr 796 |
. . . . . . . . . . . . . 14
|
45 | | simprl 794 |
. . . . . . . . . . . . . 14
|
46 | 1, 3, 8, 2, 4, 44,
45 | btwnexchand 32133 |
. . . . . . . . . . . . 13
|
47 | | btwncolinear5 32180 |
. . . . . . . . . . . . . . 15
|
48 | 1, 3, 4, 8, 47 | syl13anc 1328 |
. . . . . . . . . . . . . 14
|
49 | 48 | adantr 481 |
. . . . . . . . . . . . 13
|
50 | 46, 49 | mpd 15 |
. . . . . . . . . . . 12
|
51 | 50 | expr 643 |
. . . . . . . . . . 11
|
52 | | simpl3r 1117 |
. . . . . . . . . . . . . . . 16
|
53 | 52 | necomd 2849 |
. . . . . . . . . . . . . . 15
|
54 | 53 | adantr 481 |
. . . . . . . . . . . . . 14
|
55 | | simprl 794 |
. . . . . . . . . . . . . . 15
|
56 | 1, 2, 3, 4, 55 | btwncomand 32122 |
. . . . . . . . . . . . . 14
|
57 | | simprr 796 |
. . . . . . . . . . . . . 14
|
58 | | btwnouttr2 32129 |
. . . . . . . . . . . . . . . 16
|
59 | 1, 4, 2, 3, 8, 58 | syl122anc 1335 |
. . . . . . . . . . . . . . 15
|
60 | 59 | adantr 481 |
. . . . . . . . . . . . . 14
|
61 | 54, 56, 57, 60 | mp3and 1427 |
. . . . . . . . . . . . 13
|
62 | | btwncolinear4 32179 |
. . . . . . . . . . . . . . 15
|
63 | 1, 4, 8, 3, 62 | syl13anc 1328 |
. . . . . . . . . . . . . 14
|
64 | 63 | adantr 481 |
. . . . . . . . . . . . 13
|
65 | 61, 64 | mpd 15 |
. . . . . . . . . . . 12
|
66 | 65 | expr 643 |
. . . . . . . . . . 11
|
67 | 52 | adantr 481 |
. . . . . . . . . . . . . 14
|
68 | | simprl 794 |
. . . . . . . . . . . . . 14
|
69 | | simprr 796 |
. . . . . . . . . . . . . . 15
|
70 | 1, 2, 8, 3, 69 | btwncomand 32122 |
. . . . . . . . . . . . . 14
|
71 | | btwnconn1 32208 |
. . . . . . . . . . . . . . . 16
|
72 | 1, 3, 2, 4, 8, 71 | syl122anc 1335 |
. . . . . . . . . . . . . . 15
|
73 | 72 | adantr 481 |
. . . . . . . . . . . . . 14
|
74 | 67, 68, 70, 73 | mp3and 1427 |
. . . . . . . . . . . . 13
|
75 | | btwncolinear3 32178 |
. . . . . . . . . . . . . . . 16
|
76 | 1, 3, 8, 4, 75 | syl13anc 1328 |
. . . . . . . . . . . . . . 15
|
77 | 76, 48 | jaod 395 |
. . . . . . . . . . . . . 14
|
78 | 77 | adantr 481 |
. . . . . . . . . . . . 13
|
79 | 74, 78 | mpd 15 |
. . . . . . . . . . . 12
|
80 | 79 | expr 643 |
. . . . . . . . . . 11
|
81 | 51, 66, 80 | 3jaod 1392 |
. . . . . . . . . 10
|
82 | 43, 81 | sylbid 230 |
. . . . . . . . 9
|
83 | 40, 82 | impbid 202 |
. . . . . . . 8
|
84 | 10 | adantr 481 |
. . . . . . . . . 10
|
85 | | simprr 796 |
. . . . . . . . . . . . . . 15
|
86 | 1, 8, 3, 4, 85 | btwncomand 32122 |
. . . . . . . . . . . . . 14
|
87 | | simprl 794 |
. . . . . . . . . . . . . 14
|
88 | 1, 4, 8, 3, 2, 86,
87 | btwnexch3and 32128 |
. . . . . . . . . . . . 13
|
89 | | btwncolinear2 32177 |
. . . . . . . . . . . . . . 15
|
90 | 1, 8, 2, 3, 89 | syl13anc 1328 |
. . . . . . . . . . . . . 14
|
91 | 90 | adantr 481 |
. . . . . . . . . . . . 13
|
92 | 88, 91 | mpd 15 |
. . . . . . . . . . . 12
|
93 | 92 | expr 643 |
. . . . . . . . . . 11
|
94 | | simpl23 1141 |
. . . . . . . . . . . . . . . 16
|
95 | 94 | necomd 2849 |
. . . . . . . . . . . . . . 15
|
96 | 95 | adantr 481 |
. . . . . . . . . . . . . 14
|
97 | | simprl 794 |
. . . . . . . . . . . . . 14
|
98 | | simprr 796 |
. . . . . . . . . . . . . 14
|
99 | | btwnconn2 32209 |
. . . . . . . . . . . . . . . 16
|
100 | 1, 4, 3, 2, 8, 99 | syl122anc 1335 |
. . . . . . . . . . . . . . 15
|
101 | 100 | adantr 481 |
. . . . . . . . . . . . . 14
|
102 | 96, 97, 98, 101 | mp3and 1427 |
. . . . . . . . . . . . 13
|
103 | 19 | adantr 481 |
. . . . . . . . . . . . 13
|
104 | 102, 103 | mpd 15 |
. . . . . . . . . . . 12
|
105 | 104 | expr 643 |
. . . . . . . . . . 11
|
106 | 94 | adantr 481 |
. . . . . . . . . . . . . 14
|
107 | | simprl 794 |
. . . . . . . . . . . . . . 15
|
108 | 1, 3, 4, 2, 107 | btwncomand 32122 |
. . . . . . . . . . . . . 14
|
109 | | simprr 796 |
. . . . . . . . . . . . . . 15
|
110 | 1, 4, 8, 3, 109 | btwncomand 32122 |
. . . . . . . . . . . . . 14
|
111 | | btwnouttr 32131 |
. . . . . . . . . . . . . . . 16
|
112 | 1, 2, 3, 4, 8, 111 | syl122anc 1335 |
. . . . . . . . . . . . . . 15
|
113 | 112 | adantr 481 |
. . . . . . . . . . . . . 14
|
114 | 106, 108,
110, 113 | mp3and 1427 |
. . . . . . . . . . . . 13
|
115 | 28 | adantr 481 |
. . . . . . . . . . . . 13
|
116 | 114, 115 | mpd 15 |
. . . . . . . . . . . 12
|
117 | 116 | expr 643 |
. . . . . . . . . . 11
|
118 | 93, 105, 117 | 3jaod 1392 |
. . . . . . . . . 10
|
119 | 84, 118 | sylbid 230 |
. . . . . . . . 9
|
120 | 42 | adantr 481 |
. . . . . . . . . 10
|
121 | | simprr 796 |
. . . . . . . . . . . . . . 15
|
122 | 1, 8, 3, 2, 121 | btwncomand 32122 |
. . . . . . . . . . . . . 14
|
123 | | simprl 794 |
. . . . . . . . . . . . . . 15
|
124 | 1, 3, 4, 2, 123 | btwncomand 32122 |
. . . . . . . . . . . . . 14
|
125 | 1, 2, 8, 3, 4, 122, 124 | btwnexch3and 32128 |
. . . . . . . . . . . . 13
|
126 | | btwncolinear2 32177 |
. . . . . . . . . . . . . . 15
|
127 | 1, 8, 4, 3, 126 | syl13anc 1328 |
. . . . . . . . . . . . . 14
|
128 | 127 | adantr 481 |
. . . . . . . . . . . . 13
|
129 | 125, 128 | mpd 15 |
. . . . . . . . . . . 12
|
130 | 129 | expr 643 |
. . . . . . . . . . 11
|
131 | 53 | adantr 481 |
. . . . . . . . . . . . . 14
|
132 | | simprl 794 |
. . . . . . . . . . . . . . 15
|
133 | 1, 3, 4, 2, 132 | btwncomand 32122 |
. . . . . . . . . . . . . 14
|
134 | | simprr 796 |
. . . . . . . . . . . . . 14
|
135 | | btwnconn2 32209 |
. . . . . . . . . . . . . . . 16
|
136 | 1, 2, 3, 4, 8, 135 | syl122anc 1335 |
. . . . . . . . . . . . . . 15
|
137 | 136 | adantr 481 |
. . . . . . . . . . . . . 14
|
138 | 131, 133,
134, 137 | mp3and 1427 |
. . . . . . . . . . . . 13
|
139 | 77 | adantr 481 |
. . . . . . . . . . . . 13
|
140 | 138, 139 | mpd 15 |
. . . . . . . . . . . 12
|
141 | 140 | expr 643 |
. . . . . . . . . . 11
|
142 | 52 | adantr 481 |
. . . . . . . . . . . . . 14
|
143 | | simprl 794 |
. . . . . . . . . . . . . 14
|
144 | | simprr 796 |
. . . . . . . . . . . . . . 15
|
145 | 1, 2, 8, 3, 144 | btwncomand 32122 |
. . . . . . . . . . . . . 14
|
146 | | btwnouttr 32131 |
. . . . . . . . . . . . . . . 16
|
147 | 1, 4, 3, 2, 8, 146 | syl122anc 1335 |
. . . . . . . . . . . . . . 15
|
148 | 147 | adantr 481 |
. . . . . . . . . . . . . 14
|
149 | 142, 143,
145, 148 | mp3and 1427 |
. . . . . . . . . . . . 13
|
150 | 63 | adantr 481 |
. . . . . . . . . . . . 13
|
151 | 149, 150 | mpd 15 |
. . . . . . . . . . . 12
|
152 | 151 | expr 643 |
. . . . . . . . . . 11
|
153 | 130, 141,
152 | 3jaod 1392 |
. . . . . . . . . 10
|
154 | 120, 153 | sylbid 230 |
. . . . . . . . 9
|
155 | 119, 154 | impbid 202 |
. . . . . . . 8
|
156 | 10 | adantr 481 |
. . . . . . . . . 10
|
157 | | simprr 796 |
. . . . . . . . . . . . . 14
|
158 | | simprl 794 |
. . . . . . . . . . . . . . 15
|
159 | 1, 4, 2, 3, 158 | btwncomand 32122 |
. . . . . . . . . . . . . 14
|
160 | 1, 3, 8, 4, 2, 157, 159 | btwnexchand 32133 |
. . . . . . . . . . . . 13
|
161 | 18 | adantr 481 |
. . . . . . . . . . . . 13
|
162 | 160, 161 | mpd 15 |
. . . . . . . . . . . 12
|
163 | 162 | expr 643 |
. . . . . . . . . . 11
|
164 | 95 | adantr 481 |
. . . . . . . . . . . . . 14
|
165 | | simprl 794 |
. . . . . . . . . . . . . 14
|
166 | | simprr 796 |
. . . . . . . . . . . . . 14
|
167 | | btwnouttr2 32129 |
. . . . . . . . . . . . . . . 16
|
168 | 1, 2, 4, 3, 8, 167 | syl122anc 1335 |
. . . . . . . . . . . . . . 15
|
169 | 168 | adantr 481 |
. . . . . . . . . . . . . 14
|
170 | 164, 165,
166, 169 | mp3and 1427 |
. . . . . . . . . . . . 13
|
171 | 28 | adantr 481 |
. . . . . . . . . . . . 13
|
172 | 170, 171 | mpd 15 |
. . . . . . . . . . . 12
|
173 | 172 | expr 643 |
. . . . . . . . . . 11
|
174 | 94 | adantr 481 |
. . . . . . . . . . . . . 14
|
175 | | simprl 794 |
. . . . . . . . . . . . . . 15
|
176 | 1, 4, 2, 3, 175 | btwncomand 32122 |
. . . . . . . . . . . . . 14
|
177 | | simprr 796 |
. . . . . . . . . . . . . . 15
|
178 | 1, 4, 8, 3, 177 | btwncomand 32122 |
. . . . . . . . . . . . . 14
|
179 | | btwnconn1 32208 |
. . . . . . . . . . . . . . . 16
|
180 | 1, 3, 4, 2, 8, 179 | syl122anc 1335 |
. . . . . . . . . . . . . . 15
|
181 | 180 | adantr 481 |
. . . . . . . . . . . . . 14
|
182 | 174, 176,
178, 181 | mp3and 1427 |
. . . . . . . . . . . . 13
|
183 | 19 | adantr 481 |
. . . . . . . . . . . . 13
|
184 | 182, 183 | mpd 15 |
. . . . . . . . . . . 12
|
185 | 184 | expr 643 |
. . . . . . . . . . 11
|
186 | 163, 173,
185 | 3jaod 1392 |
. . . . . . . . . 10
|
187 | 156, 186 | sylbid 230 |
. . . . . . . . 9
|
188 | 42 | adantr 481 |
. . . . . . . . . 10
|
189 | | simprl 794 |
. . . . . . . . . . . . . . 15
|
190 | 1, 4, 2, 3, 189 | btwncomand 32122 |
. . . . . . . . . . . . . 14
|
191 | | simprr 796 |
. . . . . . . . . . . . . 14
|
192 | | btwnconn3 32210 |
. . . . . . . . . . . . . . . 16
|
193 | 1, 3, 4, 8, 2, 192 | syl122anc 1335 |
. . . . . . . . . . . . . . 15
|
194 | 193 | adantr 481 |
. . . . . . . . . . . . . 14
|
195 | 190, 191,
194 | mp2and 715 |
. . . . . . . . . . . . 13
|
196 | 77 | adantr 481 |
. . . . . . . . . . . . 13
|
197 | 195, 196 | mpd 15 |
. . . . . . . . . . . 12
|
198 | 197 | expr 643 |
. . . . . . . . . . 11
|
199 | | simprl 794 |
. . . . . . . . . . . . . 14
|
200 | | simprr 796 |
. . . . . . . . . . . . . 14
|
201 | 1, 2, 4, 3, 8, 199, 200 | btwnexch3and 32128 |
. . . . . . . . . . . . 13
|
202 | 63 | adantr 481 |
. . . . . . . . . . . . 13
|
203 | 201, 202 | mpd 15 |
. . . . . . . . . . . 12
|
204 | 203 | expr 643 |
. . . . . . . . . . 11
|
205 | | simprl 794 |
. . . . . . . . . . . . . . 15
|
206 | 1, 4, 2, 3, 205 | btwncomand 32122 |
. . . . . . . . . . . . . 14
|
207 | | simprr 796 |
. . . . . . . . . . . . . . 15
|
208 | 1, 2, 8, 3, 207 | btwncomand 32122 |
. . . . . . . . . . . . . 14
|
209 | 1, 3, 4, 2, 8, 206, 208 | btwnexchand 32133 |
. . . . . . . . . . . . 13
|
210 | 76 | adantr 481 |
. . . . . . . . . . . . 13
|
211 | 209, 210 | mpd 15 |
. . . . . . . . . . . 12
|
212 | 211 | expr 643 |
. . . . . . . . . . 11
|
213 | 198, 204,
212 | 3jaod 1392 |
. . . . . . . . . 10
|
214 | 188, 213 | sylbid 230 |
. . . . . . . . 9
|
215 | 187, 214 | impbid 202 |
. . . . . . . 8
|
216 | 83, 155, 215 | 3jaodan 1394 |
. . . . . . 7
|
217 | 7, 216 | syldan 487 |
. . . . . 6
|
218 | 217 | adantrl 752 |
. . . . 5
|
219 | 218 | an32s 846 |
. . . 4
|
220 | 219 | rabbidva 3188 |
. . 3
|
221 | 220 | ex 450 |
. 2
|
222 | | fvline2 32253 |
. . . . 5
Line |
223 | 222 | 3adant3 1081 |
. . . 4
Line |
224 | 223 | eleq2d 2687 |
. . 3
Line
|
225 | | breq1 4656 |
. . . 4
|
226 | 225 | elrab 3363 |
. . 3
|
227 | 224, 226 | syl6bb 276 |
. 2
Line
|
228 | | simp1 1061 |
. . . 4
|
229 | | simp21 1094 |
. . . 4
|
230 | | simp3l 1089 |
. . . 4
|
231 | | simp3r 1090 |
. . . 4
|
232 | | fvline2 32253 |
. . . 4
Line |
233 | 228, 229,
230, 231, 232 | syl13anc 1328 |
. . 3
Line |
234 | 223, 233 | eqeq12d 2637 |
. 2
Line Line
|
235 | 221, 227,
234 | 3imtr4d 283 |
1
Line Line Line |