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

Theorem radcnvlt1 25684
Description: If 𝑋 is within the open disk of radius 𝑅 centered at zero, then the infinite series converges absolutely at 𝑋, and also converges when the series is multiplied by 𝑛. (Contributed by Mario Carneiro, 26-Feb-2015.)
Hypotheses
Ref Expression
pser.g 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))))
radcnv.a (𝜑𝐴:ℕ0⟶ℂ)
radcnv.r 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < )
radcnvlt.x (𝜑𝑋 ∈ ℂ)
radcnvlt.a (𝜑 → (abs‘𝑋) < 𝑅)
radcnvlt1.h 𝐻 = (𝑚 ∈ ℕ0 ↦ (𝑚 · (abs‘((𝐺𝑋)‘𝑚))))
Assertion
Ref Expression
radcnvlt1 (𝜑 → (seq0( + , 𝐻) ∈ dom ⇝ ∧ seq0( + , (abs ∘ (𝐺𝑋))) ∈ dom ⇝ ))
Distinct variable groups:   𝑚,𝑛,𝑥,𝐴   𝑚,𝐻   𝜑,𝑚   𝑚,𝑋   𝑚,𝑟,𝐺
Allowed substitution hints:   𝜑(𝑥,𝑛,𝑟)   𝐴(𝑟)   𝑅(𝑥,𝑚,𝑛,𝑟)   𝐺(𝑥,𝑛)   𝐻(𝑥,𝑛,𝑟)   𝑋(𝑥,𝑛,𝑟)

