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

Theorem elioc2 12791
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 10679 . . 3 (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
2 elioc1 12772 . . 3 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)))
31, 2sylan2 594 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)))
4 mnfxr 10690 . . . . . . . 8 -∞ ∈ ℝ*
54a1i 11 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → -∞ ∈ ℝ*)
6 simpll 765 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → 𝐴 ∈ ℝ*)
7 simpr1 1188 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → 𝐶 ∈ ℝ*)
8 mnfle 12521 . . . . . . . 8 (𝐴 ∈ ℝ* → -∞ ≤ 𝐴)
98ad2antrr 724 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → -∞ ≤ 𝐴)
10 simpr2 1189 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → 𝐴 < 𝐶)
115, 6, 7, 9, 10xrlelttrd 12545 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → -∞ < 𝐶)
121ad2antlr 725 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → 𝐵 ∈ ℝ*)
13 pnfxr 10687 . . . . . . . 8 +∞ ∈ ℝ*
1413a1i 11 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → +∞ ∈ ℝ*)
15 simpr3 1190 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → 𝐶𝐵)
16 ltpnf 12507 . . . . . . . 8 (𝐵 ∈ ℝ → 𝐵 < +∞)
1716ad2antlr 725 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → 𝐵 < +∞)
187, 12, 14, 15, 17xrlelttrd 12545 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → 𝐶 < +∞)
19 xrrebnd 12553 . . . . . . 7 (𝐶 ∈ ℝ* → (𝐶 ∈ ℝ ↔ (-∞ < 𝐶𝐶 < +∞)))
207, 19syl 17 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → (𝐶 ∈ ℝ ↔ (-∞ < 𝐶𝐶 < +∞)))
2111, 18, 20mpbir2and 711 . . . . 5 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → 𝐶 ∈ ℝ)
2221, 10, 153jca 1122 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)) → (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶𝐶𝐵))
2322ex 415 . . 3 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → ((𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵) → (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶𝐶𝐵)))
24 rexr 10679 . . . 4 (𝐶 ∈ ℝ → 𝐶 ∈ ℝ*)
25243anim1i 1146 . . 3 ((𝐶 ∈ ℝ ∧ 𝐴 < 𝐶𝐶𝐵) → (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵))
2623, 25impbid1 227 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → ((𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶𝐶𝐵)))
273, 26bitrd 281 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶𝐶𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  w3a 1081  wcel 2107   class class class wbr 5057  (class class class)co 7148  cr 10528  +∞cpnf 10664  -∞cmnf 10665  *cxr 10666   < clt 10667  cle 10668  (,]cioc 12731
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586  ax-pre-lttri 10603  ax-pre-lttrn 10604
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7151  df-oprab 7152  df-mpo 7153  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-ioc 12735
This theorem is referenced by:  iocssre  12808  ef01bndlem  15529  sin01bnd  15530  cos01bnd  15531  cos1bnd  15532  sinltx  15534  sin01gt0  15535  cos01gt0  15536  sin02gt0  15537  sincos1sgn  15538  sincos2sgn  15539  icoopnst  23535  iocopnst  23536  ismbf3d  24247  aaliou3lem2  24924  aaliou3lem3  24925  pilem2  25032  sinhalfpilem  25041  sincosq1lem  25075  coseq0negpitopi  25081  tangtx  25083  sincos4thpi  25091  efif1olem1  25118  efif1olem2  25119  efif1o  25122  efifo  25123  ellogrn  25135  logimclad  25148  ellogdm  25214  logdmnrp  25216  dvloglem  25223  dvlog2lem  25227  asinneg  25456  atans2  25501  ressatans  25504  abvcxp  26183  ostth2  26205  xrge0iifcv  31165  xrge0iifiso  31166  xrge0iifhom  31168  sinccvglem  32903  bj-pinftyccb  34490  bj-pinftynminfty  34496  dvasin  34965  areacirclem4  34972  gtnelioc  41749  limcicciooub  41902  fourierdlem4  42381  fourierdlem26  42403  fourierdlem33  42410  fourierdlem37  42414  fourierdlem65  42441  fourierdlem79  42455  fouriersw  42501  eenglngeehlnmlem1  44709  eenglngeehlnmlem2  44710
  Copyright terms: Public domain W3C validator