Metamath Proof Explorer

Theorem abelth2

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

Ref Expression
Hypotheses abelth2.1 ⊢φ→A:ℕ0⟶ℂ
abelth2.2 ⊢φ→seq0+A∈dom⁡⇝
abelth2.3 ⊢F=x∈01⟼∑n∈ℕ0A⁡n⁢xn
Assertion abelth2 ⊢φ→F:01⟶cnℂ

Proof

Step Hyp Ref Expression
1 abelth2.1 ⊢φ→A:ℕ0⟶ℂ
2 abelth2.2 ⊢φ→seq0+A∈dom⁡⇝
3 abelth2.3 ⊢F=x∈01⟼∑n∈ℕ0A⁡n⁢xn
4 unitssre ⊢01⊆ℝ
5 ax-resscn ⊢ℝ⊆ℂ
6 4 5 sstri ⊢01⊆ℂ
7 6 a1i ⊢φ→01⊆ℂ
8 1re ⊢1∈ℝ
9 simpr ⊢φ∧z∈01→z∈01
10 elicc01 ⊢z∈01↔z∈ℝ∧0≤z∧z≤1
11 9 10 sylib ⊢φ∧z∈01→z∈ℝ∧0≤z∧z≤1
12 11 simp1d ⊢φ∧z∈01→z∈ℝ
13 resubcl ⊢1∈ℝ∧z∈ℝ→1−z∈ℝ
14 8 12 13 sylancr ⊢φ∧z∈01→1−z∈ℝ
15 14 leidd ⊢φ∧z∈01→1−z≤1−z
16 1red ⊢φ∧z∈01→1∈ℝ
17 11 simp3d ⊢φ∧z∈01→z≤1
18 12 16 17 abssubge0d ⊢φ∧z∈01→1−z=1−z
19 11 simp2d ⊢φ∧z∈01→0≤z
20 12 19 absidd ⊢φ∧z∈01→z=z
21 20 oveq2d ⊢φ∧z∈01→1−z=1−z
22 21 oveq2d ⊢φ∧z∈01→1⁢1−z=1⁢1−z
23 14 recnd ⊢φ∧z∈01→1−z∈ℂ
24 23 mullidd ⊢φ∧z∈01→1⁢1−z=1−z
25 22 24 eqtrd ⊢φ∧z∈01→1⁢1−z=1−z
26 15 18 25 3brtr4d ⊢φ∧z∈01→1−z≤1⁢1−z
27 7 26 ssrabdv ⊢φ→01⊆z∈ℂ|1−z≤1⁢1−z
28 27 resmptd ⊢φ→x∈z∈ℂ|1−z≤1⁢1−z⟼∑n∈ℕ0A⁡n⁢xn↾01=x∈01⟼∑n∈ℕ0A⁡n⁢xn
29 28 3 eqtr4di ⊢φ→x∈z∈ℂ|1−z≤1⁢1−z⟼∑n∈ℕ0A⁡n⁢xn↾01=F
30 1red ⊢φ→1∈ℝ
31 0le1 ⊢0≤1
32 31 a1i ⊢φ→0≤1
33 eqid ⊢z∈ℂ|1−z≤1⁢1−z=z∈ℂ|1−z≤1⁢1−z
34 eqid ⊢x∈z∈ℂ|1−z≤1⁢1−z⟼∑n∈ℕ0A⁡n⁢xn=x∈z∈ℂ|1−z≤1⁢1−z⟼∑n∈ℕ0A⁡n⁢xn
35 1 2 30 32 33 34 abelth ⊢φ→x∈z∈ℂ|1−z≤1⁢1−z⟼∑n∈ℕ0A⁡n⁢xn:z∈ℂ|1−z≤1⁢1−z⟶cnℂ
36 rescncf ⊢01⊆z∈ℂ|1−z≤1⁢1−z→x∈z∈ℂ|1−z≤1⁢1−z⟼∑n∈ℕ0A⁡n⁢xn:z∈ℂ|1−z≤1⁢1−z⟶cnℂ→x∈z∈ℂ|1−z≤1⁢1−z⟼∑n∈ℕ0A⁡n⁢xn↾01:01⟶cnℂ
37 27 35 36 sylc ⊢φ→x∈z∈ℂ|1−z≤1⁢1−z⟼∑n∈ℕ0A⁡n⁢xn↾01:01⟶cnℂ
38 29 37 eqeltrrd ⊢φ→F:01⟶cnℂ