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

Theorem efsep 11599
Description: Separate out the next term of the power series expansion of the exponential function. The last hypothesis allows the separated terms to be rearranged as desired. (Contributed by Paul Chapman, 23-Nov-2007.) (Revised by Mario Carneiro, 29-Apr-2014.)
Hypotheses
Ref Expression
efsep.1 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) / (!‘𝑛)))
efsep.2 𝑁 = (𝑀 + 1)
efsep.3 𝑀 ∈ ℕ0
efsep.4 (𝜑𝐴 ∈ ℂ)
efsep.5 (𝜑𝐵 ∈ ℂ)
efsep.6 (𝜑 → (exp‘𝐴) = (𝐵 + Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘)))
efsep.7 (𝜑 → (𝐵 + ((𝐴𝑀) / (!‘𝑀))) = 𝐷)
Assertion
Ref Expression
efsep (𝜑 → (exp‘𝐴) = (𝐷 + Σ𝑘 ∈ (ℤ𝑁)(𝐹𝑘)))
Distinct variable groups:   𝑘,𝑛,𝐴   𝑘,𝐹   𝑘,𝑀,𝑛   𝑘,𝑁,𝑛   𝜑,𝑘
Allowed substitution hints:   𝜑(𝑛)   𝐵(𝑘,𝑛)   𝐷(𝑘,𝑛)   𝐹(𝑛)

