Theorem elioore 12423

Description: A member of an open interval of reals is a real. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 3-Nov-2013.)

Assertion

Ref	Expression
elioore	⊢ (𝐴 ∈ (𝐵(,)𝐶) → 𝐴 ∈ ℝ)

Proof of Theorem elioore

Step	Hyp	Ref	Expression
1		elioo3g 12422	. 2 ⊢ (𝐴 ∈ (𝐵(,)𝐶) ↔ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) ∧ (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)))
2		3ancomb 1114	. . 3 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) ↔ (𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ*))
3		xrre2 12219	. . 3 ⊢ (((𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) → 𝐴 ∈ ℝ)
4	2, 3	sylanb 572	. 2 ⊢ (((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) ∧ (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) → 𝐴 ∈ ℝ)
5	1, 4	sylbi 208	1 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1100   ∈ wcel 2156   class class class wbr 4844  (class class class)co 6874  ℝcr 10220  ℝ^*cxr 10358   < clt 10359  (,)cioo 12393

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-cnex 10277  ax-resscn 10278  ax-pre-lttri 10295  ax-pre-lttrn 10296

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-po 5232  df-so 5233  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-1st 7398  df-2nd 7399  df-er 7979  df-en 8193  df-dom 8194  df-sdom 8195  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-ioo 12397

This theorem is referenced by:  iooval2  12426  elioo4g  12452  ioossre  12453  zltaddlt1le  12547  tgioo  22812  zcld  22829  ioorcl2  23553  lhop2  23992  dvcvx  23997  pilem2  24420  pilem3  24421  pilem3OLD  24422  pire  24425  tanrpcl  24471  tangtx  24472  tanabsge  24473  sinq34lt0t  24476  cosq14gt0  24477  sineq0  24488  cosne0  24491  tanord  24499  divlogrlim  24595  logno1  24596  logccv  24623  angpieqvd  24772  asinsin  24833  reasinsin  24837  scvxcvx  24926  basellem3  25023  basellem8  25028  vmalogdivsum2  25441  vmalogdivsum  25442  2vmadivsumlem  25443  selberg3lem1  25460  selberg3  25462  selberg4lem1  25463  selberg4  25464  selberg3r  25472  selberg4r  25473  selberg34r  25474  pntrlog2bndlem1  25480  pntrlog2bndlem2  25481  pntrlog2bndlem3  25482  pntrlog2bndlem4  25483  pntrlog2bndlem5  25484  pntrlog2bndlem6a  25485  pntrlog2bndlem6  25486  pntpbnd  25491  pntibndlem3  25495  pntibnd  25496  knoppndvlem3  32822  iooelexlt  33526  relowlssretop  33527  relowlpssretop  33528  tan2h  33714  itg2gt0cn  33777  itggt0cn  33794  ftc1cnnclem  33795  ftc1cnnc  33796  ftc1anclem7  33803  ftc1anclem8  33804  ftc1anc  33805  dvasin  33808  areacirclem1  33812  areacirc  33817  cvgdvgrat  39012  iooabslt  40205  iocopn  40227  iooshift  40229  icoopn  40232  iooiinicc  40249  elioored  40256  iooiinioc  40263  islptre  40331  limciccioolb  40333  limcicciooub  40349  lptre2pt  40352  xlimxrre  40537  sinaover2ne0  40559  icccncfext  40580  cncfiooicclem1  40586  dvbdfbdioolem2  40624  itgcoscmulx  40664  iblcncfioo  40673  wallispilem1  40761  dirkeritg  40798  dirkercncflem2  40800  fourierdlem27  40830  fourierdlem28  40831  fourierdlem31  40834  fourierdlem32  40835  fourierdlem33  40836  fourierdlem39  40842  fourierdlem40  40843  fourierdlem41  40844  fourierdlem47  40849  fourierdlem48  40850  fourierdlem49  40851  fourierdlem56  40858  fourierdlem57  40859  fourierdlem59  40861  fourierdlem60  40862  fourierdlem61  40863  fourierdlem62  40864  fourierdlem64  40866  fourierdlem68  40870  fourierdlem72  40874  fourierdlem73  40875  fourierdlem74  40876  fourierdlem75  40877  fourierdlem76  40878  fourierdlem78  40880  fourierdlem81  40883  fourierdlem84  40886  fourierdlem89  40891  fourierdlem90  40892  fourierdlem91  40893  fourierdlem92  40894  fourierdlem93  40895  fourierdlem97  40899  fourierdlem100  40902  fourierdlem101  40903  fourierdlem103  40905  fourierdlem104  40906  fourierdlem111  40913  fourierdlem112  40914  sqwvfoura  40924  sqwvfourb  40925  fouriersw  40927  etransclem23  40953  etransclem46  40976  smfaddlem1  41453  amgmwlem  43119