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 ‘ 𝑋 ) ) ) ) )