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 simpr ⊢ φ ∧ z ∈ 0 1 → z ∈ 0 1
10 elicc01 ⊢ z ∈ 0 1 ↔ z ∈ ℝ ∧ 0 ≤ z ∧ z ≤ 1
11 9 10 sylib ⊢ φ ∧ z ∈ 0 1 → z ∈ ℝ ∧ 0 ≤ z ∧ z ≤ 1
12 11 simp1d ⊢ φ ∧ z ∈ 0 1 → z ∈ ℝ
13 resubcl ⊢ 1 ∈ ℝ ∧ z ∈ ℝ → 1 − z ∈ ℝ
14 8 12 13 sylancr ⊢ φ ∧ z ∈ 0 1 → 1 − z ∈ ℝ
15 14 leidd ⊢ φ ∧ z ∈ 0 1 → 1 − z ≤ 1 − z
16 1red ⊢ φ ∧ z ∈ 0 1 → 1 ∈ ℝ
17 11 simp3d ⊢ φ ∧ z ∈ 0 1 → z ≤ 1
18 12 16 17 abssubge0d ⊢ φ ∧ z ∈ 0 1 → 1 − z = 1 − z
19 11 simp2d ⊢ φ ∧ z ∈ 0 1 → 0 ≤ z
20 12 19 absidd ⊢ φ ∧ z ∈ 0 1 → z = z
21 20 oveq2d ⊢ φ ∧ z ∈ 0 1 → 1 − z = 1 − z
22 21 oveq2d ⊢ φ ∧ z ∈ 0 1 → 1 ⁢ 1 − z = 1 ⁢ 1 − z
23 14 recnd ⊢ φ ∧ z ∈ 0 1 → 1 − z ∈ ℂ
24 23 mulid2d ⊢ φ ∧ z ∈ 0 1 → 1 ⁢ 1 − z = 1 − z
25 22 24 eqtrd ⊢ φ ∧ z ∈ 0 1 → 1 ⁢ 1 − z = 1 − z
26 15 18 25 3brtr4d ⊢ φ ∧ z ∈ 0 1 → 1 − z ≤ 1 ⁢ 1 − z
27 7 26 ssrabdv ⊢ φ → 0 1 ⊆ z ∈ ℂ | 1 − z ≤ 1 ⁢ 1 − z
28 27 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
29 28 3 eqtr4di ⊢ φ → x ∈ z ∈ ℂ | 1 − z ≤ 1 ⁢ 1 − z ⟼ ∑ n ∈ ℕ 0 A ⁡ n ⁢ x n ↾ 0 1 = 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 ∈ ℕ 0 A ⁡ n ⁢ x n = x ∈ z ∈ ℂ | 1 − z ≤ 1 ⁢ 1 − z ⟼ ∑ n ∈ ℕ 0 A ⁡ n ⁢ x n
35 1 2 30 32 33 34 abelth ⊢ φ → x ∈ z ∈ ℂ | 1 − z ≤ 1 ⁢ 1 − z ⟼ ∑ n ∈ ℕ 0 A ⁡ n ⁢ x n : z ∈ ℂ | 1 − z ≤ 1 ⁢ 1 − z ⟶cn ℂ
36 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 ℂ
37 27 35 36 sylc ⊢ φ → x ∈ z ∈ ℂ | 1 − z ≤ 1 ⁢ 1 − z ⟼ ∑ n ∈ ℕ 0 A ⁡ n ⁢ x n ↾ 0 1 : 0 1 ⟶cn ℂ
38 29 37 eqeltrrd ⊢ φ → F : 0 1 ⟶cn ℂ