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 ) < 𝑅 ) )