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 ⊢ φ → seq 0 + A ∈ dom ⁡ ⇝
abelth2.3 ⊢ F = x ∈ 0 1 ⟼ ∑ n ∈ ℕ 0 A ⁡ n ⁢ x n
Assertion abelth2 ⊢ φ → F : 0 1 ⟶cn ℂ

Proof

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