Metamath Proof Explorer

Theorem efopnlem1

Description: Lemma for efopn . (Contributed by Mario Carneiro, 23-Apr-2015) (Revised by Mario Carneiro, 8-Sep-2015)

Ref Expression
Assertion efopnlem1 ⊢R∈ℝ+∧R<π∧A∈0ball⁡abs∘−R→ℑ⁡A<π

Proof

Step Hyp Ref Expression
1 simpr ⊢R∈ℝ+∧R<π∧A∈0ball⁡abs∘−R→A∈0ball⁡abs∘−R
2 rpxr ⊢R∈ℝ+→R∈ℝ*
3 2 ad2antrr ⊢R∈ℝ+∧R<π∧A∈0ball⁡abs∘−R→R∈ℝ*
4 eqid ⊢abs∘−=abs∘−
5 4 cnbl0 ⊢R∈ℝ*→abs-10R=0ball⁡abs∘−R
6 3 5 syl ⊢R∈ℝ+∧R<π∧A∈0ball⁡abs∘−R→abs-10R=0ball⁡abs∘−R
7 1 6 eleqtrrd ⊢R∈ℝ+∧R<π∧A∈0ball⁡abs∘−R→A∈abs-10R
8 absf ⊢abs:ℂ⟶ℝ
9 ffn ⊢abs:ℂ⟶ℝ→absFnℂ
10 elpreima ⊢absFnℂ→A∈abs-10R↔A∈ℂ∧A∈0R
11 8 9 10 mp2b ⊢A∈abs-10R↔A∈ℂ∧A∈0R
12 11 simplbi ⊢A∈abs-10R→A∈ℂ
13 7 12 syl ⊢R∈ℝ+∧R<π∧A∈0ball⁡abs∘−R→A∈ℂ
14 13 imcld ⊢R∈ℝ+∧R<π∧A∈0ball⁡abs∘−R→ℑ⁡A∈ℝ
15 14 recnd ⊢R∈ℝ+∧R<π∧A∈0ball⁡abs∘−R→ℑ⁡A∈ℂ
16 15 abscld ⊢R∈ℝ+∧R<π∧A∈0ball⁡abs∘−R→ℑ⁡A∈ℝ
17 rpre ⊢R∈ℝ+→R∈ℝ
18 17 ad2antrr ⊢R∈ℝ+∧R<π∧A∈0ball⁡abs∘−R→R∈ℝ
19 pire ⊢π∈ℝ
20 19 a1i ⊢R∈ℝ+∧R<π∧A∈0ball⁡abs∘−R→π∈ℝ
21 13 abscld ⊢R∈ℝ+∧R<π∧A∈0ball⁡abs∘−R→A∈ℝ
22 absimle ⊢A∈ℂ→ℑ⁡A≤A
23 13 22 syl ⊢R∈ℝ+∧R<π∧A∈0ball⁡abs∘−R→ℑ⁡A≤A
24 11 simprbi ⊢A∈abs-10R→A∈0R
25 7 24 syl ⊢R∈ℝ+∧R<π∧A∈0ball⁡abs∘−R→A∈0R
26 0re ⊢0∈ℝ
27 elico2 ⊢0∈ℝ∧R∈ℝ*→A∈0R↔A∈ℝ∧0≤A∧A<R
28 26 3 27 sylancr ⊢R∈ℝ+∧R<π∧A∈0ball⁡abs∘−R→A∈0R↔A∈ℝ∧0≤A∧A<R
29 25 28 mpbid ⊢R∈ℝ+∧R<π∧A∈0ball⁡abs∘−R→A∈ℝ∧0≤A∧A<R
30 29 simp3d ⊢R∈ℝ+∧R<π∧A∈0ball⁡abs∘−R→A<R
31 16 21 18 23 30 lelttrd ⊢R∈ℝ+∧R<π∧A∈0ball⁡abs∘−R→ℑ⁡A<R
32 simplr ⊢R∈ℝ+∧R<π∧A∈0ball⁡abs∘−R→R<π
33 16 18 20 31 32 lttrd ⊢R∈ℝ+∧R<π∧A∈0ball⁡abs∘−R→ℑ⁡A<π