Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  geolim GIF version

Theorem geolim 11390
 Description: The partial sums in the infinite series 1 + 𝐴↑1 + 𝐴↑2... converge to (1 / (1 − 𝐴)). (Contributed by NM, 15-May-2006.)
Hypotheses
Ref Expression
geolim.1 (𝜑𝐴 ∈ ℂ)
geolim.2 (𝜑 → (abs‘𝐴) < 1)
geolim.3 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) = (𝐴𝑘))
Assertion
Ref Expression
geolim (𝜑 → seq0( + , 𝐹) ⇝ (1 / (1 − 𝐴)))
Distinct variable groups:   𝐴,𝑘   𝑘,𝐹   𝜑,𝑘

Proof of Theorem geolim
Dummy variables 𝑗 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nn0uz 9456 . . 3 0 = (ℤ‘0)
2 0zd 9162 . . 3 (𝜑 → 0 ∈ ℤ)
3 geolim.1 . . . . . 6 (𝜑𝐴 ∈ ℂ)
4 geolim.2 . . . . . 6 (𝜑 → (abs‘𝐴) < 1)
53, 4expcnv 11383 . . . . 5 (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐴𝑛)) ⇝ 0)
6 ax-1cn 7808 . . . . . . 7 1 ∈ ℂ
7 subcl 8057 . . . . . . 7 ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 − 𝐴) ∈ ℂ)
86, 3, 7sylancr 411 . . . . . 6 (𝜑 → (1 − 𝐴) ∈ ℂ)
9 1cnd 7877 . . . . . . 7 (𝜑 → 1 ∈ ℂ)
10 1red 7876 . . . . . . . . 9 (𝜑 → 1 ∈ ℝ)
113, 10, 4absltap 11388 . . . . . . . 8 (𝜑𝐴 # 1)
12 apsym 8464 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 # 1 ↔ 1 # 𝐴))
133, 6, 12sylancl 410 . . . . . . . 8 (𝜑 → (𝐴 # 1 ↔ 1 # 𝐴))
1411, 13mpbid 146 . . . . . . 7 (𝜑 → 1 # 𝐴)
159, 3, 14subap0d 8502 . . . . . 6 (𝜑 → (1 − 𝐴) # 0)
163, 8, 15divclapd 8646 . . . . 5 (𝜑 → (𝐴 / (1 − 𝐴)) ∈ ℂ)
17 nn0ex 9079 . . . . . . 7 0 ∈ V
1817mptex 5690 . . . . . 6 (𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴))) ∈ V
1918a1i 9 . . . . 5 (𝜑 → (𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴))) ∈ V)
20 simpr 109 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → 𝑗 ∈ ℕ0)
213adantr 274 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)
2221, 20expcld 10533 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → (𝐴𝑗) ∈ ℂ)
23 oveq2 5826 . . . . . . . 8 (𝑛 = 𝑗 → (𝐴𝑛) = (𝐴𝑗))
24 eqid 2157 . . . . . . . 8 (𝑛 ∈ ℕ0 ↦ (𝐴𝑛)) = (𝑛 ∈ ℕ0 ↦ (𝐴𝑛))
2523, 24fvmptg 5541 . . . . . . 7 ((𝑗 ∈ ℕ0 ∧ (𝐴𝑗) ∈ ℂ) → ((𝑛 ∈ ℕ0 ↦ (𝐴𝑛))‘𝑗) = (𝐴𝑗))
2620, 22, 25syl2anc 409 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (𝐴𝑛))‘𝑗) = (𝐴𝑗))
27 expcl 10419 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (𝐴𝑗) ∈ ℂ)
283, 27sylan 281 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (𝐴𝑗) ∈ ℂ)
2926, 28eqeltrd 2234 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (𝐴𝑛))‘𝑗) ∈ ℂ)
30 expp1 10408 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (𝐴↑(𝑗 + 1)) = ((𝐴𝑗) · 𝐴))
313, 30sylan 281 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → (𝐴↑(𝑗 + 1)) = ((𝐴𝑗) · 𝐴))
3228, 21mulcomd 7882 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → ((𝐴𝑗) · 𝐴) = (𝐴 · (𝐴𝑗)))
3331, 32eqtrd 2190 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (𝐴↑(𝑗 + 1)) = (𝐴 · (𝐴𝑗)))
3433oveq1d 5833 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((𝐴↑(𝑗 + 1)) / (1 − 𝐴)) = ((𝐴 · (𝐴𝑗)) / (1 − 𝐴)))
358adantr 274 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (1 − 𝐴) ∈ ℂ)
3615adantr 274 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (1 − 𝐴) # 0)
3721, 28, 35, 36div23apd 8684 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((𝐴 · (𝐴𝑗)) / (1 − 𝐴)) = ((𝐴 / (1 − 𝐴)) · (𝐴𝑗)))
3834, 37eqtrd 2190 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → ((𝐴↑(𝑗 + 1)) / (1 − 𝐴)) = ((𝐴 / (1 − 𝐴)) · (𝐴𝑗)))
39 peano2nn0 9113 . . . . . . . . . 10 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ0)
4039adantl 275 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → (𝑗 + 1) ∈ ℕ0)
4121, 40expcld 10533 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (𝐴↑(𝑗 + 1)) ∈ ℂ)
4241, 35, 36divclapd 8646 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((𝐴↑(𝑗 + 1)) / (1 − 𝐴)) ∈ ℂ)
43 oveq1 5825 . . . . . . . . . 10 (𝑛 = 𝑗 → (𝑛 + 1) = (𝑗 + 1))
4443oveq2d 5834 . . . . . . . . 9 (𝑛 = 𝑗 → (𝐴↑(𝑛 + 1)) = (𝐴↑(𝑗 + 1)))
4544oveq1d 5833 . . . . . . . 8 (𝑛 = 𝑗 → ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)) = ((𝐴↑(𝑗 + 1)) / (1 − 𝐴)))
46 eqid 2157 . . . . . . . 8 (𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴))) = (𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))
4745, 46fvmptg 5541 . . . . . . 7 ((𝑗 ∈ ℕ0 ∧ ((𝐴↑(𝑗 + 1)) / (1 − 𝐴)) ∈ ℂ) → ((𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗) = ((𝐴↑(𝑗 + 1)) / (1 − 𝐴)))
4820, 42, 47syl2anc 409 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗) = ((𝐴↑(𝑗 + 1)) / (1 − 𝐴)))
4926oveq2d 5834 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → ((𝐴 / (1 − 𝐴)) · ((𝑛 ∈ ℕ0 ↦ (𝐴𝑛))‘𝑗)) = ((𝐴 / (1 − 𝐴)) · (𝐴𝑗)))
5038, 48, 493eqtr4d 2200 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗) = ((𝐴 / (1 − 𝐴)) · ((𝑛 ∈ ℕ0 ↦ (𝐴𝑛))‘𝑗)))
511, 2, 5, 16, 19, 29, 50climmulc2 11210 . . . 4 (𝜑 → (𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴))) ⇝ ((𝐴 / (1 − 𝐴)) · 0))
5216mul01d 8251 . . . 4 (𝜑 → ((𝐴 / (1 − 𝐴)) · 0) = 0)
5351, 52breqtrd 3990 . . 3 (𝜑 → (𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴))) ⇝ 0)
548, 15recclapd 8637 . . 3 (𝜑 → (1 / (1 − 𝐴)) ∈ ℂ)
55 seqex 10328 . . . 4 seq0( + , 𝐹) ∈ V
5655a1i 9 . . 3 (𝜑 → seq0( + , 𝐹) ∈ V)
57 expcl 10419 . . . . . 6 ((𝐴 ∈ ℂ ∧ (𝑗 + 1) ∈ ℕ0) → (𝐴↑(𝑗 + 1)) ∈ ℂ)
583, 39, 57syl2an 287 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → (𝐴↑(𝑗 + 1)) ∈ ℂ)
5958, 35, 36divclapd 8646 . . . 4 ((𝜑𝑗 ∈ ℕ0) → ((𝐴↑(𝑗 + 1)) / (1 − 𝐴)) ∈ ℂ)
6048, 59eqeltrd 2234 . . 3 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗) ∈ ℂ)
61 nn0cn 9083 . . . . . . . 8 (𝑗 ∈ ℕ0𝑗 ∈ ℂ)
6261adantl 275 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → 𝑗 ∈ ℂ)
63 pncan 8064 . . . . . . 7 ((𝑗 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑗 + 1) − 1) = 𝑗)
6462, 6, 63sylancl 410 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → ((𝑗 + 1) − 1) = 𝑗)
6564oveq2d 5834 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → (0...((𝑗 + 1) − 1)) = (0...𝑗))
6665sumeq1d 11245 . . . 4 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ (0...((𝑗 + 1) − 1))(𝐴𝑘) = Σ𝑘 ∈ (0...𝑗)(𝐴𝑘))
67 1cnd 7877 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → 1 ∈ ℂ)
6867, 58, 35, 36divsubdirapd 8686 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → ((1 − (𝐴↑(𝑗 + 1))) / (1 − 𝐴)) = ((1 / (1 − 𝐴)) − ((𝐴↑(𝑗 + 1)) / (1 − 𝐴))))
6911adantr 274 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → 𝐴 # 1)
7021, 69, 40geoserap 11386 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ (0...((𝑗 + 1) − 1))(𝐴𝑘) = ((1 − (𝐴↑(𝑗 + 1))) / (1 − 𝐴)))
7148oveq2d 5834 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → ((1 / (1 − 𝐴)) − ((𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗)) = ((1 / (1 − 𝐴)) − ((𝐴↑(𝑗 + 1)) / (1 − 𝐴))))
7268, 70, 713eqtr4d 2200 . . . 4 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ (0...((𝑗 + 1) − 1))(𝐴𝑘) = ((1 / (1 − 𝐴)) − ((𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗)))
73 simpll 519 . . . . . 6 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (ℤ‘0)) → 𝜑)
74 elnn0uz 9459 . . . . . . . 8 (𝑘 ∈ ℕ0𝑘 ∈ (ℤ‘0))
7574biimpri 132 . . . . . . 7 (𝑘 ∈ (ℤ‘0) → 𝑘 ∈ ℕ0)
7675adantl 275 . . . . . 6 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (ℤ‘0)) → 𝑘 ∈ ℕ0)
77 geolim.3 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) = (𝐴𝑘))
7873, 76, 77syl2anc 409 . . . . 5 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (ℤ‘0)) → (𝐹𝑘) = (𝐴𝑘))
7920, 1eleqtrdi 2250 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → 𝑗 ∈ (ℤ‘0))
8021adantr 274 . . . . . 6 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (ℤ‘0)) → 𝐴 ∈ ℂ)
8180, 76expcld 10533 . . . . 5 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (ℤ‘0)) → (𝐴𝑘) ∈ ℂ)
8278, 79, 81fsum3ser 11276 . . . 4 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ (0...𝑗)(𝐴𝑘) = (seq0( + , 𝐹)‘𝑗))
8366, 72, 823eqtr3rd 2199 . . 3 ((𝜑𝑗 ∈ ℕ0) → (seq0( + , 𝐹)‘𝑗) = ((1 / (1 − 𝐴)) − ((𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗)))
841, 2, 53, 54, 56, 60, 83climsubc2 11212 . 2 (𝜑 → seq0( + , 𝐹) ⇝ ((1 / (1 − 𝐴)) − 0))
8554subid1d 8158 . 2 (𝜑 → ((1 / (1 − 𝐴)) − 0) = (1 / (1 − 𝐴)))
8684, 85breqtrd 3990 1 (𝜑 → seq0( + , 𝐹) ⇝ (1 / (1 − 𝐴)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1335   ∈ wcel 2128  Vcvv 2712   class class class wbr 3965   ↦ cmpt 4025  ‘cfv 5167  (class class class)co 5818  ℂcc 7713  0cc0 7715  1c1 7716   + caddc 7718   · cmul 7720   < clt 7895   − cmin 8029   # cap 8439   / cdiv 8528  ℕ0cn0 9073  ℤ≥cuz 9422  ...cfz 9894  seqcseq 10326  ↑cexp 10400  abscabs 10879   ⇝ cli 11157  Σcsu 11232 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4079  ax-sep 4082  ax-nul 4090  ax-pow 4134  ax-pr 4168  ax-un 4392  ax-setind 4494  ax-iinf 4545  ax-cnex 7806  ax-resscn 7807  ax-1cn 7808  ax-1re 7809  ax-icn 7810  ax-addcl 7811  ax-addrcl 7812  ax-mulcl 7813  ax-mulrcl 7814  ax-addcom 7815  ax-mulcom 7816  ax-addass 7817  ax-mulass 7818  ax-distr 7819  ax-i2m1 7820  ax-0lt1 7821  ax-1rid 7822  ax-0id 7823  ax-rnegex 7824  ax-precex 7825  ax-cnre 7826  ax-pre-ltirr 7827  ax-pre-ltwlin 7828  ax-pre-lttrn 7829  ax-pre-apti 7830  ax-pre-ltadd 7831  ax-pre-mulgt0 7832  ax-pre-mulext 7833  ax-arch 7834  ax-caucvg 7835 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-reu 2442  df-rmo 2443  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-if 3506  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-iun 3851  df-br 3966  df-opab 4026  df-mpt 4027  df-tr 4063  df-id 4252  df-po 4255  df-iso 4256  df-iord 4325  df-on 4327  df-ilim 4328  df-suc 4330  df-iom 4548  df-xp 4589  df-rel 4590  df-cnv 4591  df-co 4592  df-dm 4593  df-rn 4594  df-res 4595  df-ima 4596  df-iota 5132  df-fun 5169  df-fn 5170  df-f 5171  df-f1 5172  df-fo 5173  df-f1o 5174  df-fv 5175  df-isom 5176  df-riota 5774  df-ov 5821  df-oprab 5822  df-mpo 5823  df-1st 6082  df-2nd 6083  df-recs 6246  df-irdg 6311  df-frec 6332  df-1o 6357  df-oadd 6361  df-er 6473  df-en 6679  df-dom 6680  df-fin 6681  df-pnf 7897  df-mnf 7898  df-xr 7899  df-ltxr 7900  df-le 7901  df-sub 8031  df-neg 8032  df-reap 8433  df-ap 8440  df-div 8529  df-inn 8817  df-2 8875  df-3 8876  df-4 8877  df-n0 9074  df-z 9151  df-uz 9423  df-q 9511  df-rp 9543  df-fz 9895  df-fzo 10024  df-seqfrec 10327  df-exp 10401  df-ihash 10632  df-cj 10724  df-re 10725  df-im 10726  df-rsqrt 10880  df-abs 10881  df-clim 11158  df-sumdc 11233 This theorem is referenced by:  geolim2  11391  georeclim  11392  geoisum  11396  eflegeo  11580
 Copyright terms: Public domain W3C validator