Theorem abelth2

Description: Abel's theorem, restricted to the [ 0 , 1 ] interval. (Contributed by Mario Carneiro, 2-Apr-2015)

	Ref	Expression
Hypotheses	abelth2.1	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
	abelth2.2	⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
	abelth2.3	⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) )
Assertion	abelth2	⊢ ( 𝜑 → 𝐹 ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		abelth2.1	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
2		abelth2.2	⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
3		abelth2.3	⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) )
4		unitssre	⊢ ( 0 [,] 1 ) ⊆ ℝ
5		ax-resscn	⊢ ℝ ⊆ ℂ
6	4 5	sstri	⊢ ( 0 [,] 1 ) ⊆ ℂ
7	6	a1i	⊢ ( 𝜑 → ( 0 [,] 1 ) ⊆ ℂ )
8		1re	⊢ 1 ∈ ℝ
9		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → 𝑧 ∈ ( 0 [,] 1 ) )
10		elicc01	⊢ ( 𝑧 ∈ ( 0 [,] 1 ) ↔ ( 𝑧 ∈ ℝ ∧ 0 ≤ 𝑧 ∧ 𝑧 ≤ 1 ) )
11	9 10	sylib	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( 𝑧 ∈ ℝ ∧ 0 ≤ 𝑧 ∧ 𝑧 ≤ 1 ) )
12	11	simp1d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → 𝑧 ∈ ℝ )
13		resubcl	⊢ ( ( 1 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 1 − 𝑧 ) ∈ ℝ )
14	8 12 13	sylancr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( 1 − 𝑧 ) ∈ ℝ )
15	14	leidd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( 1 − 𝑧 ) ≤ ( 1 − 𝑧 ) )
16		1red	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → 1 ∈ ℝ )
17	11	simp3d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → 𝑧 ≤ 1 )
18	12 16 17	abssubge0d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( abs ‘ ( 1 − 𝑧 ) ) = ( 1 − 𝑧 ) )
19	11	simp2d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → 0 ≤ 𝑧 )
20	12 19	absidd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( abs ‘ 𝑧 ) = 𝑧 )
21	20	oveq2d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( 1 − ( abs ‘ 𝑧 ) ) = ( 1 − 𝑧 ) )
22	21	oveq2d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) = ( 1 · ( 1 − 𝑧 ) ) )
23	14	recnd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( 1 − 𝑧 ) ∈ ℂ )
24	23	mullidd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( 1 · ( 1 − 𝑧 ) ) = ( 1 − 𝑧 ) )
25	22 24	eqtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) = ( 1 − 𝑧 ) )
26	15 18 25	3brtr4d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) )
27	7 26	ssrabdv	⊢ ( 𝜑 → ( 0 [,] 1 ) ⊆ { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } )
28	27	resmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ↾ ( 0 [,] 1 ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
29	28 3	eqtr4di	⊢ ( 𝜑 → ( ( 𝑥 ∈ { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ↾ ( 0 [,] 1 ) ) = 𝐹 )
30		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
31		0le1	⊢ 0 ≤ 1
32	31	a1i	⊢ ( 𝜑 → 0 ≤ 1 )
33		eqid	⊢ { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } = { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) }
34		eqid	⊢ ( 𝑥 ∈ { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) = ( 𝑥 ∈ { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) )
35	1 2 30 32 33 34	abelth	⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ∈ ( { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } –cn→ ℂ ) )
36		rescncf	⊢ ( ( 0 [,] 1 ) ⊆ { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } → ( ( 𝑥 ∈ { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ∈ ( { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } –cn→ ℂ ) → ( ( 𝑥 ∈ { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ↾ ( 0 [,] 1 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) )
37	27 35 36	sylc	⊢ ( 𝜑 → ( ( 𝑥 ∈ { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ↾ ( 0 [,] 1 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
38	29 37	eqeltrrd	⊢ ( 𝜑 → 𝐹 ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )