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 26794

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 15202	. . . 4 ⊢ ℑ:ℂ⟶ℝ
2		ffn 6706	. . . 4 ⊢ (ℑ:ℂ⟶ℝ → ℑ Fn ℂ)
3		elpreima 7054	. . . 4 ⊢ (ℑ Fn ℂ → (𝐴 ∈ (^◡ℑ “ (-π(,]π)) ↔ (𝐴 ∈ ℂ ∧ (ℑ‘𝐴) ∈ (-π(,]π))))
4	1, 2, 3	mp2b 10	. . 3 ⊢ (𝐴 ∈ (^◡ℑ “ (-π(,]π)) ↔ (𝐴 ∈ ℂ ∧ (ℑ‘𝐴) ∈ (-π(,]π)))
5		pire 26689	. . . . . . . . 9 ⊢ π ∈ ℝ
6	5	renegcli 11546	. . . . . . . 8 ⊢ -π ∈ ℝ
7	6	rexri 11294	. . . . . . 7 ⊢ -π ∈ ℝ^*
8		elioc2 13464	. . . . . . 7 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ) → ((ℑ‘𝐴) ∈ (-π(,]π) ↔ ((ℑ‘𝐴) ∈ ℝ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
9	7, 5, 8	mp2an 705	. . . . . 6 ⊢ ((ℑ‘𝐴) ∈ (-π(,]π) ↔ ((ℑ‘𝐴) ∈ ℝ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π))
10		3anass 1111	. . . . . 6 ⊢ (((ℑ‘𝐴) ∈ ℝ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π) ↔ ((ℑ‘𝐴) ∈ ℝ ∧ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
11	9, 10	bitri 278	. . . . 5 ⊢ ((ℑ‘𝐴) ∈ (-π(,]π) ↔ ((ℑ‘𝐴) ∈ ℝ ∧ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
12		imcl 15200	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℝ)
13	12	biantrurd 542	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π) ↔ ((ℑ‘𝐴) ∈ ℝ ∧ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π))))
14	11, 13	bitr4id 293	. . . 4 ⊢ (𝐴 ∈ ℂ → ((ℑ‘𝐴) ∈ (-π(,]π) ↔ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
15	14	pm5.32i 585	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) ∈ (-π(,]π)) ↔ (𝐴 ∈ ℂ ∧ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
16	4, 15	bitri 278	. 2 ⊢ (𝐴 ∈ (^◡ℑ “ (-π(,]π)) ↔ (𝐴 ∈ ℂ ∧ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
17		logrn 26793	. . 3 ⊢ ran log = (^◡ℑ “ (-π(,]π))
18	17	eleq2i 2854	. 2 ⊢ (𝐴 ∈ ran log ↔ 𝐴 ∈ (^◡ℑ “ (-π(,]π)))
19		3anass 1111	. 2 ⊢ ((𝐴 ∈ ℂ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π) ↔ (𝐴 ∈ ℂ ∧ (-π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)))
20	16, 18, 19	3bitr4i 306	1 ⊢ (𝐴 ∈ ran log ↔ (𝐴 ∈ ℂ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ↔ wb 209 ∧ wa 401 ∧ w3a 1103 ∈ wcel 2145 class class class wbr 5107 ^◡ccnv 5658 ran crn 5660 “ cima 5662 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 (class class class)co 7416 ℂcc 11125 ℝcr 11126 ℝ^*cxr 11269 < clt 11270 ≤ cle 11271 -cneg 11469 (,]cioc 13401 ℑcim 15187 πcpi 16156 logclog 26789

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-inf2 9623 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205 ax-addf 11206

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-of 7681 df-om 7866 df-1st 7989 df-2nd 7990 df-supp 8162 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8458 df-2o 8459 df-er 8699 df-map 8831 df-pm 8832 df-ixp 8908 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-fsupp 9335 df-fi 9384 df-sup 9415 df-inf 9416 df-oi 9485 df-card 9947 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12532 df-z 12619 df-dec 12740 df-uz 12891 df-q 13001 df-rp 13045 df-xneg 13165 df-xadd 13166 df-xmul 13167 df-ioo 13404 df-ioc 13405 df-ico 13406 df-icc 13407 df-fz 13564 df-fzo 13712 df-fl 13855 df-mod 13933 df-seq 14068 df-exp 14128 df-fac 14340 df-bc 14369 df-hash 14397 df-shft 15142 df-cj 15188 df-re 15189 df-im 15190 df-sqrt 15324 df-abs 15325 df-limsup 15560 df-clim 15577 df-rlim 15578 df-sum 15776 df-ef 16157 df-sin 16159 df-cos 16160 df-pi 16162 df-struct 17243 df-sets 17260 df-slot 17278 df-ndx 17290 df-base 17306 df-ress 17327 df-plusg 17359 df-mulr 17360 df-starv 17361 df-sca 17362 df-vsca 17363 df-ip 17364 df-tset 17365 df-ple 17366 df-ds 17368 df-unif 17369 df-hom 17370 df-cco 17371 df-rest 17511 df-topn 17512 df-0g 17530 df-gsum 17531 df-topgen 17532 df-pt 17533 df-prds 17536 df-xrs 17592 df-qtop 17597 df-imas 17598 df-xps 17600 df-mre 17674 df-mrc 17675 df-acs 17677 df-mgm 18734 df-sgrp 18823 df-mnd 18839 df-submnd 18893 df-mulg 19192 df-cntz 19445 df-cmn 19910 df-psmet 21578 df-xmet 21579 df-met 21580 df-bl 21581 df-mopn 21582 df-fbas 21583 df-fg 21584 df-cnfld 21587 df-top 23120 df-topon 23137 df-topsp 23159 df-bases 23172 df-cld 23245 df-ntr 23246 df-cls 23247 df-nei 23324 df-lp 23362 df-perf 23363 df-cn 23453 df-cnp 23454 df-haus 23541 df-tx 23789 df-hmeo 23982 df-fil 24073 df-fm 24165 df-flim 24166 df-flf 24167 df-xms 24547 df-ms 24548 df-tms 24549 df-cncf 25107 df-limc 26095 df-dv 26096 df-log 26791

This theorem is used by: relogrn 26796 logrncn 26797 logimcl 26804 logrnaddcl 26809 logi 26822 logneg 26823 logcj 26841 logimul 26849 logneg2 26850 logcnlem4 26880 logf1o2 26885 logreclem 26997 asinsin 27127 asin1 27129 atanlogaddlem 27148 atanlogsub 27151 atantan 27158

W3C validator