MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  abelthlem7a Structured version   Visualization version   GIF version

Theorem abelthlem7a 24411
Description: Lemma for abelth 24415. (Contributed by Mario Carneiro, 8-May-2015.)
Hypotheses
Ref Expression
abelth.1 (𝜑𝐴:ℕ0⟶ℂ)
abelth.2 (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )
abelth.3 (𝜑𝑀 ∈ ℝ)
abelth.4 (𝜑 → 0 ≤ 𝑀)
abelth.5 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}
abelth.6 𝐹 = (𝑥𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)))
abelth.7 (𝜑 → seq0( + , 𝐴) ⇝ 0)
abelthlem6.1 (𝜑𝑋 ∈ (𝑆 ∖ {1}))
Assertion
Ref Expression
abelthlem7a (𝜑 → (𝑋 ∈ ℂ ∧ (abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋)))))
Distinct variable groups:   𝑥,𝑛,𝑧,𝑀   𝑛,𝑋,𝑥,𝑧   𝐴,𝑛,𝑥,𝑧   𝜑,𝑛,𝑥   𝑆,𝑛,𝑥
Allowed substitution hints:   𝜑(𝑧)   𝑆(𝑧)   𝐹(𝑥,𝑧,𝑛)

Proof of Theorem abelthlem7a
StepHypRef Expression
1 abelthlem6.1 . . 3 (𝜑𝑋 ∈ (𝑆 ∖ {1}))
21eldifad 3735 . 2 (𝜑𝑋𝑆)
3 oveq2 6801 . . . . 5 (𝑧 = 𝑋 → (1 − 𝑧) = (1 − 𝑋))
43fveq2d 6336 . . . 4 (𝑧 = 𝑋 → (abs‘(1 − 𝑧)) = (abs‘(1 − 𝑋)))
5 fveq2 6332 . . . . . 6 (𝑧 = 𝑋 → (abs‘𝑧) = (abs‘𝑋))
65oveq2d 6809 . . . . 5 (𝑧 = 𝑋 → (1 − (abs‘𝑧)) = (1 − (abs‘𝑋)))
76oveq2d 6809 . . . 4 (𝑧 = 𝑋 → (𝑀 · (1 − (abs‘𝑧))) = (𝑀 · (1 − (abs‘𝑋))))
84, 7breq12d 4799 . . 3 (𝑧 = 𝑋 → ((abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧))) ↔ (abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋)))))
9 abelth.5 . . 3 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}
108, 9elrab2 3518 . 2 (𝑋𝑆 ↔ (𝑋 ∈ ℂ ∧ (abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋)))))
112, 10sylib 208 1 (𝜑 → (𝑋 ∈ ℂ ∧ (abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1631  wcel 2145  {crab 3065  cdif 3720  {csn 4316   class class class wbr 4786  cmpt 4863  dom cdm 5249  wf 6027  cfv 6031  (class class class)co 6793  cc 10136  cr 10137  0cc0 10138  1c1 10139   + caddc 10141   · cmul 10143  cle 10277  cmin 10468  0cn0 11494  seqcseq 13008  cexp 13067  abscabs 14182  cli 14423  Σcsu 14624
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-iota 5994  df-fv 6039  df-ov 6796
This theorem is referenced by:  abelthlem7  24412
  Copyright terms: Public domain W3C validator