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

Theorem geolim3 24621
Description: Geometric series convergence with arbitrary shift, radix, and multiplicative constant. (Contributed by Stefan O'Rear, 16-Nov-2014.)
Hypotheses
Ref Expression
geolim3.a (𝜑𝐴 ∈ ℤ)
geolim3.b1 (𝜑𝐵 ∈ ℂ)
geolim3.b2 (𝜑 → (abs‘𝐵) < 1)
geolim3.c (𝜑𝐶 ∈ ℂ)
geolim3.f 𝐹 = (𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴))))
Assertion
Ref Expression
geolim3 (𝜑 → seq𝐴( + , 𝐹) ⇝ (𝐶 / (1 − 𝐵)))
Distinct variable groups:   𝜑,𝑘   𝐴,𝑘   𝐵,𝑘   𝐶,𝑘
Allowed substitution hint:   𝐹(𝑘)

Proof of Theorem geolim3
Dummy variable 𝑎 is distinct from all other variables.
StepHypRef Expression
1 geolim3.f . . 3 𝐹 = (𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴))))
2 seqeq3 13182 . . 3 (𝐹 = (𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴)))) → seq𝐴( + , 𝐹) = seq𝐴( + , (𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴))))))
31, 2ax-mp 5 . 2 seq𝐴( + , 𝐹) = seq𝐴( + , (𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴)))))
4 nn0uz 12087 . . . . 5 0 = (ℤ‘0)
5 0zd 11798 . . . . 5 (𝜑 → 0 ∈ ℤ)
6 geolim3.c . . . . 5 (𝜑𝐶 ∈ ℂ)
7 geolim3.b1 . . . . . 6 (𝜑𝐵 ∈ ℂ)
8 geolim3.b2 . . . . . 6 (𝜑 → (abs‘𝐵) < 1)
9 oveq2 6978 . . . . . . . 8 (𝑘 = 𝑎 → (𝐵𝑘) = (𝐵𝑎))
10 eqid 2772 . . . . . . . 8 (𝑘 ∈ ℕ0 ↦ (𝐵𝑘)) = (𝑘 ∈ ℕ0 ↦ (𝐵𝑘))
11 ovex 7002 . . . . . . . 8 (𝐵𝑎) ∈ V
129, 10, 11fvmpt 6589 . . . . . . 7 (𝑎 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (𝐵𝑘))‘𝑎) = (𝐵𝑎))
1312adantl 474 . . . . . 6 ((𝜑𝑎 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (𝐵𝑘))‘𝑎) = (𝐵𝑎))
147, 8, 13geolim 15076 . . . . 5 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ (𝐵𝑘))) ⇝ (1 / (1 − 𝐵)))
15 expcl 13255 . . . . . . 7 ((𝐵 ∈ ℂ ∧ 𝑎 ∈ ℕ0) → (𝐵𝑎) ∈ ℂ)
167, 15sylan 572 . . . . . 6 ((𝜑𝑎 ∈ ℕ0) → (𝐵𝑎) ∈ ℂ)
1713, 16eqeltrd 2860 . . . . 5 ((𝜑𝑎 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (𝐵𝑘))‘𝑎) ∈ ℂ)
18 geolim3.a . . . . . . . 8 (𝜑𝐴 ∈ ℤ)
1918zcnd 11894 . . . . . . 7 (𝜑𝐴 ∈ ℂ)
20 nn0cn 11711 . . . . . . 7 (𝑎 ∈ ℕ0𝑎 ∈ ℂ)
21 fvex 6506 . . . . . . . . 9 (ℤ𝐴) ∈ V
2221mptex 6806 . . . . . . . 8 (𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴)))) ∈ V
2322shftval4 14287 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑎 ∈ ℂ) → (((𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴)))) shift -𝐴)‘𝑎) = ((𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴))))‘(𝐴 + 𝑎)))
2419, 20, 23syl2an 586 . . . . . 6 ((𝜑𝑎 ∈ ℕ0) → (((𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴)))) shift -𝐴)‘𝑎) = ((𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴))))‘(𝐴 + 𝑎)))
25 uzid 12066 . . . . . . . . 9 (𝐴 ∈ ℤ → 𝐴 ∈ (ℤ𝐴))
2618, 25syl 17 . . . . . . . 8 (𝜑𝐴 ∈ (ℤ𝐴))
27 uzaddcl 12111 . . . . . . . 8 ((𝐴 ∈ (ℤ𝐴) ∧ 𝑎 ∈ ℕ0) → (𝐴 + 𝑎) ∈ (ℤ𝐴))
2826, 27sylan 572 . . . . . . 7 ((𝜑𝑎 ∈ ℕ0) → (𝐴 + 𝑎) ∈ (ℤ𝐴))
29 oveq1 6977 . . . . . . . . . 10 (𝑘 = (𝐴 + 𝑎) → (𝑘𝐴) = ((𝐴 + 𝑎) − 𝐴))
3029oveq2d 6986 . . . . . . . . 9 (𝑘 = (𝐴 + 𝑎) → (𝐵↑(𝑘𝐴)) = (𝐵↑((𝐴 + 𝑎) − 𝐴)))
3130oveq2d 6986 . . . . . . . 8 (𝑘 = (𝐴 + 𝑎) → (𝐶 · (𝐵↑(𝑘𝐴))) = (𝐶 · (𝐵↑((𝐴 + 𝑎) − 𝐴))))
32 eqid 2772 . . . . . . . 8 (𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴)))) = (𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴))))
33 ovex 7002 . . . . . . . 8 (𝐶 · (𝐵↑((𝐴 + 𝑎) − 𝐴))) ∈ V
3431, 32, 33fvmpt 6589 . . . . . . 7 ((𝐴 + 𝑎) ∈ (ℤ𝐴) → ((𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴))))‘(𝐴 + 𝑎)) = (𝐶 · (𝐵↑((𝐴 + 𝑎) − 𝐴))))
3528, 34syl 17 . . . . . 6 ((𝜑𝑎 ∈ ℕ0) → ((𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴))))‘(𝐴 + 𝑎)) = (𝐶 · (𝐵↑((𝐴 + 𝑎) − 𝐴))))
36 pncan2 10685 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝑎 ∈ ℂ) → ((𝐴 + 𝑎) − 𝐴) = 𝑎)
3719, 20, 36syl2an 586 . . . . . . . . 9 ((𝜑𝑎 ∈ ℕ0) → ((𝐴 + 𝑎) − 𝐴) = 𝑎)
3837oveq2d 6986 . . . . . . . 8 ((𝜑𝑎 ∈ ℕ0) → (𝐵↑((𝐴 + 𝑎) − 𝐴)) = (𝐵𝑎))
3938, 13eqtr4d 2811 . . . . . . 7 ((𝜑𝑎 ∈ ℕ0) → (𝐵↑((𝐴 + 𝑎) − 𝐴)) = ((𝑘 ∈ ℕ0 ↦ (𝐵𝑘))‘𝑎))
4039oveq2d 6986 . . . . . 6 ((𝜑𝑎 ∈ ℕ0) → (𝐶 · (𝐵↑((𝐴 + 𝑎) − 𝐴))) = (𝐶 · ((𝑘 ∈ ℕ0 ↦ (𝐵𝑘))‘𝑎)))
4124, 35, 403eqtrd 2812 . . . . 5 ((𝜑𝑎 ∈ ℕ0) → (((𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴)))) shift -𝐴)‘𝑎) = (𝐶 · ((𝑘 ∈ ℕ0 ↦ (𝐵𝑘))‘𝑎)))
424, 5, 6, 14, 17, 41isermulc2 14865 . . . 4 (𝜑 → seq0( + , ((𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴)))) shift -𝐴)) ⇝ (𝐶 · (1 / (1 − 𝐵))))
4319negidd 10780 . . . . 5 (𝜑 → (𝐴 + -𝐴) = 0)
4443seqeq1d 13183 . . . 4 (𝜑 → seq(𝐴 + -𝐴)( + , ((𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴)))) shift -𝐴)) = seq0( + , ((𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴)))) shift -𝐴)))
45 ax-1cn 10385 . . . . . 6 1 ∈ ℂ
46 subcl 10677 . . . . . 6 ((1 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 − 𝐵) ∈ ℂ)
4745, 7, 46sylancr 578 . . . . 5 (𝜑 → (1 − 𝐵) ∈ ℂ)
48 abs1 14508 . . . . . . . . 9 (abs‘1) = 1
4948a1i 11 . . . . . . . 8 (𝜑 → (abs‘1) = 1)
507abscld 14647 . . . . . . . . 9 (𝜑 → (abs‘𝐵) ∈ ℝ)
5150, 8gtned 10567 . . . . . . . 8 (𝜑 → 1 ≠ (abs‘𝐵))
5249, 51eqnetrd 3028 . . . . . . 7 (𝜑 → (abs‘1) ≠ (abs‘𝐵))
53 fveq2 6493 . . . . . . . 8 (1 = 𝐵 → (abs‘1) = (abs‘𝐵))
5453necon3i 2993 . . . . . . 7 ((abs‘1) ≠ (abs‘𝐵) → 1 ≠ 𝐵)
5552, 54syl 17 . . . . . 6 (𝜑 → 1 ≠ 𝐵)
56 subeq0 10705 . . . . . . . 8 ((1 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 − 𝐵) = 0 ↔ 1 = 𝐵))
5745, 7, 56sylancr 578 . . . . . . 7 (𝜑 → ((1 − 𝐵) = 0 ↔ 1 = 𝐵))
5857necon3bid 3005 . . . . . 6 (𝜑 → ((1 − 𝐵) ≠ 0 ↔ 1 ≠ 𝐵))
5955, 58mpbird 249 . . . . 5 (𝜑 → (1 − 𝐵) ≠ 0)
606, 47, 59divrecd 11212 . . . 4 (𝜑 → (𝐶 / (1 − 𝐵)) = (𝐶 · (1 / (1 − 𝐵))))
6142, 44, 603brtr4d 4955 . . 3 (𝜑 → seq(𝐴 + -𝐴)( + , ((𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴)))) shift -𝐴)) ⇝ (𝐶 / (1 − 𝐵)))
6218znegcld 11895 . . . 4 (𝜑 → -𝐴 ∈ ℤ)
6322isershft 14871 . . . 4 ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℤ) → (seq𝐴( + , (𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴))))) ⇝ (𝐶 / (1 − 𝐵)) ↔ seq(𝐴 + -𝐴)( + , ((𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴)))) shift -𝐴)) ⇝ (𝐶 / (1 − 𝐵))))
6418, 62, 63syl2anc 576 . . 3 (𝜑 → (seq𝐴( + , (𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴))))) ⇝ (𝐶 / (1 − 𝐵)) ↔ seq(𝐴 + -𝐴)( + , ((𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴)))) shift -𝐴)) ⇝ (𝐶 / (1 − 𝐵))))
6561, 64mpbird 249 . 2 (𝜑 → seq𝐴( + , (𝑘 ∈ (ℤ𝐴) ↦ (𝐶 · (𝐵↑(𝑘𝐴))))) ⇝ (𝐶 / (1 − 𝐵)))
663, 65syl5eqbr 4958 1 (𝜑 → seq𝐴( + , 𝐹) ⇝ (𝐶 / (1 − 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387   = wceq 1507  wcel 2048  wne 2961   class class class wbr 4923  cmpt 5002  cfv 6182  (class class class)co 6970  cc 10325  0cc0 10327  1c1 10328   + caddc 10330   · cmul 10332   < clt 10466  cmin 10662  -cneg 10663   / cdiv 11090  0cn0 11700  cz 11786  cuz 12051  seqcseq 13177  cexp 13237   shift cshi 14276  abscabs 14444  cli 14692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-inf2 8890  ax-cnex 10383  ax-resscn 10384  ax-1cn 10385  ax-icn 10386  ax-addcl 10387  ax-addrcl 10388  ax-mulcl 10389  ax-mulrcl 10390  ax-mulcom 10391  ax-addass 10392  ax-mulass 10393  ax-distr 10394  ax-i2m1 10395  ax-1ne0 10396  ax-1rid 10397  ax-rnegex 10398  ax-rrecex 10399  ax-cnre 10400  ax-pre-lttri 10401  ax-pre-lttrn 10402  ax-pre-ltadd 10403  ax-pre-mulgt0 10404  ax-pre-sup 10405
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-pss 3841  df-nul 4174  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4707  df-int 4744  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-tr 5025  df-id 5305  df-eprel 5310  df-po 5319  df-so 5320  df-fr 5359  df-se 5360  df-we 5361  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-pred 5980  df-ord 6026  df-on 6027  df-lim 6028  df-suc 6029  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-isom 6191  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-om 7391  df-1st 7494  df-2nd 7495  df-wrecs 7743  df-recs 7805  df-rdg 7843  df-1o 7897  df-oadd 7901  df-er 8081  df-pm 8201  df-en 8299  df-dom 8300  df-sdom 8301  df-fin 8302  df-sup 8693  df-inf 8694  df-oi 8761  df-card 9154  df-pnf 10468  df-mnf 10469  df-xr 10470  df-ltxr 10471  df-le 10472  df-sub 10664  df-neg 10665  df-div 11091  df-nn 11432  df-2 11496  df-3 11497  df-n0 11701  df-z 11787  df-uz 12052  df-rp 12198  df-fz 12702  df-fzo 12843  df-fl 12970  df-seq 13178  df-exp 13238  df-hash 13499  df-shft 14277  df-cj 14309  df-re 14310  df-im 14311  df-sqrt 14445  df-abs 14446  df-clim 14696  df-rlim 14697  df-sum 14894
This theorem is referenced by:  aaliou3lem3  24626
  Copyright terms: Public domain W3C validator