Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  outsideofrflx Structured version   Visualization version   GIF version

Theorem outsideofrflx 36069
Description: Reflexivity of outsideness. Theorem 6.5 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
Assertion
Ref Expression
outsideofrflx ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝐴𝑃𝑃OutsideOf⟨𝐴, 𝐴⟩))

Proof of Theorem outsideofrflx
StepHypRef Expression
1 axbtwnid 28951 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝐴, 𝐴⟩ → 𝑃 = 𝐴))
2 eqcom 2740 . . . . 5 (𝑃 = 𝐴𝐴 = 𝑃)
31, 2imbitrdi 251 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝐴, 𝐴⟩ → 𝐴 = 𝑃))
43necon3ad 2949 . . 3 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝐴𝑃 → ¬ 𝑃 Btwn ⟨𝐴, 𝐴⟩))
5 colineartriv2 36010 . . 3 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → 𝑃 Colinear ⟨𝐴, 𝐴⟩)
64, 5jctild 525 . 2 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝐴𝑃 → (𝑃 Colinear ⟨𝐴, 𝐴⟩ ∧ ¬ 𝑃 Btwn ⟨𝐴, 𝐴⟩)))
7 broutsideof 36063 . 2 (𝑃OutsideOf⟨𝐴, 𝐴⟩ ↔ (𝑃 Colinear ⟨𝐴, 𝐴⟩ ∧ ¬ 𝑃 Btwn ⟨𝐴, 𝐴⟩))
86, 7imbitrrdi 252 1 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝐴𝑃𝑃OutsideOf⟨𝐴, 𝐴⟩))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  w3a 1085   = wceq 1535  wcel 2104  wne 2936  cop 4637   class class class wbr 5150  cfv 6559  cn 12258  𝔼cee 28900   Btwn cbtwn 28901   Colinear ccolin 35979  OutsideOfcoutsideof 36061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1963  ax-7 2003  ax-8 2106  ax-9 2114  ax-10 2137  ax-11 2153  ax-12 2173  ax-ext 2704  ax-rep 5287  ax-sep 5301  ax-nul 5308  ax-pow 5367  ax-pr 5431  ax-un 7748  ax-inf2 9673  ax-cnex 11203  ax-resscn 11204  ax-1cn 11205  ax-icn 11206  ax-addcl 11207  ax-addrcl 11208  ax-mulcl 11209  ax-mulrcl 11210  ax-mulcom 11211  ax-addass 11212  ax-mulass 11213  ax-distr 11214  ax-i2m1 11215  ax-1ne0 11216  ax-1rid 11217  ax-rnegex 11218  ax-rrecex 11219  ax-cnre 11220  ax-pre-lttri 11221  ax-pre-lttrn 11222  ax-pre-ltadd 11223  ax-pre-mulgt0 11224  ax-pre-sup 11225
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1538  df-fal 1548  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2536  df-eu 2565  df-clab 2711  df-cleq 2725  df-clel 2812  df-nfc 2888  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3479  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4916  df-int 4955  df-iun 5001  df-br 5151  df-opab 5213  df-mpt 5234  df-tr 5268  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-se 5637  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6318  df-ord 6384  df-on 6385  df-lim 6386  df-suc 6387  df-iota 6511  df-fun 6561  df-fn 6562  df-f 6563  df-f1 6564  df-fo 6565  df-f1o 6566  df-fv 6567  df-isom 6568  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7882  df-1st 8008  df-2nd 8009  df-frecs 8300  df-wrecs 8331  df-recs 8405  df-rdg 8444  df-1o 8500  df-er 8739  df-map 8862  df-en 8980  df-dom 8981  df-sdom 8982  df-fin 8983  df-sup 9474  df-oi 9542  df-card 9971  df-pnf 11289  df-mnf 11290  df-xr 11291  df-ltxr 11292  df-le 11293  df-sub 11486  df-neg 11487  df-div 11913  df-nn 12259  df-2 12321  df-3 12322  df-n0 12519  df-z 12606  df-uz 12871  df-rp 13027  df-ico 13384  df-icc 13385  df-fz 13539  df-fzo 13683  df-seq 14030  df-exp 14090  df-hash 14357  df-cj 15125  df-re 15126  df-im 15127  df-sqrt 15261  df-abs 15262  df-clim 15511  df-sum 15710  df-ee 28903  df-btwn 28904  df-cgr 28905  df-colinear 35981  df-outsideof 36062
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator