Theorem psercnlem1

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 [,) 𝑅 ) )
	psercn.m	⊢ 𝑀 = if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) )
Assertion	psercnlem1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑀 ∈ ℝ+ ∧ ( abs ‘ 𝑎 ) < 𝑀 ∧ 𝑀 < 𝑅 ) )

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		readdcl	⊢ ( ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) + 𝑅 ) ∈ ℝ )
16	14 15	sylan	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑅 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) + 𝑅 ) ∈ ℝ )
17	16	rehalfcld	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑅 ∈ ℝ ) → ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) ∈ ℝ )
18		peano2re	⊢ ( ( abs ‘ 𝑎 ) ∈ ℝ → ( ( abs ‘ 𝑎 ) + 1 ) ∈ ℝ )
19	14 18	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( abs ‘ 𝑎 ) + 1 ) ∈ ℝ )
20	19	adantr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ¬ 𝑅 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) + 1 ) ∈ ℝ )
21	17 20	ifclda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) ∈ ℝ )
22	6 21	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 ∈ ℝ )
23		0re	⊢ 0 ∈ ℝ
24	23	a1i	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 0 ∈ ℝ )
25	13	absge0d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 0 ≤ ( abs ‘ 𝑎 ) )
26		breq2	⊢ ( ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) = if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) → ( ( abs ‘ 𝑎 ) < ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) ↔ ( abs ‘ 𝑎 ) < if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) ) )
27		breq2	⊢ ( ( ( abs ‘ 𝑎 ) + 1 ) = if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) → ( ( abs ‘ 𝑎 ) < ( ( abs ‘ 𝑎 ) + 1 ) ↔ ( abs ‘ 𝑎 ) < if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) ) )
28		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ 𝑆 )
29	28 5	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ ( ◡ abs “ ( 0 [,) 𝑅 ) ) )
30		ffn	⊢ ( abs : ℂ ⟶ ℝ → abs Fn ℂ )
31		elpreima	⊢ ( abs Fn ℂ → ( 𝑎 ∈ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ↔ ( 𝑎 ∈ ℂ ∧ ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑅 ) ) ) )
32	8 30 31	mp2b	⊢ ( 𝑎 ∈ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ↔ ( 𝑎 ∈ ℂ ∧ ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑅 ) ) )
33	29 32	sylib	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑎 ∈ ℂ ∧ ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑅 ) ) )
34	33	simprd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑅 ) )
35		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
36	1 3 4	radcnvcl	⊢ ( 𝜑 → 𝑅 ∈ ( 0 [,] +∞ ) )
37	36	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑅 ∈ ( 0 [,] +∞ ) )
38	35 37	sselid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑅 ∈ ℝ* )
39		elico2	⊢ ( ( 0 ∈ ℝ ∧ 𝑅 ∈ ℝ* ) → ( ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑅 ) ↔ ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑎 ) ∧ ( abs ‘ 𝑎 ) < 𝑅 ) ) )
40	23 38 39	sylancr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑅 ) ↔ ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑎 ) ∧ ( abs ‘ 𝑎 ) < 𝑅 ) ) )
41	34 40	mpbid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑎 ) ∧ ( abs ‘ 𝑎 ) < 𝑅 ) )
42	41	simp3d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) < 𝑅 )
43	42	adantr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑅 ∈ ℝ ) → ( abs ‘ 𝑎 ) < 𝑅 )
44		avglt1	⊢ ( ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) < 𝑅 ↔ ( abs ‘ 𝑎 ) < ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) ) )
45	14 44	sylan	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑅 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) < 𝑅 ↔ ( abs ‘ 𝑎 ) < ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) ) )
46	43 45	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑅 ∈ ℝ ) → ( abs ‘ 𝑎 ) < ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) )
47	14	ltp1d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) < ( ( abs ‘ 𝑎 ) + 1 ) )
48	47	adantr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ¬ 𝑅 ∈ ℝ ) → ( abs ‘ 𝑎 ) < ( ( abs ‘ 𝑎 ) + 1 ) )
49	26 27 46 48	ifbothda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) < if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) )
50	49 6	breqtrrdi	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) < 𝑀 )
51	24 14 22 25 50	lelttrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 0 < 𝑀 )
52	22 51	elrpd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 ∈ ℝ+ )
53		breq1	⊢ ( ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) = if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) → ( ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) < 𝑅 ↔ if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) < 𝑅 ) )
54		breq1	⊢ ( ( ( abs ‘ 𝑎 ) + 1 ) = if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) → ( ( ( abs ‘ 𝑎 ) + 1 ) < 𝑅 ↔ if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) < 𝑅 ) )
55		avglt2	⊢ ( ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) < 𝑅 ↔ ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) < 𝑅 ) )
56	14 55	sylan	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑅 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) < 𝑅 ↔ ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) < 𝑅 ) )
57	43 56	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑅 ∈ ℝ ) → ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) < 𝑅 )
58	19	rexrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( abs ‘ 𝑎 ) + 1 ) ∈ ℝ* )
59	38 58	xrlenltd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑅 ≤ ( ( abs ‘ 𝑎 ) + 1 ) ↔ ¬ ( ( abs ‘ 𝑎 ) + 1 ) < 𝑅 ) )
60		0xr	⊢ 0 ∈ ℝ*
61		pnfxr	⊢ +∞ ∈ ℝ*
62		elicc1	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝑅 ∈ ( 0 [,] +∞ ) ↔ ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞ ) ) )
63	60 61 62	mp2an	⊢ ( 𝑅 ∈ ( 0 [,] +∞ ) ↔ ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞ ) )
64	36 63	sylib	⊢ ( 𝜑 → ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞ ) )
65	64	simp2d	⊢ ( 𝜑 → 0 ≤ 𝑅 )
66	65	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 0 ≤ 𝑅 )
67		ge0gtmnf	⊢ ( ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅 ) → -∞ < 𝑅 )
68	38 66 67	syl2anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → -∞ < 𝑅 )
69		xrre	⊢ ( ( ( 𝑅 ∈ ℝ* ∧ ( ( abs ‘ 𝑎 ) + 1 ) ∈ ℝ ) ∧ ( -∞ < 𝑅 ∧ 𝑅 ≤ ( ( abs ‘ 𝑎 ) + 1 ) ) ) → 𝑅 ∈ ℝ )
70	69	expr	⊢ ( ( ( 𝑅 ∈ ℝ* ∧ ( ( abs ‘ 𝑎 ) + 1 ) ∈ ℝ ) ∧ -∞ < 𝑅 ) → ( 𝑅 ≤ ( ( abs ‘ 𝑎 ) + 1 ) → 𝑅 ∈ ℝ ) )
71	38 19 68 70	syl21anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑅 ≤ ( ( abs ‘ 𝑎 ) + 1 ) → 𝑅 ∈ ℝ ) )
72	59 71	sylbird	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ¬ ( ( abs ‘ 𝑎 ) + 1 ) < 𝑅 → 𝑅 ∈ ℝ ) )
73	72	con1d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ¬ 𝑅 ∈ ℝ → ( ( abs ‘ 𝑎 ) + 1 ) < 𝑅 ) )
74	73	imp	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ¬ 𝑅 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) + 1 ) < 𝑅 )
75	53 54 57 74	ifbothda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) < 𝑅 )
76	6 75	eqbrtrid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 < 𝑅 )
77	52 50 76	3jca	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑀 ∈ ℝ+ ∧ ( abs ‘ 𝑎 ) < 𝑀 ∧ 𝑀 < 𝑅 ) )