Metamath Proof Explorer

Theorem psercnlem2

Description: Lemma for psercn . (Contributed by Mario Carneiro, 18-Mar-2015)

Ref Expression
Hypotheses pserf.g ⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
pserf.f ⊢ 𝐹 = ( 𝑦 ∈ 𝑆 ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) )
pserf.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
pserf.r ⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
psercn.s ⊢ 𝑆 = ( ◡ abs “ ( 0 [,) 𝑅 ) )
psercnlem2.i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑀 ∈ ℝ+ ∧ ( abs ‘ 𝑎 ) < 𝑀 ∧ 𝑀 < 𝑅 ) )
Assertion psercnlem2 ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑎 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ∧ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ⊆ ( ◡ abs “ ( 0 [,] 𝑀 ) ) ∧ ( ◡ abs “ ( 0 [,] 𝑀 ) ) ⊆ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 pserf.g ⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
2 pserf.f ⊢ 𝐹 = ( 𝑦 ∈ 𝑆 ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) )
3 pserf.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
4 pserf.r ⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
5 psercn.s ⊢ 𝑆 = ( ◡ abs “ ( 0 [,) 𝑅 ) )
6 psercnlem2.i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑀 ∈ ℝ+ ∧ ( abs ‘ 𝑎 ) < 𝑀 ∧ 𝑀 < 𝑅 ) )
7 cnvimass ⊢ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ⊆ dom abs
8 absf ⊢ abs : ℂ ⟶ ℝ
9 8 fdmi ⊢ dom abs = ℂ
10 7 9 sseqtri ⊢ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ⊆ ℂ
11 5 10 eqsstri ⊢ 𝑆 ⊆ ℂ
12 11 a1i ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
13 12 sselda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ ℂ )
14 13 abscld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) ∈ ℝ )
15 13 absge0d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 0 ≤ ( abs ‘ 𝑎 ) )
16 6 simp2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) < 𝑀 )
17 0re ⊢ 0 ∈ ℝ
18 6 simp1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 ∈ ℝ+ )
19 18 rpxrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 ∈ ℝ* )
20 elico2 ⊢ ( ( 0 ∈ ℝ ∧ 𝑀 ∈ ℝ* ) → ( ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑀 ) ↔ ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑎 ) ∧ ( abs ‘ 𝑎 ) < 𝑀 ) ) )
21 17 19 20 sylancr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑀 ) ↔ ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑎 ) ∧ ( abs ‘ 𝑎 ) < 𝑀 ) ) )
22 14 15 16 21 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑀 ) )
23 ffn ⊢ ( abs : ℂ ⟶ ℝ → abs Fn ℂ )
24 elpreima ⊢ ( abs Fn ℂ → ( 𝑎 ∈ ( ◡ abs “ ( 0 [,) 𝑀 ) ) ↔ ( 𝑎 ∈ ℂ ∧ ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑀 ) ) ) )
25 8 23 24 mp2b ⊢ ( 𝑎 ∈ ( ◡ abs “ ( 0 [,) 𝑀 ) ) ↔ ( 𝑎 ∈ ℂ ∧ ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑀 ) ) )
26 13 22 25 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ ( ◡ abs “ ( 0 [,) 𝑀 ) ) )
27 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
28 27 cnbl0 ⊢ ( 𝑀 ∈ ℝ* → ( ◡ abs “ ( 0 [,) 𝑀 ) ) = ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) )
29 19 28 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ◡ abs “ ( 0 [,) 𝑀 ) ) = ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) )
30 26 29 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) )
31 icossicc ⊢ ( 0 [,) 𝑀 ) ⊆ ( 0 [,] 𝑀 )
32 imass2 ⊢ ( ( 0 [,) 𝑀 ) ⊆ ( 0 [,] 𝑀 ) → ( ◡ abs “ ( 0 [,) 𝑀 ) ) ⊆ ( ◡ abs “ ( 0 [,] 𝑀 ) ) )
33 31 32 mp1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ◡ abs “ ( 0 [,) 𝑀 ) ) ⊆ ( ◡ abs “ ( 0 [,] 𝑀 ) ) )
34 29 33 eqsstrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ⊆ ( ◡ abs “ ( 0 [,] 𝑀 ) ) )
35 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
36 1 3 4 radcnvcl ⊢ ( 𝜑 → 𝑅 ∈ ( 0 [,] +∞ ) )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑅 ∈ ( 0 [,] +∞ ) )
38 35 37 sseldi ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑅 ∈ ℝ* )
39 6 simp3d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 < 𝑅 )
40 df-ico ⊢ [,) = ( 𝑢 ∈ ℝ* , 𝑣 ∈ ℝ* ↦ { 𝑤 ∈ ℝ* ∣ ( 𝑢 ≤ 𝑤 ∧ 𝑤 < 𝑣 ) } )
41 df-icc ⊢ [,] = ( 𝑢 ∈ ℝ* , 𝑣 ∈ ℝ* ↦ { 𝑤 ∈ ℝ* ∣ ( 𝑢 ≤ 𝑤 ∧ 𝑤 ≤ 𝑣 ) } )
42 xrlelttr ⊢ ( ( 𝑧 ∈ ℝ* ∧ 𝑀 ∈ ℝ* ∧ 𝑅 ∈ ℝ* ) → ( ( 𝑧 ≤ 𝑀 ∧ 𝑀 < 𝑅 ) → 𝑧 < 𝑅 ) )
43 40 41 42 ixxss2 ⊢ ( ( 𝑅 ∈ ℝ* ∧ 𝑀 < 𝑅 ) → ( 0 [,] 𝑀 ) ⊆ ( 0 [,) 𝑅 ) )
44 38 39 43 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 0 [,] 𝑀 ) ⊆ ( 0 [,) 𝑅 ) )
45 imass2 ⊢ ( ( 0 [,] 𝑀 ) ⊆ ( 0 [,) 𝑅 ) → ( ◡ abs “ ( 0 [,] 𝑀 ) ) ⊆ ( ◡ abs “ ( 0 [,) 𝑅 ) ) )
46 44 45 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ◡ abs “ ( 0 [,] 𝑀 ) ) ⊆ ( ◡ abs “ ( 0 [,) 𝑅 ) ) )
47 46 5 sseqtrrdi ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ◡ abs “ ( 0 [,] 𝑀 ) ) ⊆ 𝑆 )
48 30 34 47 3jca ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑎 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ∧ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ⊆ ( ◡ abs “ ( 0 [,] 𝑀 ) ) ∧ ( ◡ abs “ ( 0 [,] 𝑀 ) ) ⊆ 𝑆 ) )