ellogdm - Metamath Proof Explorer

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

Theorem ellogdm 26600

Description: Elementhood in the "continuous domain" of the complex logarithm. (Contributed by Mario Carneiro, 18-Feb-2015.)

**Hypothesis**
Ref	Expression
logcn.d	⊢ 𝐷 = (ℂ ∖ (-∞(,]0))

**Assertion**
Ref	Expression
ellogdm	⊢ (𝐴 ∈ 𝐷 ↔ (𝐴 ∈ ℂ ∧ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ⁺)))

**Proof of Theorem ellogdm**
Step	Hyp	Ref	Expression
1		logcn.d	. . 3 ⊢ 𝐷 = (ℂ ∖ (-∞(,]0))
2	1	eleq2i 2826	. 2 ⊢ (𝐴 ∈ 𝐷 ↔ 𝐴 ∈ (ℂ ∖ (-∞(,]0)))
3		eldif 3936	. 2 ⊢ (𝐴 ∈ (ℂ ∖ (-∞(,]0)) ↔ (𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ (-∞(,]0)))
4		mnfxr 11292	. . . . . . 7 ⊢ -∞ ∈ ℝ^*
5		0re 11237	. . . . . . 7 ⊢ 0 ∈ ℝ
6		elioc2 13426	. . . . . . 7 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ) → (𝐴 ∈ (-∞(,]0) ↔ (𝐴 ∈ ℝ ∧ -∞ < 𝐴 ∧ 𝐴 ≤ 0)))
7	4, 5, 6	mp2an 692	. . . . . 6 ⊢ (𝐴 ∈ (-∞(,]0) ↔ (𝐴 ∈ ℝ ∧ -∞ < 𝐴 ∧ 𝐴 ≤ 0))
8		df-3an 1088	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ -∞ < 𝐴 ∧ 𝐴 ≤ 0) ↔ ((𝐴 ∈ ℝ ∧ -∞ < 𝐴) ∧ 𝐴 ≤ 0))
9		mnflt 13139	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)
10	9	pm4.71i 559	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ ↔ (𝐴 ∈ ℝ ∧ -∞ < 𝐴))
11	10	anbi1i 624	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≤ 0) ↔ ((𝐴 ∈ ℝ ∧ -∞ < 𝐴) ∧ 𝐴 ≤ 0))
12		lenlt 11313	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐴 ≤ 0 ↔ ¬ 0 < 𝐴))
13	5, 12	mpan2 691	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → (𝐴 ≤ 0 ↔ ¬ 0 < 𝐴))
14		elrp 13010	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ⁺ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
15	14	baib 535	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℝ⁺ ↔ 0 < 𝐴))
16	15	notbid 318	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → (¬ 𝐴 ∈ ℝ⁺ ↔ ¬ 0 < 𝐴))
17	13, 16	bitr4d 282	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → (𝐴 ≤ 0 ↔ ¬ 𝐴 ∈ ℝ⁺))
18	17	pm5.32i 574	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≤ 0) ↔ (𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℝ⁺))
19	11, 18	bitr3i 277	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ -∞ < 𝐴) ∧ 𝐴 ≤ 0) ↔ (𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℝ⁺))
20	7, 8, 19	3bitri 297	. . . . 5 ⊢ (𝐴 ∈ (-∞(,]0) ↔ (𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℝ⁺))
21	20	notbii 320	. . . 4 ⊢ (¬ 𝐴 ∈ (-∞(,]0) ↔ ¬ (𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℝ⁺))
22		iman 401	. . . 4 ⊢ ((𝐴 ∈ ℝ → 𝐴 ∈ ℝ⁺) ↔ ¬ (𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℝ⁺))
23	21, 22	bitr4i 278	. . 3 ⊢ (¬ 𝐴 ∈ (-∞(,]0) ↔ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ⁺))
24	23	anbi2i 623	. 2 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ (-∞(,]0)) ↔ (𝐴 ∈ ℂ ∧ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ⁺)))
25	2, 3, 24	3bitri 297	1 ⊢ (𝐴 ∈ 𝐷 ↔ (𝐴 ∈ ℂ ∧ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ⁺)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2108 ∖ cdif 3923 class class class wbr 5119 (class class class)co 7405 ℂcc 11127 ℝcr 11128 0cc0 11129 -∞cmnf 11267 ℝ^*cxr 11268 < clt 11269 ≤ cle 11270 ℝ⁺crp 13008 (,]cioc 13363

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-cnex 11185 ax-resscn 11186 ax-1cn 11187 ax-addrcl 11190 ax-rnegex 11200 ax-cnre 11202 ax-pre-lttri 11203 ax-pre-lttrn 11204

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-br 5120 df-opab 5182 df-mpt 5202 df-id 5548 df-po 5561 df-so 5562 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-ov 7408 df-oprab 7409 df-mpo 7410 df-er 8719 df-en 8960 df-dom 8961 df-sdom 8962 df-pnf 11271 df-mnf 11272 df-xr 11273 df-ltxr 11274 df-le 11275 df-rp 13009 df-ioc 13367

This theorem is referenced by: logdmn0 26601 logdmnrp 26602 logdmss 26603 logcnlem2 26604 logcnlem3 26605 logcnlem4 26606 logcnlem5 26607 logcn 26608 dvloglem 26609 logf1o2 26611 cxpcn 26706 cxpcnOLD 26707 cxpcn2 26708 dmlogdmgm 26986 rpdmgm 26987 lgamgulmlem2 26992 lgamcvg2 27017 logdivsqrle 34682 binomcxplemdvbinom 44377

W3C validator