This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem abelthlem7a

Description: Lemma for abelth . (Contributed by Mario Carneiro, 8-May-2015)

Ref Expression
Hypotheses abelth.1 ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
abelth.2 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
abelth.3 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
abelth.4 ⊢ ( 𝜑 → 0 ≤ 𝑀 )
abelth.5 ⊢ 𝑆 = { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) }
abelth.6 ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) )
abelth.7 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ⇝ 0 )
abelthlem6.1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑆 ∖ { 1 } ) )
Assertion abelthlem7a ( 𝜑 → ( 𝑋 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑋 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 abelth.1 ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
2 abelth.2 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
3 abelth.3 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
4 abelth.4 ⊢ ( 𝜑 → 0 ≤ 𝑀 )
5 abelth.5 ⊢ 𝑆 = { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) }
6 abelth.6 ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) )
7 abelth.7 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ⇝ 0 )
8 abelthlem6.1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑆 ∖ { 1 } ) )
9 8 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
10 oveq2 ⊢ ( 𝑧 = 𝑋 → ( 1 − 𝑧 ) = ( 1 − 𝑋 ) )
11 10 fveq2d ⊢ ( 𝑧 = 𝑋 → ( abs ‘ ( 1 − 𝑧 ) ) = ( abs ‘ ( 1 − 𝑋 ) ) )
12 fveq2 ⊢ ( 𝑧 = 𝑋 → ( abs ‘ 𝑧 ) = ( abs ‘ 𝑋 ) )
13 12 oveq2d ⊢ ( 𝑧 = 𝑋 → ( 1 − ( abs ‘ 𝑧 ) ) = ( 1 − ( abs ‘ 𝑋 ) ) )
14 13 oveq2d ⊢ ( 𝑧 = 𝑋 → ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) = ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) )
15 11 14 breq12d ⊢ ( 𝑧 = 𝑋 → ( ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ↔ ( abs ‘ ( 1 − 𝑋 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) ) )
16 15 5 elrab2 ⊢ ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑋 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) ) )
17 9 16 sylib ⊢ ( 𝜑 → ( 𝑋 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑋 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) ) )