ellogrn - Metamath Proof Explorer

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

Theorem ellogrn 26540

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 15070	. . . 4 ⊢ ℑ:ℂ⟶ℝ
2		ffn 6664	. . . 4 ⊢ (ℑ:ℂ⟶ℝ → ℑ Fn ℂ)
3		elpreima 7006	. . . 4 ⊢ (ℑ Fn ℂ → (𝐴 ∈ (^◡ℑ “ (-π(,]π)) ↔ (𝐴 ∈ ℂ ∧ (ℑ‘𝐴) ∈ (-π(,]π))))
4	1, 2, 3	mp2b 10	. . 3 ⊢ (𝐴 ∈ (^◡ℑ “ (-π(,]π)) ↔ (𝐴 ∈ ℂ ∧ (ℑ‘𝐴) ∈ (-π(,]π)))
5		pire 26438	. . . . . . . . 9 ⊢ π ∈ ℝ
6	5	renegcli 11450	. . . . . . . 8 ⊢ -π ∈ ℝ
7	6	rexri 11198	. . . . . . 7 ⊢ -π ∈ ℝ^*
8		elioc2 13357	. . . . . . 7 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ) → ((ℑ‘𝐴) ∈ (-π(,]π) ↔ ((ℑ‘𝐴) ∈ ℝ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
9	7, 5, 8	mp2an 693	. . . . . 6 ⊢ ((ℑ‘𝐴) ∈ (-π(,]π) ↔ ((ℑ‘𝐴) ∈ ℝ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π))
10		3anass 1095	. . . . . 6 ⊢ (((ℑ‘𝐴) ∈ ℝ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π) ↔ ((ℑ‘𝐴) ∈ ℝ ∧ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
11	9, 10	bitri 275	. . . . 5 ⊢ ((ℑ‘𝐴) ∈ (-π(,]π) ↔ ((ℑ‘𝐴) ∈ ℝ ∧ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
12		imcl 15068	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℝ)
13	12	biantrurd 532	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π) ↔ ((ℑ‘𝐴) ∈ ℝ ∧ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π))))
14	11, 13	bitr4id 290	. . . 4 ⊢ (𝐴 ∈ ℂ → ((ℑ‘𝐴) ∈ (-π(,]π) ↔ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
15	14	pm5.32i 574	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) ∈ (-π(,]π)) ↔ (𝐴 ∈ ℂ ∧ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
16	4, 15	bitri 275	. 2 ⊢ (𝐴 ∈ (^◡ℑ “ (-π(,]π)) ↔ (𝐴 ∈ ℂ ∧ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
17		logrn 26539	. . 3 ⊢ ran log = (^◡ℑ “ (-π(,]π))
18	17	eleq2i 2829	. 2 ⊢ (𝐴 ∈ ran log ↔ 𝐴 ∈ (^◡ℑ “ (-π(,]π)))
19		3anass 1095	. 2 ⊢ ((𝐴 ∈ ℂ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π) ↔ (𝐴 ∈ ℂ ∧ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
20	16, 18, 19	3bitr4i 303	1 ⊢ (𝐴 ∈ ran log ↔ (𝐴 ∈ ℂ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 206 ∧ wa 395 ∧ w3a 1087 ∈ wcel 2114 class class class wbr 5086 ^◡ccnv 5625 ran crn 5627 “ cima 5629 Fn wfn 6489 ⟶wf 6490 ‘cfv 6494 (class class class)co 7362 ℂcc 11031 ℝcr 11032 ℝ^*cxr 11173 < clt 11174 ≤ cle 11175 -cneg 11373 (,]cioc 13294 ℑcim 15055 πcpi 16026 logclog 26535

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5304 ax-pr 5372 ax-un 7684 ax-inf2 9557 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110 ax-pre-sup 11111 ax-addf 11112

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5521 df-eprel 5526 df-po 5534 df-so 5535 df-fr 5579 df-se 5580 df-we 5581 df-xp 5632 df-rel 5633 df-cnv 5634 df-co 5635 df-dm 5636 df-rn 5637 df-res 5638 df-ima 5639 df-pred 6261 df-ord 6322 df-on 6323 df-lim 6324 df-suc 6325 df-iota 6450 df-fun 6496 df-fn 6497 df-f 6498 df-f1 6499 df-fo 6500 df-f1o 6501 df-fv 6502 df-isom 6503 df-riota 7319 df-ov 7365 df-oprab 7366 df-mpo 7367 df-of 7626 df-om 7813 df-1st 7937 df-2nd 7938 df-supp 8106 df-frecs 8226 df-wrecs 8257 df-recs 8306 df-rdg 8344 df-1o 8400 df-2o 8401 df-er 8638 df-map 8770 df-pm 8771 df-ixp 8841 df-en 8889 df-dom 8890 df-sdom 8891 df-fin 8892 df-fsupp 9270 df-fi 9319 df-sup 9350 df-inf 9351 df-oi 9420 df-card 9858 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-div 11803 df-nn 12170 df-2 12239 df-3 12240 df-4 12241 df-5 12242 df-6 12243 df-7 12244 df-8 12245 df-9 12246 df-n0 12433 df-z 12520 df-dec 12640 df-uz 12784 df-q 12894 df-rp 12938 df-xneg 13058 df-xadd 13059 df-xmul 13060 df-ioo 13297 df-ioc 13298 df-ico 13299 df-icc 13300 df-fz 13457 df-fzo 13604 df-fl 13746 df-mod 13824 df-seq 13959 df-exp 14019 df-fac 14231 df-bc 14260 df-hash 14288 df-shft 15024 df-cj 15056 df-re 15057 df-im 15058 df-sqrt 15192 df-abs 15193 df-limsup 15428 df-clim 15445 df-rlim 15446 df-sum 15644 df-ef 16027 df-sin 16029 df-cos 16030 df-pi 16032 df-struct 17112 df-sets 17129 df-slot 17147 df-ndx 17159 df-base 17175 df-ress 17196 df-plusg 17228 df-mulr 17229 df-starv 17230 df-sca 17231 df-vsca 17232 df-ip 17233 df-tset 17234 df-ple 17235 df-ds 17237 df-unif 17238 df-hom 17239 df-cco 17240 df-rest 17380 df-topn 17381 df-0g 17399 df-gsum 17400 df-topgen 17401 df-pt 17402 df-prds 17405 df-xrs 17461 df-qtop 17466 df-imas 17467 df-xps 17469 df-mre 17543 df-mrc 17544 df-acs 17546 df-mgm 18603 df-sgrp 18682 df-mnd 18698 df-submnd 18747 df-mulg 19039 df-cntz 19287 df-cmn 19752 df-psmet 21340 df-xmet 21341 df-met 21342 df-bl 21343 df-mopn 21344 df-fbas 21345 df-fg 21346 df-cnfld 21349 df-top 22873 df-topon 22890 df-topsp 22912 df-bases 22925 df-cld 22998 df-ntr 22999 df-cls 23000 df-nei 23077 df-lp 23115 df-perf 23116 df-cn 23206 df-cnp 23207 df-haus 23294 df-tx 23541 df-hmeo 23734 df-fil 23825 df-fm 23917 df-flim 23918 df-flf 23919 df-xms 24299 df-ms 24300 df-tms 24301 df-cncf 24859 df-limc 25847 df-dv 25848 df-log 26537

This theorem is referenced by: relogrn 26542 logrncn 26543 logimcl 26550 logrnaddcl 26555 logi 26568 logneg 26569 logcj 26587 logimul 26595 logneg2 26596 logcnlem4 26626 logf1o2 26631 logreclem 26743 asinsin 26873 asin1 26875 atanlogaddlem 26894 atanlogsub 26897 atantan 26904

W3C validator