MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ellogdm Structured version   Unicode version

Theorem ellogdm 23526
Description: Elementhood in the "continuous domain" of the complex logarithm. (Contributed by Mario Carneiro, 18-Feb-2015.)
Hypothesis
Ref Expression
logcn.d  |-  D  =  ( CC  \  ( -oo (,] 0 ) )
Assertion
Ref Expression
ellogdm  |-  ( A  e.  D  <->  ( A  e.  CC  /\  ( A  e.  RR  ->  A  e.  RR+ ) ) )

Proof of Theorem ellogdm
StepHypRef Expression
1 logcn.d . . 3  |-  D  =  ( CC  \  ( -oo (,] 0 ) )
21eleq2i 2498 . 2  |-  ( A  e.  D  <->  A  e.  ( CC  \  ( -oo (,] 0 ) ) )
3 eldif 3389 . 2  |-  ( A  e.  ( CC  \ 
( -oo (,] 0 ) )  <->  ( A  e.  CC  /\  -.  A  e.  ( -oo (,] 0
) ) )
4 mnfxr 11365 . . . . . . 7  |- -oo  e.  RR*
5 0re 9594 . . . . . . 7  |-  0  e.  RR
6 elioc2 11648 . . . . . . 7  |-  ( ( -oo  e.  RR*  /\  0  e.  RR )  ->  ( A  e.  ( -oo (,] 0 )  <->  ( A  e.  RR  /\ -oo  <  A  /\  A  <_  0
) ) )
74, 5, 6mp2an 676 . . . . . 6  |-  ( A  e.  ( -oo (,] 0 )  <->  ( A  e.  RR  /\ -oo  <  A  /\  A  <_  0
) )
8 df-3an 984 . . . . . 6  |-  ( ( A  e.  RR  /\ -oo 
<  A  /\  A  <_ 
0 )  <->  ( ( A  e.  RR  /\ -oo  <  A )  /\  A  <_  0 ) )
9 mnflt 11376 . . . . . . . . 9  |-  ( A  e.  RR  -> -oo  <  A )
109pm4.71i 636 . . . . . . . 8  |-  ( A  e.  RR  <->  ( A  e.  RR  /\ -oo  <  A ) )
1110anbi1i 699 . . . . . . 7  |-  ( ( A  e.  RR  /\  A  <_  0 )  <->  ( ( A  e.  RR  /\ -oo  <  A )  /\  A  <_  0 ) )
12 lenlt 9663 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  0  e.  RR )  ->  ( A  <_  0  <->  -.  0  <  A ) )
135, 12mpan2 675 . . . . . . . . 9  |-  ( A  e.  RR  ->  ( A  <_  0  <->  -.  0  <  A ) )
14 elrp 11255 . . . . . . . . . . 11  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
1514baib 911 . . . . . . . . . 10  |-  ( A  e.  RR  ->  ( A  e.  RR+  <->  0  <  A ) )
1615notbid 295 . . . . . . . . 9  |-  ( A  e.  RR  ->  ( -.  A  e.  RR+  <->  -.  0  <  A ) )
1713, 16bitr4d 259 . . . . . . . 8  |-  ( A  e.  RR  ->  ( A  <_  0  <->  -.  A  e.  RR+ ) )
1817pm5.32i 641 . . . . . . 7  |-  ( ( A  e.  RR  /\  A  <_  0 )  <->  ( A  e.  RR  /\  -.  A  e.  RR+ ) )
1911, 18bitr3i 254 . . . . . 6  |-  ( ( ( A  e.  RR  /\ -oo  <  A )  /\  A  <_  0 )  <->  ( A  e.  RR  /\  -.  A  e.  RR+ ) )
207, 8, 193bitri 274 . . . . 5  |-  ( A  e.  ( -oo (,] 0 )  <->  ( A  e.  RR  /\  -.  A  e.  RR+ ) )
2120notbii 297 . . . 4  |-  ( -.  A  e.  ( -oo (,] 0 )  <->  -.  ( A  e.  RR  /\  -.  A  e.  RR+ ) )
22 iman 425 . . . 4  |-  ( ( A  e.  RR  ->  A  e.  RR+ )  <->  -.  ( A  e.  RR  /\  -.  A  e.  RR+ ) )
2321, 22bitr4i 255 . . 3  |-  ( -.  A  e.  ( -oo (,] 0 )  <->  ( A  e.  RR  ->  A  e.  RR+ ) )
2423anbi2i 698 . 2  |-  ( ( A  e.  CC  /\  -.  A  e.  ( -oo (,] 0 ) )  <-> 
( A  e.  CC  /\  ( A  e.  RR  ->  A  e.  RR+ )
) )
252, 3, 243bitri 274 1  |-  ( A  e.  D  <->  ( A  e.  CC  /\  ( A  e.  RR  ->  A  e.  RR+ ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1872    \ cdif 3376   class class class wbr 4366  (class class class)co 6249   CCcc 9488   RRcr 9489   0cc0 9490   -oocmnf 9624   RR*cxr 9625    < clt 9626    <_ cle 9627   RR+crp 11253   (,]cioc 11587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-i2m1 9558  ax-1ne0 9559  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-nel 2602  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-opab 4426  df-mpt 4427  df-id 4711  df-po 4717  df-so 4718  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-er 7318  df-en 7525  df-dom 7526  df-sdom 7527  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-rp 11254  df-ioc 11591
This theorem is referenced by:  logdmn0  23527  logdmnrp  23528  logdmss  23529  logcnlem2  23530  logcnlem3  23531  logcnlem4  23532  logcnlem5  23533  logcn  23534  dvloglem  23535  logf1o2  23537  cxpcn  23627  cxpcn2  23628  dmlogdmgm  23891  rpdmgm  23892  lgamgulmlem2  23897  lgamcvg2  23922  binomcxplemdvbinom  36615
  Copyright terms: Public domain W3C validator