radcnvle

Description: If X is a convergent point of the infinite series, then X is within the closed disk of radius R centered at zero. Or, by contraposition, the series diverges at any point strictly more than R from the origin. (Contributed by Mario Carneiro, 26-Feb-2015)

	Ref	Expression
Hypotheses	pser.g	⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
	radcnv.a	⊢ ( 𝜑 → 𝐴 : ℕ₀ ⟶ ℂ )
	radcnv.r	⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ^* , < )
	radcnvle.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	radcnvle.a	⊢ ( 𝜑 → seq 0 ( + , ( 𝐺 ‘ 𝑋 ) ) ∈ dom ⇝ )
Assertion	radcnvle	⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ≤ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		pser.g	⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
2		radcnv.a	⊢ ( 𝜑 → 𝐴 : ℕ₀ ⟶ ℂ )
3		radcnv.r	⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ^* , < )
4		radcnvle.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
5		radcnvle.a	⊢ ( 𝜑 → seq 0 ( + , ( 𝐺 ‘ 𝑋 ) ) ∈ dom ⇝ )
6		ressxr	⊢ ℝ ⊆ ℝ^*
7	4	abscld	⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℝ )
8	6 7	sseldi	⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℝ^* )
9		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ^*
10	1 2 3	radcnvcl	⊢ ( 𝜑 → 𝑅 ∈ ( 0 [,] +∞ ) )
11	9 10	sseldi	⊢ ( 𝜑 → 𝑅 ∈ ℝ^* )
12		simpr	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 𝑅 < ( abs ‘ 𝑋 ) )
13	11	adantr	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 𝑅 ∈ ℝ^* )
14	7	adantr	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( abs ‘ 𝑋 ) ∈ ℝ )
15		0xr	⊢ 0 ∈ ℝ^*
16		pnfxr	⊢ +∞ ∈ ℝ^*
17		elicc1	⊢ ( ( 0 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ) → ( 𝑅 ∈ ( 0 [,] +∞ ) ↔ ( 𝑅 ∈ ℝ^* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞ ) ) )
18	15 16 17	mp2an	⊢ ( 𝑅 ∈ ( 0 [,] +∞ ) ↔ ( 𝑅 ∈ ℝ^* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞ ) )
19	10 18	sylib	⊢ ( 𝜑 → ( 𝑅 ∈ ℝ^* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞ ) )
20	19	simp2d	⊢ ( 𝜑 → 0 ≤ 𝑅 )
21		ge0gtmnf	⊢ ( ( 𝑅 ∈ ℝ^* ∧ 0 ≤ 𝑅 ) → -∞ < 𝑅 )
22	11 20 21	syl2anc	⊢ ( 𝜑 → -∞ < 𝑅 )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → -∞ < 𝑅 )
24	8	adantr	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( abs ‘ 𝑋 ) ∈ ℝ^* )
25	13 24 12	xrltled	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 𝑅 ≤ ( abs ‘ 𝑋 ) )
26		xrre	⊢ ( ( ( 𝑅 ∈ ℝ^* ∧ ( abs ‘ 𝑋 ) ∈ ℝ ) ∧ ( -∞ < 𝑅 ∧ 𝑅 ≤ ( abs ‘ 𝑋 ) ) ) → 𝑅 ∈ ℝ )
27	13 14 23 25 26	syl22anc	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 𝑅 ∈ ℝ )
28		avglt1	⊢ ( ( 𝑅 ∈ ℝ ∧ ( abs ‘ 𝑋 ) ∈ ℝ ) → ( 𝑅 < ( abs ‘ 𝑋 ) ↔ 𝑅 < ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) )
29	27 14 28	syl2anc	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( 𝑅 < ( abs ‘ 𝑋 ) ↔ 𝑅 < ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) )
30	12 29	mpbid	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 𝑅 < ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) )
31	27 14	readdcld	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( 𝑅 + ( abs ‘ 𝑋 ) ) ∈ ℝ )
32	31	rehalfcld	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ∈ ℝ )
33		ssrab2	⊢ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ
34	33 6	sstri	⊢ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ^*
35	2	adantr	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 𝐴 : ℕ₀ ⟶ ℂ )
36	32	recnd	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ∈ ℂ )
37	4	adantr	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 𝑋 ∈ ℂ )
38		0red	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 0 ∈ ℝ )
39	20	adantr	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 0 ≤ 𝑅 )
40	38 27 32 39 30	lelttrd	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 0 < ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) )
41	38 32 40	ltled	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 0 ≤ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) )
42	32 41	absidd	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( abs ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) = ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) )
43		avglt2	⊢ ( ( 𝑅 ∈ ℝ ∧ ( abs ‘ 𝑋 ) ∈ ℝ ) → ( 𝑅 < ( abs ‘ 𝑋 ) ↔ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) < ( abs ‘ 𝑋 ) ) )
44	27 14 43	syl2anc	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( 𝑅 < ( abs ‘ 𝑋 ) ↔ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) < ( abs ‘ 𝑋 ) ) )
45	12 44	mpbid	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) < ( abs ‘ 𝑋 ) )
46	42 45	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( abs ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) < ( abs ‘ 𝑋 ) )
47	5	adantr	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → seq 0 ( + , ( 𝐺 ‘ 𝑋 ) ) ∈ dom ⇝ )
48	1 35 36 37 46 47	radcnvlem3	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → seq 0 ( + , ( 𝐺 ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) ) ∈ dom ⇝ )
49		fveq2	⊢ ( 𝑦 = ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) )
50	49	seqeq3d	⊢ ( 𝑦 = ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) → seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) = seq 0 ( + , ( 𝐺 ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) ) )
51	50	eleq1d	⊢ ( 𝑦 = ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) → ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( 𝐺 ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) ) ∈ dom ⇝ ) )
52		fveq2	⊢ ( 𝑟 = 𝑦 → ( 𝐺 ‘ 𝑟 ) = ( 𝐺 ‘ 𝑦 ) )
53	52	seqeq3d	⊢ ( 𝑟 = 𝑦 → seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) = seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) )
54	53	eleq1d	⊢ ( 𝑟 = 𝑦 → ( seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ∈ dom ⇝ ) )
55	54	cbvrabv	⊢ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } = { 𝑦 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ∈ dom ⇝ }
56	51 55	elrab2	⊢ ( ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ↔ ( ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ∈ ℝ ∧ seq 0 ( + , ( 𝐺 ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) ) ∈ dom ⇝ ) )
57	32 48 56	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } )
58		supxrub	⊢ ( ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ^* ∧ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ≤ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ^* , < ) )
59	34 57 58	sylancr	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ≤ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ^* , < ) )
60	59 3	breqtrrdi	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ≤ 𝑅 )
61	32 27 60	lensymd	⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ¬ 𝑅 < ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) )
62	30 61	pm2.65da	⊢ ( 𝜑 → ¬ 𝑅 < ( abs ‘ 𝑋 ) )
63	8 11 62	xrnltled	⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ≤ 𝑅 )

Metamath Proof Explorer

Theorem radcnvle

Proof