Proof of Theorem radcnvlt1
Dummy variable 𝑠 is distinct from all other variables.
StepHypRef Expression
1 radcnvlt.a . . . . 5 (𝜑 → (abs‘𝑋) < 𝑅)
2 ressxr 11121 . . . . . . 7 ℝ ⊆ ℝ*
3 radcnvlt.x . . . . . . . 8 (𝜑𝑋 ∈ ℂ)
43abscld 15248 . . . . . . 7 (𝜑 → (abs‘𝑋) ∈ ℝ)
52, 4sselid 3930 . . . . . 6 (𝜑 → (abs‘𝑋) ∈ ℝ*)
6 iccssxr 13264 . . . . . . 7 (0[,]+∞) ⊆ ℝ*
7 pser.g . . . . . . . 8 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))))
8 radcnv.a . . . . . . . 8 (𝜑𝐴:ℕ0⟶ℂ)
9 radcnv.r . . . . . . . 8 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < )
107, 8, 9radcnvcl 25683 . . . . . . 7 (𝜑𝑅 ∈ (0[,]+∞))
116, 10sselid 3930 . . . . . 6 (𝜑𝑅 ∈ ℝ*)
12 xrltnle 11144 . . . . . 6 (((abs‘𝑋) ∈ ℝ*𝑅 ∈ ℝ*) → ((abs‘𝑋) < 𝑅 ↔ ¬ 𝑅 ≤ (abs‘𝑋)))
135, 11, 12syl2anc 584 . . . . 5 (𝜑 → ((abs‘𝑋) < 𝑅 ↔ ¬ 𝑅 ≤ (abs‘𝑋)))
141, 13mpbid 231 . . . 4 (𝜑 → ¬ 𝑅 ≤ (abs‘𝑋))
159breq1i 5100 . . . . . 6 (𝑅 ≤ (abs‘𝑋) ↔ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < ) ≤ (abs‘𝑋))
16 ssrab2 4025 . . . . . . . 8 {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ } ⊆ ℝ
1716, 2sstri 3941 . . . . . . 7 {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ } ⊆ ℝ*
18 supxrleub 13162 . . . . . . 7 (({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ } ⊆ ℝ* ∧ (abs‘𝑋) ∈ ℝ*) → (sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < ) ≤ (abs‘𝑋) ↔ ∀𝑠 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }𝑠 ≤ (abs‘𝑋)))
1917, 5, 18sylancr 587 . . . . . 6 (𝜑 → (sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < ) ≤ (abs‘𝑋) ↔ ∀𝑠 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }𝑠 ≤ (abs‘𝑋)))
2015, 19bitrid 282 . . . . 5 (𝜑 → (𝑅 ≤ (abs‘𝑋) ↔ ∀𝑠 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }𝑠 ≤ (abs‘𝑋)))
21 fveq2 6826 . . . . . . . 8 (𝑟 = 𝑠 → (𝐺𝑟) = (𝐺𝑠))
2221seqeq3d 13831 . . . . . . 7 (𝑟 = 𝑠 → seq0( + , (𝐺𝑟)) = seq0( + , (𝐺𝑠)))
2322eleq1d 2821 . . . . . 6 (𝑟 = 𝑠 → (seq0( + , (𝐺𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝐺𝑠)) ∈ dom ⇝ ))
2423ralrab 3640 . . . . 5 (∀𝑠 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }𝑠 ≤ (abs‘𝑋) ↔ ∀𝑠 ∈ ℝ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ → 𝑠 ≤ (abs‘𝑋)))
2520, 24bitrdi 286 . . . 4 (𝜑 → (𝑅 ≤ (abs‘𝑋) ↔ ∀𝑠 ∈ ℝ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ → 𝑠 ≤ (abs‘𝑋))))
2614, 25mtbid 323 . . 3 (𝜑 → ¬ ∀𝑠 ∈ ℝ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ → 𝑠 ≤ (abs‘𝑋)))
27 rexanali 3101 . . 3 (∃𝑠 ∈ ℝ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ ∧ ¬ 𝑠 ≤ (abs‘𝑋)) ↔ ¬ ∀𝑠 ∈ ℝ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ → 𝑠 ≤ (abs‘𝑋)))
2826, 27sylibr 233 . 2 (𝜑 → ∃𝑠 ∈ ℝ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ ∧ ¬ 𝑠 ≤ (abs‘𝑋)))
29 ltnle 11156 . . . . . . 7 (((abs‘𝑋) ∈ ℝ ∧ 𝑠 ∈ ℝ) → ((abs‘𝑋) < 𝑠 ↔ ¬ 𝑠 ≤ (abs‘𝑋)))
304, 29sylan 580 . . . . . 6 ((𝜑𝑠 ∈ ℝ) → ((abs‘𝑋) < 𝑠 ↔ ¬ 𝑠 ≤ (abs‘𝑋)))
3130adantr 481 . . . . 5 (((𝜑𝑠 ∈ ℝ) ∧ seq0( + , (𝐺𝑠)) ∈ dom ⇝ ) → ((abs‘𝑋) < 𝑠 ↔ ¬ 𝑠 ≤ (abs‘𝑋)))
328ad2antrr 723 . . . . . . . 8 (((𝜑𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → 𝐴:ℕ0⟶ℂ)
333ad2antrr 723 . . . . . . . 8 (((𝜑𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → 𝑋 ∈ ℂ)
34 simplr 766 . . . . . . . . 9 (((𝜑𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → 𝑠 ∈ ℝ)
3534recnd 11105 . . . . . . . 8 (((𝜑𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → 𝑠 ∈ ℂ)
36 simprr 770 . . . . . . . . 9 (((𝜑𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → (abs‘𝑋) < 𝑠)
37 0red 11080 . . . . . . . . . . 11 (((𝜑𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → 0 ∈ ℝ)
3833abscld 15248 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → (abs‘𝑋) ∈ ℝ)
3933absge0d 15256 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → 0 ≤ (abs‘𝑋))
4037, 38, 34, 39, 36lelttrd 11235 . . . . . . . . . . 11 (((𝜑𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → 0 < 𝑠)
4137, 34, 40ltled 11225 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → 0 ≤ 𝑠)
4234, 41absidd 15234 . . . . . . . . 9 (((𝜑𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → (abs‘𝑠) = 𝑠)
4336, 42breqtrrd 5121 . . . . . . . 8 (((𝜑𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → (abs‘𝑋) < (abs‘𝑠))
44 simprl 768 . . . . . . . 8 (((𝜑𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → seq0( + , (𝐺𝑠)) ∈ dom ⇝ )
45 radcnvlt1.h . . . . . . . 8 𝐻 = (𝑚 ∈ ℕ0 ↦ (𝑚 · (abs‘((𝐺𝑋)‘𝑚))))
467, 32, 33, 35, 43, 44, 45radcnvlem1 25679 . . . . . . 7 (((𝜑𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → seq0( + , 𝐻) ∈ dom ⇝ )
477, 32, 33, 35, 43, 44radcnvlem2 25680 . . . . . . 7 (((𝜑𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → seq0( + , (abs ∘ (𝐺𝑋))) ∈ dom ⇝ )
4846, 47jca 512 . . . . . 6 (((𝜑𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → (seq0( + , 𝐻) ∈ dom ⇝ ∧ seq0( + , (abs ∘ (𝐺𝑋))) ∈ dom ⇝ ))
4948expr 457 . . . . 5 (((𝜑𝑠 ∈ ℝ) ∧ seq0( + , (𝐺𝑠)) ∈ dom ⇝ ) → ((abs‘𝑋) < 𝑠 → (seq0( + , 𝐻) ∈ dom ⇝ ∧ seq0( + , (abs ∘ (𝐺𝑋))) ∈ dom ⇝ )))
5031, 49sylbird 259 . . . 4 (((𝜑𝑠 ∈ ℝ) ∧ seq0( + , (𝐺𝑠)) ∈ dom ⇝ ) → (¬ 𝑠 ≤ (abs‘𝑋) → (seq0( + , 𝐻) ∈ dom ⇝ ∧ seq0( + , (abs ∘ (𝐺𝑋))) ∈ dom ⇝ )))
5150expimpd 454 . . 3 ((𝜑𝑠 ∈ ℝ) → ((seq0( + , (𝐺𝑠)) ∈ dom ⇝ ∧ ¬ 𝑠 ≤ (abs‘𝑋)) → (seq0( + , 𝐻) ∈ dom ⇝ ∧ seq0( + , (abs ∘ (𝐺𝑋))) ∈ dom ⇝ )))
5251rexlimdva 3148 . 2 (𝜑 → (∃𝑠 ∈ ℝ (seq0( + , (𝐺𝑠)) ∈ dom ⇝ ∧ ¬ 𝑠 ≤ (abs‘𝑋)) → (seq0( + , 𝐻) ∈ dom ⇝ ∧ seq0( + , (abs ∘ (𝐺𝑋))) ∈ dom ⇝ )))
5328, 52mpd 15 1 (𝜑 → (seq0( + , 𝐻) ∈ dom ⇝ ∧ seq0( + , (abs ∘ (𝐺𝑋))) ∈ dom ⇝ ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1540  wcel 2105  wral 3061  wrex 3070  {crab 3403  wss 3898   class class class wbr 5093  cmpt 5176  dom cdm 5621  ccom 5625  wf 6476  cfv 6480  (class class class)co 7338  supcsup 9298  cc 10971  cr 10972  0cc0 10973   + caddc 10976   · cmul 10978  +∞cpnf 11108  *cxr 11110   < clt 11111  cle 11112  0cn0 12335  [,]cicc 13184  seqcseq 13823  cexp 13884  abscabs 15045  cli 15293
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5230  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651  ax-inf2 9499  ax-cnex 11029  ax-resscn 11030  ax-1cn 11031  ax-icn 11032  ax-addcl 11033  ax-addrcl 11034  ax-mulcl 11035  ax-mulrcl 11036  ax-mulcom 11037  ax-addass 11038  ax-mulass 11039  ax-distr 11040  ax-i2m1 11041  ax-1ne0 11042  ax-1rid 11043  ax-rnegex 11044  ax-rrecex 11045  ax-cnre 11046  ax-pre-lttri 11047  ax-pre-lttrn 11048  ax-pre-ltadd 11049  ax-pre-mulgt0 11050  ax-pre-sup 11051
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-int 4896  df-iun 4944  df-br 5094  df-opab 5156  df-mpt 5177  df-tr 5211  df-id 5519  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5576  df-se 5577  df-we 5578  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6239  df-ord 6306  df-on 6307  df-lim 6308  df-suc 6309  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-isom 6489  df-riota 7294  df-ov 7341  df-oprab 7342  df-mpo 7343  df-om 7782  df-1st 7900  df-2nd 7901  df-frecs 8168  df-wrecs 8199  df-recs 8273  df-rdg 8312  df-1o 8368  df-er 8570  df-pm 8690  df-en 8806  df-dom 8807  df-sdom 8808  df-fin 8809  df-sup 9300  df-inf 9301  df-oi 9368  df-card 9797  df-pnf 11113  df-mnf 11114  df-xr 11115  df-ltxr 11116  df-le 11117  df-sub 11309  df-neg 11310  df-div 11735  df-nn 12076  df-2 12138  df-3 12139  df-n0 12336  df-z 12422  df-uz 12685  df-rp 12833  df-ico 13187  df-icc 13188  df-fz 13342  df-fzo 13485  df-fl 13614  df-seq 13824  df-exp 13885  df-hash 14147  df-cj 14910  df-re 14911  df-im 14912  df-sqrt 15046  df-abs 15047  df-limsup 15280  df-clim 15297  df-rlim 15298  df-sum 15498
This theorem is referenced by:  radcnvlt2  25685  dvradcnv  25687  pserulm  25688
  Copyright terms: Public domain W3C validator