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

Theorem elicc2i 12797
Description: Inference for membership in a closed interval. (Contributed by Scott Fenton, 3-Jun-2013.)
Hypotheses
Ref Expression
elicc2i.1 𝐴 ∈ ℝ
elicc2i.2 𝐵 ∈ ℝ
Assertion
Ref Expression
elicc2i (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵))

Proof of Theorem elicc2i
StepHypRef Expression
1 elicc2i.1 . 2 𝐴 ∈ ℝ
2 elicc2i.2 . 2 𝐵 ∈ ℝ
3 elicc2 12796 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵)))
41, 2, 3mp2an 688 1 (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 207  w3a 1081  wcel 2107   class class class wbr 5063  (class class class)co 7150  cr 10530  cle 10670  [,]cicc 12736
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 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-pre-lttri 10605  ax-pre-lttrn 10606
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-po 5473  df-so 5474  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-ov 7153  df-oprab 7154  df-mpo 7155  df-er 8284  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-icc 12740
This theorem is referenced by:  elicc01  12849  sinbnd2  15530  cosbnd2  15531  iihalf1  23469  iihalf2  23471  elii1  23473  elii2  23474  xrhmeo  23484  oprpiece1res2  23490  pco0  23552  pcoval2  23554  pcoass  23562  vitalilem2  24144  vitali  24148  coseq00topi  25022  coseq0negpitopi  25023  sinq12ge0  25028  cosq14ge0  25031  cosordlem  25047  cosord  25048  cos11  25049  sinord  25050  recosf1o  25051  resinf1o  25052  efif1olem3  25060  argregt0  25125  argrege0  25126  argimgt0  25127  logimul  25129  cxpsqrtlem  25217  acosbnd  25410  log2ub  25460  emcllem7  25512  emgt0  25517  harmonicbnd3  25518  harmoniclbnd  25519  harmonicubnd  25520  harmonicbnd4  25521  logdivbnd  26065  pntpbnd2  26096  sin2h  34768  cos2h  34769  lhe4.4ex1a  40545  fourierdlem40  42317  fourierdlem62  42338  fourierdlem78  42354  fourierdlem111  42387  sqwvfoura  42398  sqwvfourb  42399
  Copyright terms: Public domain W3C validator