efopnlem2

		Ref	Expression
	Hypothesis	efopn.j	⊢ 𝐽 = ( TopOpen ‘ ℂ_fld )
	Assertion	efopnlem2	⊢ ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) → ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) ∈ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		efopn.j	⊢ 𝐽 = ( TopOpen ‘ ℂ_fld )
2		logf1o	⊢ log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log
3		f1orn	⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log ↔ ( log Fn ( ℂ ∖ { 0 } ) ∧ Fun ^◡ log ) )
4	3	simprbi	⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → Fun ^◡ log )
5		funcnvres	⊢ ( Fun ^◡ log → ^◡ ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) = ( ^◡ log ↾ ( log “ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) )
6	2 4 5	mp2b	⊢ ^◡ ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) = ( ^◡ log ↾ ( log “ ( ℂ ∖ ( -∞ (,] 0 ) ) ) )
7		df-log	⊢ log = ^◡ ( exp ↾ ( ^◡ ℑ “ ( - π (,] π ) ) )
8	7	cnveqi	⊢ ^◡ log = ^◡ ^◡ ( exp ↾ ( ^◡ ℑ “ ( - π (,] π ) ) )
9		relres	⊢ Rel ( exp ↾ ( ^◡ ℑ “ ( - π (,] π ) ) )
10		dfrel2	⊢ ( Rel ( exp ↾ ( ^◡ ℑ “ ( - π (,] π ) ) ) ↔ ^◡ ^◡ ( exp ↾ ( ^◡ ℑ “ ( - π (,] π ) ) ) = ( exp ↾ ( ^◡ ℑ “ ( - π (,] π ) ) ) )
11	9 10	mpbi	⊢ ^◡ ^◡ ( exp ↾ ( ^◡ ℑ “ ( - π (,] π ) ) ) = ( exp ↾ ( ^◡ ℑ “ ( - π (,] π ) ) )
12	8 11	eqtri	⊢ ^◡ log = ( exp ↾ ( ^◡ ℑ “ ( - π (,] π ) ) )
13	12	reseq1i	⊢ ( ^◡ log ↾ ( log “ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) = ( ( exp ↾ ( ^◡ ℑ “ ( - π (,] π ) ) ) ↾ ( log “ ( ℂ ∖ ( -∞ (,] 0 ) ) ) )
14		imassrn	⊢ ( log “ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ⊆ ran log
15		logrn	⊢ ran log = ( ^◡ ℑ “ ( - π (,] π ) )
16	14 15	sseqtri	⊢ ( log “ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ⊆ ( ^◡ ℑ “ ( - π (,] π ) )
17		resabs1	⊢ ( ( log “ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ⊆ ( ^◡ ℑ “ ( - π (,] π ) ) → ( ( exp ↾ ( ^◡ ℑ “ ( - π (,] π ) ) ) ↾ ( log “ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) = ( exp ↾ ( log “ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) )
18	16 17	ax-mp	⊢ ( ( exp ↾ ( ^◡ ℑ “ ( - π (,] π ) ) ) ↾ ( log “ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) = ( exp ↾ ( log “ ( ℂ ∖ ( -∞ (,] 0 ) ) ) )
19	6 13 18	3eqtri	⊢ ^◡ ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) = ( exp ↾ ( log “ ( ℂ ∖ ( -∞ (,] 0 ) ) ) )
20	19	imaeq1i	⊢ ( ^◡ ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) = ( ( exp ↾ ( log “ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) )
21		cnxmet	⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
22		0cnd	⊢ ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) → 0 ∈ ℂ )
23		rpxr	⊢ ( 𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ^* )
24	23	adantr	⊢ ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) → 𝑅 ∈ ℝ^* )
25		blssm	⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 0 ∈ ℂ ∧ 𝑅 ∈ ℝ^* ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ⊆ ℂ )
26	21 22 24 25	mp3an2i	⊢ ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ⊆ ℂ )
27	26	sselda	⊢ ( ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) ∧ 𝑥 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) → 𝑥 ∈ ℂ )
28	27	imcld	⊢ ( ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) ∧ 𝑥 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) → ( ℑ ‘ 𝑥 ) ∈ ℝ )
29		efopnlem1	⊢ ( ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) ∧ 𝑥 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) → ( abs ‘ ( ℑ ‘ 𝑥 ) ) < π )
30		pire	⊢ π ∈ ℝ
31		abslt	⊢ ( ( ( ℑ ‘ 𝑥 ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( abs ‘ ( ℑ ‘ 𝑥 ) ) < π ↔ ( - π < ( ℑ ‘ 𝑥 ) ∧ ( ℑ ‘ 𝑥 ) < π ) ) )
32	28 30 31	sylancl	⊢ ( ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) ∧ 𝑥 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) → ( ( abs ‘ ( ℑ ‘ 𝑥 ) ) < π ↔ ( - π < ( ℑ ‘ 𝑥 ) ∧ ( ℑ ‘ 𝑥 ) < π ) ) )
33	29 32	mpbid	⊢ ( ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) ∧ 𝑥 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) → ( - π < ( ℑ ‘ 𝑥 ) ∧ ( ℑ ‘ 𝑥 ) < π ) )
34	33	simpld	⊢ ( ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) ∧ 𝑥 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) → - π < ( ℑ ‘ 𝑥 ) )
35	33	simprd	⊢ ( ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) ∧ 𝑥 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) → ( ℑ ‘ 𝑥 ) < π )
36	30	renegcli	⊢ - π ∈ ℝ
37	36	rexri	⊢ - π ∈ ℝ^*
38	30	rexri	⊢ π ∈ ℝ^*
39		elioo2	⊢ ( ( - π ∈ ℝ^* ∧ π ∈ ℝ^* ) → ( ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ↔ ( ( ℑ ‘ 𝑥 ) ∈ ℝ ∧ - π < ( ℑ ‘ 𝑥 ) ∧ ( ℑ ‘ 𝑥 ) < π ) ) )
40	37 38 39	mp2an	⊢ ( ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ↔ ( ( ℑ ‘ 𝑥 ) ∈ ℝ ∧ - π < ( ℑ ‘ 𝑥 ) ∧ ( ℑ ‘ 𝑥 ) < π ) )
41	28 34 35 40	syl3anbrc	⊢ ( ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) ∧ 𝑥 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) → ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) )
42		imf	⊢ ℑ : ℂ ⟶ ℝ
43		ffn	⊢ ( ℑ : ℂ ⟶ ℝ → ℑ Fn ℂ )
44		elpreima	⊢ ( ℑ Fn ℂ → ( 𝑥 ∈ ( ^◡ ℑ “ ( - π (,) π ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ) )
45	42 43 44	mp2b	⊢ ( 𝑥 ∈ ( ^◡ ℑ “ ( - π (,) π ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) )
46	27 41 45	sylanbrc	⊢ ( ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) ∧ 𝑥 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) → 𝑥 ∈ ( ^◡ ℑ “ ( - π (,) π ) ) )
47	46	ex	⊢ ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) → ( 𝑥 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) → 𝑥 ∈ ( ^◡ ℑ “ ( - π (,) π ) ) ) )
48	47	ssrdv	⊢ ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ⊆ ( ^◡ ℑ “ ( - π (,) π ) ) )
49		df-ima	⊢ ( log “ ( ℂ ∖ ( -∞ (,] 0 ) ) ) = ran ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) )
50		eqid	⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) = ( ℂ ∖ ( -∞ (,] 0 ) )
51	50	logf1o2	⊢ ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) : ( ℂ ∖ ( -∞ (,] 0 ) ) –1-1-onto→ ( ^◡ ℑ “ ( - π (,) π ) )
52		f1ofo	⊢ ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) : ( ℂ ∖ ( -∞ (,] 0 ) ) –1-1-onto→ ( ^◡ ℑ “ ( - π (,) π ) ) → ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) : ( ℂ ∖ ( -∞ (,] 0 ) ) –onto→ ( ^◡ ℑ “ ( - π (,) π ) ) )
53		forn	⊢ ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) : ( ℂ ∖ ( -∞ (,] 0 ) ) –onto→ ( ^◡ ℑ “ ( - π (,) π ) ) → ran ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) = ( ^◡ ℑ “ ( - π (,) π ) ) )
54	51 52 53	mp2b	⊢ ran ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) = ( ^◡ ℑ “ ( - π (,) π ) )
55	49 54	eqtri	⊢ ( log “ ( ℂ ∖ ( -∞ (,] 0 ) ) ) = ( ^◡ ℑ “ ( - π (,) π ) )
56	48 55	sseqtrrdi	⊢ ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ⊆ ( log “ ( ℂ ∖ ( -∞ (,] 0 ) ) ) )
57		resima2	⊢ ( ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ⊆ ( log “ ( ℂ ∖ ( -∞ (,] 0 ) ) ) → ( ( exp ↾ ( log “ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) = ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) )
58	56 57	syl	⊢ ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) → ( ( exp ↾ ( log “ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) = ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) )
59	20 58	eqtrid	⊢ ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) → ( ^◡ ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) = ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) )
60	50	logcn	⊢ ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∈ ( ( ℂ ∖ ( -∞ (,] 0 ) ) –cn→ ℂ )
61		difss	⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ℂ
62		ssid	⊢ ℂ ⊆ ℂ
63		eqid	⊢ ( 𝐽 ↾_t ( ℂ ∖ ( -∞ (,] 0 ) ) ) = ( 𝐽 ↾_t ( ℂ ∖ ( -∞ (,] 0 ) ) )
64	1	cnfldtopon	⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
65	64	toponrestid	⊢ 𝐽 = ( 𝐽 ↾_t ℂ )
66	1 63 65	cncfcn	⊢ ( ( ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( ℂ ∖ ( -∞ (,] 0 ) ) –cn→ ℂ ) = ( ( 𝐽 ↾_t ( ℂ ∖ ( -∞ (,] 0 ) ) ) Cn 𝐽 ) )
67	61 62 66	mp2an	⊢ ( ( ℂ ∖ ( -∞ (,] 0 ) ) –cn→ ℂ ) = ( ( 𝐽 ↾_t ( ℂ ∖ ( -∞ (,] 0 ) ) ) Cn 𝐽 )
68	60 67	eleqtri	⊢ ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∈ ( ( 𝐽 ↾_t ( ℂ ∖ ( -∞ (,] 0 ) ) ) Cn 𝐽 )
69	1	cnfldtopn	⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
70	69	blopn	⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 0 ∈ ℂ ∧ 𝑅 ∈ ℝ^* ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ∈ 𝐽 )
71	21 22 24 70	mp3an2i	⊢ ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ∈ 𝐽 )
72		cnima	⊢ ( ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∈ ( ( 𝐽 ↾_t ( ℂ ∖ ( -∞ (,] 0 ) ) ) Cn 𝐽 ) ∧ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ∈ 𝐽 ) → ( ^◡ ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) ∈ ( 𝐽 ↾_t ( ℂ ∖ ( -∞ (,] 0 ) ) ) )
73	68 71 72	sylancr	⊢ ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) → ( ^◡ ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) ∈ ( 𝐽 ↾_t ( ℂ ∖ ( -∞ (,] 0 ) ) ) )
74	59 73	eqeltrrd	⊢ ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) → ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) ∈ ( 𝐽 ↾_t ( ℂ ∖ ( -∞ (,] 0 ) ) ) )
75	1	cnfldtop	⊢ 𝐽 ∈ Top
76	50	logdmopn	⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) ∈ ( TopOpen ‘ ℂ_fld )
77	76 1	eleqtrri	⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) ∈ 𝐽
78		restopn2	⊢ ( ( 𝐽 ∈ Top ∧ ( ℂ ∖ ( -∞ (,] 0 ) ) ∈ 𝐽 ) → ( ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) ∈ ( 𝐽 ↾_t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ↔ ( ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) ∈ 𝐽 ∧ ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) ⊆ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) )
79	75 77 78	mp2an	⊢ ( ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) ∈ ( 𝐽 ↾_t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ↔ ( ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) ∈ 𝐽 ∧ ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) ⊆ ( ℂ ∖ ( -∞ (,] 0 ) ) ) )
80	74 79	sylib	⊢ ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) → ( ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) ∈ 𝐽 ∧ ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) ⊆ ( ℂ ∖ ( -∞ (,] 0 ) ) ) )
81	80	simpld	⊢ ( ( 𝑅 ∈ ℝ⁺ ∧ 𝑅 < π ) → ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) ∈ 𝐽 )

Metamath Proof Explorer

Theorem efopnlem2

Proof