Proof of Theorem efsep
StepHypRef Expression
1 efsep.6 . 2 (𝜑 → (exp‘𝐴) = (𝐵 + Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘)))
2 eqid 2157 . . . . . 6 (ℤ𝑀) = (ℤ𝑀)
3 efsep.3 . . . . . . . 8 𝑀 ∈ ℕ0
43nn0zi 9194 . . . . . . 7 𝑀 ∈ ℤ
54a1i 9 . . . . . 6 (𝜑𝑀 ∈ ℤ)
6 eqidd 2158 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) = (𝐹𝑘))
7 eluznn0 9515 . . . . . . . 8 ((𝑀 ∈ ℕ0𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℕ0)
83, 7mpan 421 . . . . . . 7 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ ℕ0)
9 efsep.4 . . . . . . . . 9 (𝜑𝐴 ∈ ℂ)
10 efsep.1 . . . . . . . . . 10 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) / (!‘𝑛)))
1110eftvalcn 11565 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐹𝑘) = ((𝐴𝑘) / (!‘𝑘)))
129, 11sylan 281 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) = ((𝐴𝑘) / (!‘𝑘)))
13 eftcl 11562 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝐴𝑘) / (!‘𝑘)) ∈ ℂ)
149, 13sylan 281 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → ((𝐴𝑘) / (!‘𝑘)) ∈ ℂ)
1512, 14eqeltrd 2234 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) ∈ ℂ)
168, 15sylan2 284 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ ℂ)
1710eftlcvg 11595 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → seq𝑀( + , 𝐹) ∈ dom ⇝ )
189, 3, 17sylancl 410 . . . . . 6 (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
192, 5, 6, 16, 18isum1p 11400 . . . . 5 (𝜑 → Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘) = ((𝐹𝑀) + Σ𝑘 ∈ (ℤ‘(𝑀 + 1))(𝐹𝑘)))
2010eftvalcn 11565 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝐹𝑀) = ((𝐴𝑀) / (!‘𝑀)))
219, 3, 20sylancl 410 . . . . . 6 (𝜑 → (𝐹𝑀) = ((𝐴𝑀) / (!‘𝑀)))
22 efsep.2 . . . . . . . . . 10 𝑁 = (𝑀 + 1)
2322eqcomi 2161 . . . . . . . . 9 (𝑀 + 1) = 𝑁
2423fveq2i 5473 . . . . . . . 8 (ℤ‘(𝑀 + 1)) = (ℤ𝑁)
2524sumeq1i 11271 . . . . . . 7 Σ𝑘 ∈ (ℤ‘(𝑀 + 1))(𝐹𝑘) = Σ𝑘 ∈ (ℤ𝑁)(𝐹𝑘)
2625a1i 9 . . . . . 6 (𝜑 → Σ𝑘 ∈ (ℤ‘(𝑀 + 1))(𝐹𝑘) = Σ𝑘 ∈ (ℤ𝑁)(𝐹𝑘))
2721, 26oveq12d 5844 . . . . 5 (𝜑 → ((𝐹𝑀) + Σ𝑘 ∈ (ℤ‘(𝑀 + 1))(𝐹𝑘)) = (((𝐴𝑀) / (!‘𝑀)) + Σ𝑘 ∈ (ℤ𝑁)(𝐹𝑘)))
2819, 27eqtrd 2190 . . . 4 (𝜑 → Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘) = (((𝐴𝑀) / (!‘𝑀)) + Σ𝑘 ∈ (ℤ𝑁)(𝐹𝑘)))
2928oveq2d 5842 . . 3 (𝜑 → (𝐵 + Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘)) = (𝐵 + (((𝐴𝑀) / (!‘𝑀)) + Σ𝑘 ∈ (ℤ𝑁)(𝐹𝑘))))
30 efsep.5 . . . 4 (𝜑𝐵 ∈ ℂ)
31 eftcl 11562 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → ((𝐴𝑀) / (!‘𝑀)) ∈ ℂ)
329, 3, 31sylancl 410 . . . 4 (𝜑 → ((𝐴𝑀) / (!‘𝑀)) ∈ ℂ)
33 peano2nn0 9135 . . . . . . 7 (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℕ0)
343, 33ax-mp 5 . . . . . 6 (𝑀 + 1) ∈ ℕ0
3522, 34eqeltri 2230 . . . . 5 𝑁 ∈ ℕ0
3610eftlcl 11596 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → Σ𝑘 ∈ (ℤ𝑁)(𝐹𝑘) ∈ ℂ)
379, 35, 36sylancl 410 . . . 4 (𝜑 → Σ𝑘 ∈ (ℤ𝑁)(𝐹𝑘) ∈ ℂ)
3830, 32, 37addassd 7902 . . 3 (𝜑 → ((𝐵 + ((𝐴𝑀) / (!‘𝑀))) + Σ𝑘 ∈ (ℤ𝑁)(𝐹𝑘)) = (𝐵 + (((𝐴𝑀) / (!‘𝑀)) + Σ𝑘 ∈ (ℤ𝑁)(𝐹𝑘))))
3929, 38eqtr4d 2193 . 2 (𝜑 → (𝐵 + Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘)) = ((𝐵 + ((𝐴𝑀) / (!‘𝑀))) + Σ𝑘 ∈ (ℤ𝑁)(𝐹𝑘)))
40 efsep.7 . . 3 (𝜑 → (𝐵 + ((𝐴𝑀) / (!‘𝑀))) = 𝐷)
4140oveq1d 5841 . 2 (𝜑 → ((𝐵 + ((𝐴𝑀) / (!‘𝑀))) + Σ𝑘 ∈ (ℤ𝑁)(𝐹𝑘)) = (𝐷 + Σ𝑘 ∈ (ℤ𝑁)(𝐹𝑘)))
421, 39, 413eqtrd 2194 1 (𝜑 → (exp‘𝐴) = (𝐷 + Σ𝑘 ∈ (ℤ𝑁)(𝐹𝑘)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103   = wceq 1335  wcel 2128  cmpt 4027  dom cdm 4588  cfv 5172  (class class class)co 5826  cc 7732  1c1 7735   + caddc 7737   / cdiv 8549  0cn0 9095  cz 9172  cuz 9444  seqcseq 10353  cexp 10427  !cfa 10610  cli 11186  Σcsu 11261  expce 11550
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 4081  ax-sep 4084  ax-nul 4092  ax-pow 4137  ax-pr 4171  ax-un 4395  ax-setind 4498  ax-iinf 4549  ax-cnex 7825  ax-resscn 7826  ax-1cn 7827  ax-1re 7828  ax-icn 7829  ax-addcl 7830  ax-addrcl 7831  ax-mulcl 7832  ax-mulrcl 7833  ax-addcom 7834  ax-mulcom 7835  ax-addass 7836  ax-mulass 7837  ax-distr 7838  ax-i2m1 7839  ax-0lt1 7840  ax-1rid 7841  ax-0id 7842  ax-rnegex 7843  ax-precex 7844  ax-cnre 7845  ax-pre-ltirr 7846  ax-pre-ltwlin 7847  ax-pre-lttrn 7848  ax-pre-apti 7849  ax-pre-ltadd 7850  ax-pre-mulgt0 7851  ax-pre-mulext 7852  ax-arch 7853  ax-caucvg 7854
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 3396  df-if 3507  df-pw 3546  df-sn 3567  df-pr 3568  df-op 3570  df-uni 3775  df-int 3810  df-iun 3853  df-br 3968  df-opab 4028  df-mpt 4029  df-tr 4065  df-id 4255  df-po 4258  df-iso 4259  df-iord 4328  df-on 4330  df-ilim 4331  df-suc 4333  df-iom 4552  df-xp 4594  df-rel 4595  df-cnv 4596  df-co 4597  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-iota 5137  df-fun 5174  df-fn 5175  df-f 5176  df-f1 5177  df-fo 5178  df-f1o 5179  df-fv 5180  df-isom 5181  df-riota 5782  df-ov 5829  df-oprab 5830  df-mpo 5831  df-1st 6090  df-2nd 6091  df-recs 6254  df-irdg 6319  df-frec 6340  df-1o 6365  df-oadd 6369  df-er 6482  df-en 6688  df-dom 6689  df-fin 6690  df-pnf 7916  df-mnf 7917  df-xr 7918  df-ltxr 7919  df-le 7920  df-sub 8052  df-neg 8053  df-reap 8454  df-ap 8461  df-div 8550  df-inn 8839  df-2 8897  df-3 8898  df-4 8899  df-n0 9096  df-z 9173  df-uz 9445  df-q 9535  df-rp 9567  df-ico 9804  df-fz 9919  df-fzo 10051  df-seqfrec 10354  df-exp 10428  df-fac 10611  df-ihash 10661  df-cj 10753  df-re 10754  df-im 10755  df-rsqrt 10909  df-abs 10910  df-clim 11187  df-sumdc 11262
This theorem is referenced by:  ef4p  11602  dveflem  13157
  Copyright terms: Public domain W3C validator