MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elioc2 Structured version   Visualization version   GIF version

Theorem elioc2 13338
Description: Membership in an open-below, closed-above real interval. (Contributed by Paul Chapman, 30-Dec-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
Assertion
Ref Expression
elioc2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶𝐶𝐵)))

Proof of Theorem elioc2
StepHypRef Expression
1 rexr 11211 . . 3 (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
2 elioc1 13317 . . 3 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)))
31, 2sylan2 594 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)))
4 mnfxr 11222 . . . . . . . 8 -∞ ∈ ℝ*
54a1i 11 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → -∞ ∈ ℝ*)
6 simpll 766 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → 𝐴 ∈ ℝ*)
7 simpr1 1195 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → 𝐶 ∈ ℝ*)
8 mnfle 13065 . . . . . . . 8 (𝐴 ∈ ℝ* → -∞ ≤ 𝐴)
98ad2antrr 725 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → -∞ ≤ 𝐴)
10 simpr2 1196 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → 𝐴 < 𝐶)
115, 6, 7, 9, 10xrlelttrd 13090 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → -∞ < 𝐶)
121ad2antlr 726 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → 𝐵 ∈ ℝ*)
13 pnfxr 11219 . . . . . . . 8 +∞ ∈ ℝ*
1413a1i 11 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → +∞ ∈ ℝ*)
15 simpr3 1197 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → 𝐶𝐵)
16 ltpnf 13051 . . . . . . . 8 (𝐵 ∈ ℝ → 𝐵 < +∞)
1716ad2antlr 726 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → 𝐵 < +∞)
187, 12, 14, 15, 17xrlelttrd 13090 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → 𝐶 < +∞)
19 xrrebnd 13098 . . . . . . 7 (𝐶 ∈ ℝ* → (𝐶 ∈ ℝ ↔ (-∞ < 𝐶𝐶 < +∞)))
207, 19syl 17 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → (𝐶 ∈ ℝ ↔ (-∞ < 𝐶𝐶 < +∞)))
2111, 18, 20mpbir2and 712 . . . . 5 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → 𝐶 ∈ ℝ)
2221, 10, 153jca 1129 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶𝐶𝐵))
2322ex 414 . . 3 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → ((𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵) → (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶𝐶𝐵)))
24 rexr 11211 . . . 4 (𝐶 ∈ ℝ → 𝐶 ∈ ℝ*)
25243anim1i 1153 . . 3 ((𝐶 ∈ ℝ ∧ 𝐴 < 𝐶𝐶𝐵) → (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵))
2623, 25impbid1 224 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → ((𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶𝐶𝐵)))
273, 26bitrd 279 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶𝐶𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088  wcel 2107   class class class wbr 5111  (class class class)co 7363  cr 11060  +∞cpnf 11196  -∞cmnf 11197  *cxr 11198   < clt 11199  cle 11200  (,]cioc 13276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2703  ax-sep 5262  ax-nul 5269  ax-pow 5326  ax-pr 5390  ax-un 7678  ax-cnex 11117  ax-resscn 11118  ax-pre-lttri 11135  ax-pre-lttrn 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4289  df-if 4493  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4872  df-br 5112  df-opab 5174  df-mpt 5195  df-id 5537  df-po 5551  df-so 5552  df-xp 5645  df-rel 5646  df-cnv 5647  df-co 5648  df-dm 5649  df-rn 5650  df-res 5651  df-ima 5652  df-iota 6454  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-ov 7366  df-oprab 7367  df-mpo 7368  df-er 8656  df-en 8892  df-dom 8893  df-sdom 8894  df-pnf 11201  df-mnf 11202  df-xr 11203  df-ltxr 11204  df-le 11205  df-ioc 13280
This theorem is referenced by:  iocssre  13355  ef01bndlem  16078  sin01bnd  16079  cos01bnd  16080  cos1bnd  16081  sinltx  16083  sin01gt0  16084  cos01gt0  16085  sin02gt0  16086  sincos1sgn  16087  sincos2sgn  16088  icoopnst  24340  iocopnst  24341  ismbf3d  25056  aaliou3lem2  25741  aaliou3lem3  25742  pilem2  25849  sinhalfpilem  25858  sincosq1lem  25892  coseq0negpitopi  25898  tangtx  25900  sincos4thpi  25908  efif1olem1  25936  efif1olem2  25937  efif1o  25940  efifo  25941  ellogrn  25953  logimclad  25966  ellogdm  26032  logdmnrp  26034  dvloglem  26041  dvlog2lem  26045  asinneg  26274  atans2  26319  ressatans  26322  abvcxp  27001  ostth2  27023  xrge0iifcv  32605  xrge0iifiso  32606  xrge0iifhom  32608  sinccvglem  34348  bj-pinftyccb  35766  bj-pinftynminfty  35772  dvasin  36236  areacirclem4  36243  gtnelioc  43831  limcicciooub  43980  fourierdlem4  44454  fourierdlem26  44476  fourierdlem33  44483  fourierdlem37  44487  fourierdlem65  44514  fourierdlem79  44528  fouriersw  44574  eenglngeehlnmlem1  46925  eenglngeehlnmlem2  46926  io1ii  47055  sepfsepc  47062
  Copyright terms: Public domain W3C validator