Theorem ellogrn 24860

Description: Write out the property 𝐴 ∈ ran log explicitly. (Contributed by Mario Carneiro, 1-Apr-2015.)

Assertion

Ref	Expression
ellogrn	⊢ (𝐴 ∈ ran log ↔ (𝐴 ∈ ℂ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π))

Proof of Theorem ellogrn

Step	Hyp	Ref	Expression
1		imf 14332	. . . 4 ⊢ ℑ:ℂ⟶ℝ
2		ffn 6342	. . . 4 ⊢ (ℑ:ℂ⟶ℝ → ℑ Fn ℂ)
3		elpreima 6652	. . . 4 ⊢ (ℑ Fn ℂ → (𝐴 ∈ (◡ℑ “ (-π(,]π)) ↔ (𝐴 ∈ ℂ ∧ (ℑ‘𝐴) ∈ (-π(,]π))))
4	1, 2, 3	mp2b 10	. . 3 ⊢ (𝐴 ∈ (◡ℑ “ (-π(,]π)) ↔ (𝐴 ∈ ℂ ∧ (ℑ‘𝐴) ∈ (-π(,]π)))
5		imcl 14330	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℝ)
6	5	biantrurd 525	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π) ↔ ((ℑ‘𝐴) ∈ ℝ ∧ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π))))
7		pire 24763	. . . . . . . . 9 ⊢ π ∈ ℝ
8	7	renegcli 10747	. . . . . . . 8 ⊢ -π ∈ ℝ
9	8	rexri 10498	. . . . . . 7 ⊢ -π ∈ ℝ*
10		elioc2 12614	. . . . . . 7 ⊢ ((-π ∈ ℝ* ∧ π ∈ ℝ) → ((ℑ‘𝐴) ∈ (-π(,]π) ↔ ((ℑ‘𝐴) ∈ ℝ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
11	9, 7, 10	mp2an 680	. . . . . 6 ⊢ ((ℑ‘𝐴) ∈ (-π(,]π) ↔ ((ℑ‘𝐴) ∈ ℝ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π))
12		3anass 1077	. . . . . 6 ⊢ (((ℑ‘𝐴) ∈ ℝ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π) ↔ ((ℑ‘𝐴) ∈ ℝ ∧ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
13	11, 12	bitri 267	. . . . 5 ⊢ ((ℑ‘𝐴) ∈ (-π(,]π) ↔ ((ℑ‘𝐴) ∈ ℝ ∧ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
14	6, 13	syl6rbbr 282	. . . 4 ⊢ (𝐴 ∈ ℂ → ((ℑ‘𝐴) ∈ (-π(,]π) ↔ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
15	14	pm5.32i 567	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) ∈ (-π(,]π)) ↔ (𝐴 ∈ ℂ ∧ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
16	4, 15	bitri 267	. 2 ⊢ (𝐴 ∈ (◡ℑ “ (-π(,]π)) ↔ (𝐴 ∈ ℂ ∧ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
17		logrn 24859	. . 3 ⊢ ran log = (◡ℑ “ (-π(,]π))
18	17	eleq2i 2852	. 2 ⊢ (𝐴 ∈ ran log ↔ 𝐴 ∈ (◡ℑ “ (-π(,]π)))
19		3anass 1077	. 2 ⊢ ((𝐴 ∈ ℂ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π) ↔ (𝐴 ∈ ℂ ∧ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
20	16, 18, 19	3bitr4i 295	1 ⊢ (𝐴 ∈ ran log ↔ (𝐴 ∈ ℂ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π))

Syntax hints:   ↔ wb 198   ∧ wa 387   ∧ w3a 1069   ∈ wcel 2051   class class class wbr 4926  ^◡ccnv 5403  ran crn 5405   “ cima 5407   Fn wfn 6181  ⟶wf 6182  ‘cfv 6186  (class class class)co 6975  ℂcc 10332  ℝcr 10333  ℝ^*cxr 10472   < clt 10473   ≤ cle 10474  -cneg 10670  (,]cioc 12554  ℑcim 14317  πcpi 15279  logclog 24855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-rep 5046  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278  ax-inf2 8897  ax-cnex 10390  ax-resscn 10391  ax-1cn 10392  ax-icn 10393  ax-addcl 10394  ax-addrcl 10395  ax-mulcl 10396  ax-mulrcl 10397  ax-mulcom 10398  ax-addass 10399  ax-mulass 10400  ax-distr 10401  ax-i2m1 10402  ax-1ne0 10403  ax-1rid 10404  ax-rnegex 10405  ax-rrecex 10406  ax-cnre 10407  ax-pre-lttri 10408  ax-pre-lttrn 10409  ax-pre-ltadd 10410  ax-pre-mulgt0 10411  ax-pre-sup 10412  ax-addf 10413  ax-mulf 10414

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-fal 1521  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-nel 3069  df-ral 3088  df-rex 3089  df-reu 3090  df-rmo 3091  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-pss 3840  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-tp 4441  df-op 4443  df-uni 4710  df-int 4747  df-iun 4791  df-iin 4792  df-br 4927  df-opab 4989  df-mpt 5006  df-tr 5028  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-se 5364  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-isom 6195  df-riota 6936  df-ov 6978  df-oprab 6979  df-mpo 6980  df-of 7226  df-om 7396  df-1st 7500  df-2nd 7501  df-supp 7633  df-wrecs 7749  df-recs 7811  df-rdg 7849  df-1o 7904  df-2o 7905  df-oadd 7908  df-er 8088  df-map 8207  df-pm 8208  df-ixp 8259  df-en 8306  df-dom 8307  df-sdom 8308  df-fin 8309  df-fsupp 8628  df-fi 8669  df-sup 8700  df-inf 8701  df-oi 8768  df-card 9161  df-cda 9387  df-pnf 10475  df-mnf 10476  df-xr 10477  df-ltxr 10478  df-le 10479  df-sub 10671  df-neg 10672  df-div 11098  df-nn 11439  df-2 11502  df-3 11503  df-4 11504  df-5 11505  df-6 11506  df-7 11507  df-8 11508  df-9 11509  df-n0 11707  df-z 11793  df-dec 11911  df-uz 12058  df-q 12162  df-rp 12204  df-xneg 12323  df-xadd 12324  df-xmul 12325  df-ioo 12557  df-ioc 12558  df-ico 12559  df-icc 12560  df-fz 12708  df-fzo 12849  df-fl 12976  df-mod 13052  df-seq 13184  df-exp 13244  df-fac 13448  df-bc 13477  df-hash 13505  df-shft 14286  df-cj 14318  df-re 14319  df-im 14320  df-sqrt 14454  df-abs 14455  df-limsup 14688  df-clim 14705  df-rlim 14706  df-sum 14903  df-ef 15280  df-sin 15282  df-cos 15283  df-pi 15285  df-struct 16340  df-ndx 16341  df-slot 16342  df-base 16344  df-sets 16345  df-ress 16346  df-plusg 16433  df-mulr 16434  df-starv 16435  df-sca 16436  df-vsca 16437  df-ip 16438  df-tset 16439  df-ple 16440  df-ds 16442  df-unif 16443  df-hom 16444  df-cco 16445  df-rest 16551  df-topn 16552  df-0g 16570  df-gsum 16571  df-topgen 16572  df-pt 16573  df-prds 16576  df-xrs 16630  df-qtop 16635  df-imas 16636  df-xps 16638  df-mre 16728  df-mrc 16729  df-acs 16731  df-mgm 17723  df-sgrp 17765  df-mnd 17776  df-submnd 17817  df-mulg 18025  df-cntz 18231  df-cmn 18681  df-psmet 20255  df-xmet 20256  df-met 20257  df-bl 20258  df-mopn 20259  df-fbas 20260  df-fg 20261  df-cnfld 20264  df-top 21222  df-topon 21239  df-topsp 21261  df-bases 21274  df-cld 21347  df-ntr 21348  df-cls 21349  df-nei 21426  df-lp 21464  df-perf 21465  df-cn 21555  df-cnp 21556  df-haus 21643  df-tx 21890  df-hmeo 22083  df-fil 22174  df-fm 22266  df-flim 22267  df-flf 22268  df-xms 22649  df-ms 22650  df-tms 22651  df-cncf 23205  df-limc 24183  df-dv 24184  df-log 24857

This theorem is referenced by:  relogrn  24862  logrncn  24863  logimcl  24870  logrnaddcl  24875  logneg  24888  logcj  24906  logimul  24914  logneg2  24915  logcnlem4  24945  logf1o2  24950  logreclem  25057  asinsin  25187  asin1  25189  atanlogaddlem  25208  atanlogsub  25211  atantan  25218  logi  32519