Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nbssntrs Unicode version

Theorem nbssntrs 26147
 Description: IF and are not on the same side, and and are not on the same side then and are on the same side. (For my private use only. Don't use.) (Contributed by FL, 14-Jul-2016.)
Hypotheses
Ref Expression
bsstrs.1 PPoints
bsstrs.2 PLines
bsstrs.3
bsstrs.4 Ibg
bsstrs.5
nbssntrs.6
nbssntrs.7
nbssntrs.8
nbssntrs.9
nbssntrs.10
Assertion
Ref Expression
nbssntrs

Proof of Theorem nbssntrs
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bsstrs.1 . . . . . 6 PPoints
2 bsstrs.3 . . . . . 6
3 bsstrs.4 . . . . . . 7 Ibg
43adantl 452 . . . . . 6 Ibg
5 nbssntrs.6 . . . . . . . 8
6 eldifi 3298 . . . . . . . 8
75, 6syl 15 . . . . . . 7
87adantl 452 . . . . . 6
9 eqid 2283 . . . . . 6 btw btw
10 nbssntrs.8 . . . . . . . 8
11 eldifi 3298 . . . . . . . 8
1210, 11syl 15 . . . . . . 7
1312adantl 452 . . . . . 6
14 df-ne 2448 . . . . . . . . 9
1514biimpri 197 . . . . . . . 8
16153ad2ant2 977 . . . . . . 7
1716adantr 451 . . . . . 6
181, 2, 4, 8, 9, 13, 17sgplpte21 26132 . . . . 5 btw
1918ineq1d 3369 . . . 4 btw
20 inrab2 3441 . . . . 5 btw btw
21 incom 3361 . . . . . . . . . . 11 btw btw
22 bsstrs.2 . . . . . . . . . . . 12 PLines
23 bsstrs.5 . . . . . . . . . . . . 13
2423adantl 452 . . . . . . . . . . . 12
255adantl 452 . . . . . . . . . . . 12
26 nbssntrs.7 . . . . . . . . . . . . 13
2726adantl 452 . . . . . . . . . . . 12
2810adantl 452 . . . . . . . . . . . 12
29 nbssntrs.9 . . . . . . . . . . . . . 14
303adantr 451 . . . . . . . . . . . . . . . . . . . 20 Ibg
317adantr 451 . . . . . . . . . . . . . . . . . . . 20
32 eldifi 3298 . . . . . . . . . . . . . . . . . . . . . 22
3326, 32syl 15 . . . . . . . . . . . . . . . . . . . . 21
3433adantr 451 . . . . . . . . . . . . . . . . . . . 20
35 df-ne 2448 . . . . . . . . . . . . . . . . . . . . . . 23
3635biimpri 197 . . . . . . . . . . . . . . . . . . . . . 22
37363ad2ant3 978 . . . . . . . . . . . . . . . . . . . . 21
3837adantl 452 . . . . . . . . . . . . . . . . . . . 20
391, 2, 30, 31, 9, 34, 38sgplpte21 26132 . . . . . . . . . . . . . . . . . . 19 btw
4039ineq1d 3369 . . . . . . . . . . . . . . . . . 18 btw
41 inrab2 3441 . . . . . . . . . . . . . . . . . 18 btw btw
4240, 41syl6eq 2331 . . . . . . . . . . . . . . . . 17 btw
43 neeq1 2454 . . . . . . . . . . . . . . . . . 18 btw btw
44 rabn0 3474 . . . . . . . . . . . . . . . . . . 19 btw btw
45 elin 3358 . . . . . . . . . . . . . . . . . . . . . . . 24
46 elin 3358 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 btw btw
47 ne0i 3461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 btw btw
4847a1d 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 btw btw
4946, 48sylbir 204 . . . . . . . . . . . . . . . . . . . . . . . . . 26 btw btw
5049expcom 424 . . . . . . . . . . . . . . . . . . . . . . . . 25 btw btw
5150adantl 452 . . . . . . . . . . . . . . . . . . . . . . . 24 btw btw
5245, 51sylbi 187 . . . . . . . . . . . . . . . . . . . . . . 23 btw btw
5352com12 27 . . . . . . . . . . . . . . . . . . . . . 22 btw btw
54 eleq1 2343 . . . . . . . . . . . . . . . . . . . . . . 23
55 elin 3358 . . . . . . . . . . . . . . . . . . . . . . . 24
56 eldifn 3299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
575, 56syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5857pm2.21d 98 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 btw
5958adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26 btw
6059com12 27 . . . . . . . . . . . . . . . . . . . . . . . . 25 btw
6160adantl 452 . . . . . . . . . . . . . . . . . . . . . . . 24 btw
6255, 61sylbi 187 . . . . . . . . . . . . . . . . . . . . . . 23 btw
6354, 62syl6bi 219 . . . . . . . . . . . . . . . . . . . . . 22 btw
64 eleq1 2343 . . . . . . . . . . . . . . . . . . . . . . 23
65 elin 3358 . . . . . . . . . . . . . . . . . . . . . . . 24
66 eldifn 3299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6726, 66syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6867pm2.21d 98 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 btw
6968adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26 btw
7069com12 27 . . . . . . . . . . . . . . . . . . . . . . . . 25 btw
7170adantl 452 . . . . . . . . . . . . . . . . . . . . . . . 24 btw
7265, 71sylbi 187 . . . . . . . . . . . . . . . . . . . . . . 23 btw
7364, 72syl6bi 219 . . . . . . . . . . . . . . . . . . . . . 22 btw
7453, 63, 733jaoi 1245 . . . . . . . . . . . . . . . . . . . . 21 btw btw
7574com12 27 . . . . . . . . . . . . . . . . . . . 20 btw btw
7675rexlimiv 2661 . . . . . . . . . . . . . . . . . . 19 btw btw
7744, 76sylbi 187 . . . . . . . . . . . . . . . . . 18 btw btw
7843, 77syl6bi 219 . . . . . . . . . . . . . . . . 17 btw btw
7942, 78syl 15 . . . . . . . . . . . . . . . 16 btw
8079pm2.43a 45 . . . . . . . . . . . . . . 15 btw
8180ex 423 . . . . . . . . . . . . . 14 btw
8229, 81mpid 37 . . . . . . . . . . . . 13 btw
8382impcom 419 . . . . . . . . . . . 12 btw
84 nbssntrs.10 . . . . . . . . . . . . . 14
8512adantr 451 . . . . . . . . . . . . . . . . . . . . 21
86 df-ne 2448 . . . . . . . . . . . . . . . . . . . . . . . 24
8786biimpri 197 . . . . . . . . . . . . . . . . . . . . . . 23
88873ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . 22
8988adantl 452 . . . . . . . . . . . . . . . . . . . . 21
901, 2, 30, 34, 9, 85, 89sgplpte21 26132 . . . . . . . . . . . . . . . . . . . 20 btw
9190ineq1d 3369 . . . . . . . . . . . . . . . . . . 19 btw
92 inrab2 3441 . . . . . . . . . . . . . . . . . . 19 btw btw
9391, 92syl6eq 2331 . . . . . . . . . . . . . . . . . 18 btw
94 neeq1 2454 . . . . . . . . . . . . . . . . . . 19 btw btw
95 rabn0 3474 . . . . . . . . . . . . . . . . . . . 20 btw btw
96 elin 3358 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 btw btw
97 ne0i 3461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 btw btw
9897a1ii 24 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 btw btw
9998com3r 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 btw btw
10096, 99sylbir 204 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 btw btw
101100expcom 424 . . . . . . . . . . . . . . . . . . . . . . . . . 26 btw btw
102101adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . 25 btw btw
10345, 102sylbi 187 . . . . . . . . . . . . . . . . . . . . . . . 24 btw btw
104103com12 27 . . . . . . . . . . . . . . . . . . . . . . 23 btw btw
10567pm2.21d 98 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 btw
106105adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 btw
107106com12 27 . . . . . . . . . . . . . . . . . . . . . . . . . 26 btw
108107adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . 25 btw
10965, 108sylbi 187 . . . . . . . . . . . . . . . . . . . . . . . 24 btw
11064, 109syl6bi 219 . . . . . . . . . . . . . . . . . . . . . . 23 btw
111 eleq1 2343 . . . . . . . . . . . . . . . . . . . . . . . 24
112 elin 3358 . . . . . . . . . . . . . . . . . . . . . . . . 25
113 eldifn 3299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
11410, 113syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
115114pm2.21d 98 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 btw
116115adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 btw
117116com12 27 . . . . . . . . . . . . . . . . . . . . . . . . . 26 btw
118117adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . 25 btw
119112, 118sylbi 187 . . . . . . . . . . . . . . . . . . . . . . . 24 btw
120111, 119syl6bi 219 . . . . . . . . . . . . . . . . . . . . . . 23 btw
121104, 110, 1203jaoi 1245 . . . . . . . . . . . . . . . . . . . . . 22 btw btw
122121com12 27 . . . . . . . . . . . . . . . . . . . . 21 btw btw
123122rexlimiv 2661 . . . . . . . . . . . . . . . . . . . 20 btw btw
12495, 123sylbi 187 . . . . . . . . . . . . . . . . . . 19 btw btw
12594, 124syl6bi 219 . . . . . . . . . . . . . . . . . 18 btw btw
12693, 125syl 15 . . . . . . . . . . . . . . . . 17 btw
127126pm2.43a 45 . . . . . . . . . . . . . . . 16 btw
128127ex 423 . . . . . . . . . . . . . . 15 btw
12984, 128mpid 37 . . . . . . . . . . . . . 14 btw
13084, 129mpid 37 . . . . . . . . . . . . 13 btw
131130impcom 419 . . . . . . . . . . . 12 btw
1321, 22, 9, 4, 24, 25, 27, 28, 83, 131nbssntr 26129 . . . . . . . . . . 11 btw
13321, 132syl5eq 2327 . . . . . . . . . 10 btw
134 disj 3495 . . . . . . . . . 10 btw btw
135133, 134sylib 188 . . . . . . . . 9 btw
136 risset 2590 . . . . . . . . . . . 12
13757, 136sylnib 295 . . . . . . . . . . 11
138137adantl 452 . . . . . . . . . 10
139 ralnex 2553 . . . . . . . . . 10
140138, 139sylibr 203 . . . . . . . . 9
141114adantl 452 . . . . . . . . . . 11
142 risset 2590 . . . . . . . . . . 11
143141, 142sylnib 295 . . . . . . . . . 10
144 ralnex 2553 . . . . . . . . . 10
145143, 144sylibr 203 . . . . . . . . 9
146 r19.26-3 2677 . . . . . . . . 9 btw btw
147135, 140, 145, 146syl3anbrc 1136 . . . . . . . 8 btw
148 inss2 3390 . . . . . . . . . . . . 13
149148a1i 10 . . . . . . . . . . . 12
150149sseld 3179 . . . . . . . . . . 11
151150imim1d 69 . . . . . . . . . 10 btw btw
152151adantl 452 . . . . . . . . 9 btw btw
153152ralimdv2 2623 . . . . . . . 8 btw btw
154147, 153mpd 14 . . . . . . 7 btw
155 3ioran 950 . . . . . . . . 9 btw btw
156155a1i 10 . . . . . . . 8 btw btw
157156ralbidv 2563 . . . . . . 7 btw btw
158154, 157mpbird 223 . . . . . 6 btw
159 rabeq0 3476 . . . . . 6 btw btw
160158, 159sylibr 203 . . . . 5 btw
16120, 160syl5eq 2327 . . . 4 btw
16219, 161eqtrd 2315 . . 3
1631623exp1 1167 . 2
164 oveq1 5865 . . . . . . . 8
165164ineq1d 3369 . . . . . . 7
166165neeq1d 2459 . . . . . 6
1671, 2, 3, 12sgplpte22 26138 . . . . . . . . . . 11
168167ineq1d 3369 . . . . . . . . . 10
169168neeq1d 2459 . . . . . . . . 9
170 df-ne 2448 . . . . . . . . . 10
171 incom 3361 . . . . . . . . . . . 12
172171eqeq1i 2290 . . . . . . . . . . 11
173 disjsn 3693 . . . . . . . . . . . 12
174 notnot2 104 . . . . . . . . . . . 12
175173, 174sylnbi 297 . . . . . . . . . . 11
176172, 175sylnbi 297 . . . . . . . . . 10
177170, 176sylbi 187 . . . . . . . . 9
178169, 177syl6bi 219 . . . . . . . 8
179114pm2.21d 98 . . . . . . . 8
180178, 179syld 40 . . . . . . 7
181180com12 27 . . . . . 6
182166, 181syl6bi 219 . . . . 5
183182com3l 75 . . . 4
18484, 183mpcom 32 . . 3
185184com12 27 . 2
1861, 2, 3, 7sgplpte22 26138 . . . 4
187 incom 3361 . . . . . 6
188 disjsn 3693 . . . . . . 7
18957, 188sylibr 203 . . . . . 6
190187, 189syl5eq 2327 . . . . 5
191 ineq1 3363 . . . . . 6
192191eqeq1d 2291 . . . . 5
193190, 192syl5ibr 212 . . . 4
194186, 193mpcom 32 . . 3
195 oveq2 5866 . . . . . 6
196195eqcoms 2286 . . . . 5
197196ineq1d 3369 . . . 4
198197eqeq1d 2291 . . 3
199194, 198syl5ibr 212 . 2
200 oveq1 5865 . . . . . . . 8
201200ineq1d 3369 . . . . . . 7
202201neeq1d 2459 . . . . . 6
2031, 2, 3, 33sgplpte22 26138 . . . . . . . 8
204 ineq1 3363 . . . . . . . . . . 11
205204neeq1d 2459 . . . . . . . . . 10
206 incom 3361 . . . . . . . . . . . 12
207206neeq1i 2456 . . . . . . . . . . 11
208 disjsn 3693 . . . . . . . . . . . . . 14
209208bicomi 193 . . . . . . . . . . . . 13
210209necon3bbii 2477 . . . . . . . . . . . 12
211 notnot2 104 . . . . . . . . . . . . 13
21267pm2.21d 98 . . . . . . . . . . . . . 14
213212com12 27 . . . . . . . . . . . . 13
214211, 213syl 15 . . . . . . . . . . . 12
215210, 214sylbir 204 . . . . . . . . . . 11
216207, 215sylbi 187 . . . . . . . . . 10
217205, 216syl6bi 219 . . . . . . . . 9
218217com23 72 . . . . . . . 8
219203, 218mpcom 32 . . . . . . 7
220219com12 27 . . . . . 6
221202, 220syl6bi 219 . . . . 5
222221com3l 75 . . . 4
22329, 222mpcom 32 . . 3
224223com12 27 . 2
225163, 185, 199, 224pm2.61iii 159 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wa 358   w3o 933   w3a 934   wceq 1623   wcel 1684   wne 2446  wral 2543  wrex 2544  crab 2547   cdif 3149   cin 3151   wss 3152  c0 3455  csn 3640  cfv 5255  (class class class)co 5858  PPointscpoints 26056  PLinescplines 26058  btwcbtw 26106  Ibgcibg 26107  cseg 26130 This theorem is referenced by:  pdiveql  26168 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-ibg2 26109  df-seg2 26131
 Copyright terms: Public domain W3C validator