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 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 mulid2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 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→ ℂ ) )