Metamath Proof Explorer

Theorem pserdvlem1

Description: Lemma for pserdv . (Contributed by Mario Carneiro, 7-May-2015)

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

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 psercn.m ⊢ 𝑀 = if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) )
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 1 2 3 4 5 6 psercnlem1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑀 ∈ ℝ+ ∧ ( abs ‘ 𝑎 ) < 𝑀 ∧ 𝑀 < 𝑅 ) )
16 15 simp1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 ∈ ℝ+ )
17 16 rpred ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 ∈ ℝ )
18 14 17 readdcld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( abs ‘ 𝑎 ) + 𝑀 ) ∈ ℝ )
19 0red ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 0 ∈ ℝ )
20 13 absge0d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 0 ≤ ( abs ‘ 𝑎 ) )
21 14 16 ltaddrpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) < ( ( abs ‘ 𝑎 ) + 𝑀 ) )
22 19 14 18 20 21 lelttrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 0 < ( ( abs ‘ 𝑎 ) + 𝑀 ) )
23 18 22 elrpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( abs ‘ 𝑎 ) + 𝑀 ) ∈ ℝ+ )
24 23 rphalfcld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ∈ ℝ+ )
25 15 simp2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) < 𝑀 )
26 avglt1 ⊢ ( ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) < 𝑀 ↔ ( abs ‘ 𝑎 ) < ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) )
27 14 17 26 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( abs ‘ 𝑎 ) < 𝑀 ↔ ( abs ‘ 𝑎 ) < ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) )
28 25 27 mpbid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) < ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) )
29 18 rehalfcld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ∈ ℝ )
30 29 rexrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ∈ ℝ* )
31 17 rexrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 ∈ ℝ* )
32 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
33 1 3 4 radcnvcl ⊢ ( 𝜑 → 𝑅 ∈ ( 0 [,] +∞ ) )
34 32 33 sselid ⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑅 ∈ ℝ* )
36 avglt2 ⊢ ( ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) < 𝑀 ↔ ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) < 𝑀 ) )
37 14 17 36 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( abs ‘ 𝑎 ) < 𝑀 ↔ ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) < 𝑀 ) )
38 25 37 mpbid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) < 𝑀 )
39 15 simp3d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 < 𝑅 )
40 30 31 35 38 39 xrlttrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) < 𝑅 )
41 24 28 40 3jca ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ∈ ℝ+ ∧ ( abs ‘ 𝑎 ) < ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ∧ ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) < 𝑅 ) )