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 ⊢ φ → A : ℕ 0 ⟶ ℂ
abelth.2 ⊢ φ → seq 0 + A ∈ dom ⁡ ⇝
abelth.3 ⊢ φ → M ∈ ℝ
abelth.4 ⊢ φ → 0 ≤ M
abelth.5 ⊢ S = z ∈ ℂ | 1 − z ≤ M ⁢ 1 − z
abelth.6 ⊢ F = x ∈ S ⟼ ∑ n ∈ ℕ 0 A ⁡ n ⁢ x n
abelth.7 ⊢ φ → seq 0 + A ⇝ 0
abelthlem6.1 ⊢ φ → X ∈ S ∖ 1
Assertion abelthlem7a ⊢ φ → X ∈ ℂ ∧ 1 − X ≤ M ⁢ 1 − X

Proof

Step Hyp Ref Expression
1 abelth.1 ⊢ φ → A : ℕ 0 ⟶ ℂ
2 abelth.2 ⊢ φ → seq 0 + A ∈ dom ⁡ ⇝
3 abelth.3 ⊢ φ → M ∈ ℝ
4 abelth.4 ⊢ φ → 0 ≤ M
5 abelth.5 ⊢ S = z ∈ ℂ | 1 − z ≤ M ⁢ 1 − z
6 abelth.6 ⊢ F = x ∈ S ⟼ ∑ n ∈ ℕ 0 A ⁡ n ⁢ x n
7 abelth.7 ⊢ φ → seq 0 + A ⇝ 0
8 abelthlem6.1 ⊢ φ → X ∈ S ∖ 1
9 8 eldifad ⊢ φ → X ∈ S
10 oveq2 ⊢ z = X → 1 − z = 1 − X
11 10 fveq2d ⊢ z = X → 1 − z = 1 − X
12 fveq2 ⊢ z = X → z = X
13 12 oveq2d ⊢ z = X → 1 − z = 1 − X
14 13 oveq2d ⊢ z = X → M ⁢ 1 − z = M ⁢ 1 − X
15 11 14 breq12d ⊢ z = X → 1 − z ≤ M ⁢ 1 − z ↔ 1 − X ≤ M ⁢ 1 − X
16 15 5 elrab2 ⊢ X ∈ S ↔ X ∈ ℂ ∧ 1 − X ≤ M ⁢ 1 − X
17 9 16 sylib ⊢ φ → X ∈ ℂ ∧ 1 − X ≤ M ⁢ 1 − X