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 ⊢ ( 𝜑 → 𝐴 : ℕ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 elicc01 ⊢ ( 𝑧 ∈ ( 0 [,] 1 ) ↔ ( 𝑧 ∈ ℝ ∧ 0 ≤ 𝑧 ∧ 𝑧 ≤ 1 ) )
10 9 bilani ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( 𝑧 ∈ ℝ ∧ 0 ≤ 𝑧 ∧ 𝑧 ≤ 1 ) )
11 10 simp1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → 𝑧 ∈ ℝ )
12 resubcl ⊢ ( ( 1 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 1 − 𝑧 ) ∈ ℝ )
13 8 11 12 sylancr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( 1 − 𝑧 ) ∈ ℝ )
14 13 leidd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( 1 − 𝑧 ) ≤ ( 1 − 𝑧 ) )
15 1red ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → 1 ∈ ℝ )
16 10 simp3d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → 𝑧 ≤ 1 )
17 11 15 16 abssubge0d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( abs ‘ ( 1 − 𝑧 ) ) = ( 1 − 𝑧 ) )
18 10 simp2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → 0 ≤ 𝑧 )
19 11 18 absidd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( abs ‘ 𝑧 ) = 𝑧 )
20 19 oveq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( 1 − ( abs ‘ 𝑧 ) ) = ( 1 − 𝑧 ) )
21 20 oveq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) = ( 1 · ( 1 − 𝑧 ) ) )
22 13 recnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( 1 − 𝑧 ) ∈ ℂ )
23 22 mullidd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( 1 · ( 1 − 𝑧 ) ) = ( 1 − 𝑧 ) )
24 21 23 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) = ( 1 − 𝑧 ) )
25 14 17 24 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) )
26 7 25 ssrabdv ⊢ ( 𝜑 → ( 0 [,] 1 ) ⊆ { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } )
27 26 resmptd ⊢ ( 𝜑 → ( ( 𝑥 ∈ { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ↾ ( 0 [,] 1 ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
28 27 3 eqtr4di ⊢ ( 𝜑 → ( ( 𝑥 ∈ { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ↾ ( 0 [,] 1 ) ) = 𝐹 )
29 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
30 0le1 ⊢ 0 ≤ 1
31 30 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
32 eqid ⊢ { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } = { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) }
33 eqid ⊢ ( 𝑥 ∈ { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) = ( 𝑥 ∈ { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) )
34 1 2 29 31 32 33 abelth ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ∈ ( { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } –cn→ ℂ ) )
35 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→ ℂ ) ) )
36 26 34 35 sylc ⊢ ( 𝜑 → ( ( 𝑥 ∈ { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 1 · ( 1 − ( abs ‘ 𝑧 ) ) ) } ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ↾ ( 0 [,] 1 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
37 28 36 eqeltrrd ⊢ ( 𝜑 → 𝐹 ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )