This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( ( 𝑅 ∈ ℝ+ ∧ 𝑅 < π ) ∧ 𝐴 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) → ( abs ‘ ( ℑ ‘ 𝐴 ) ) < π )

Proof

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