Theorem efclt 7290

Description: Closure law for the exponential function.

Assertion

Ref	Expression
efclt	|- (A e. CC -> (exp` A) e. CC)

Proof of Theorem efclt

Step	Hyp	Ref	Expression
1		efvalt 7286	. 2 |- (A e. CC -> (exp` A) = sum_k e. NN0 ((A^k) / (!` k)))
2		nn0uz 6388	. . . . . . . . . 10 |- NN0 = (ZZ>` 0)
3	2	eqcomi 1478	. . . . . . . . 9 |- (ZZ>` 0) = NN0
4	3	eleq2i 1537	. . . . . . . 8 |- (j e. (ZZ>` 0) <-> j e. NN0)
5	4	anbi1i 481	. . . . . . 7 |- ((j e. (ZZ>` 0) /\ y = ((A^j) / (!` j))) <-> (j e. NN0 /\ y = ((A^j) / (!` j))))
6	5	opabbii 2668	. . . . . 6 |- {<.j, y>. | (j e. (ZZ>` 0) /\ y = ((A^j) / (!` j)))} = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}
7	6	efseq0ex 7289	. . . . 5 |- (A e. CC -> E.x( + seq0 {<.j, y>. | (j e. (ZZ>` 0) /\ y = ((A^j) / (!` j)))}) ~~> x)
8		addex 5304	. . . . . . . 8 |- + e. V
9		fvex 3729	. . . . . . . . 9 |- (ZZ>` 0) e. V
10	9	opabex2 3607	. . . . . . . 8 |- {<.j, y>. | (j e. (ZZ>` 0) /\ y = ((A^j) / (!` j)))} e. V
11	8, 10	seq0seqz 6492	. . . . . . 7 |- ( + seq0 {<.j, y>. | (j e. (ZZ>` 0) /\ y = ((A^j) / (!` j)))}) = (<.0, + >. seq {<.j, y>. | (j e. (ZZ>` 0) /\ y = ((A^j) / (!` j)))})
12	11	breq1i 2623	. . . . . 6 |- (( + seq0 {<.j, y>. | (j e. (ZZ>` 0) /\ y = ((A^j) / (!` j)))}) ~~> x <-> (<.0, + >. seq {<.j, y>. | (j e. (ZZ>` 0) /\ y = ((A^j) / (!` j)))}) ~~> x)
13	12	exbii 1050	. . . . 5 |- (E.x( + seq0 {<.j, y>. | (j e. (ZZ>` 0) /\ y = ((A^j) / (!` j)))}) ~~> x <-> E.x(<.0, + >. seq {<.j, y>. | (j e. (ZZ>` 0) /\ y = ((A^j) / (!` j)))}) ~~> x)
14	7, 13	sylib 198	. . . 4 |- (A e. CC -> E.x(<.0, + >. seq {<.j, y>. | (j e. (ZZ>` 0) /\ y = ((A^j) / (!` j)))}) ~~> x)
15		0z 6107	. . . . 5 |- 0 e. ZZ
16	10	isumclt 7180	. . . . 5 |- ((0 e. ZZ /\ E.x(<.0, + >. seq {<.j, y>. | (j e. (ZZ>` 0) /\ y = ((A^j) / (!` j)))}) ~~> x) -> sum_k e. (ZZ>` 0)({<.j, y>. | (j e. (ZZ>` 0) /\ y = ((A^j) / (!` j)))}` k) e. CC)
17	15, 16	mpan 694	. . . 4 |- (E.x(<.0, + >. seq {<.j, y>. | (j e. (ZZ>` 0) /\ y = ((A^j) / (!` j)))}) ~~> x -> sum_k e. (ZZ>` 0)({<.j, y>. | (j e. (ZZ>` 0) /\ y = ((A^j) / (!` j)))}` k) e. CC)
18	14, 17	syl 10	. . 3 |- (A e. CC -> sum_k e. (ZZ>` 0)({<.j, y>. | (j e. (ZZ>` 0) /\ y = ((A^j) / (!` j)))}` k) e. CC)
19	2	sumeq1i 6955	. . . 4 |- sum_k e. NN0 ((A^k) / (!` k)) = sum_k e. (ZZ>` 0)((A^k) / (!` k))
20		opreq2 3966	. . . . . . 7 |- (j = k -> (A^j) = (A^k))
21		fveq2 3721	. . . . . . 7 |- (j = k -> (!` j) = (!` k))
22	20, 21	opreq12d 3975	. . . . . 6 |- (j = k -> ((A^j) / (!` j)) = ((A^k) / (!` k)))
23		eqid 1475	. . . . . 6 |- {<.j, y>. | (j e. (ZZ>` 0) /\ y = ((A^j) / (!` j)))} = {<.j, y>. | (j e. (ZZ>` 0) /\ y = ((A^j) / (!` j)))}
24		oprex 3980	. . . . . 6 |- ((A^k) / (!` k)) e. V
25	22, 23, 24	fvopab4 3777	. . . . 5 |- (k e. (ZZ>` 0) -> ({<.j, y>. | (j e. (ZZ>` 0) /\ y = ((A^j) / (!` j)))}` k) = ((A^k) / (!` k)))
26	25	sumeq2i 6956	. . . 4 |- sum_k e. (ZZ>` 0)({<.j, y>. | (j e. (ZZ>` 0) /\ y = ((A^j) / (!` j)))}` k) = sum_k e. (ZZ>` 0)((A^k) / (!` k))
27	19, 26	eqtr4 1497	. . 3 |- sum_k e. NN0 ((A^k) / (!` k)) = sum_k e. (ZZ>` 0)({<.j, y>. | (j e. (ZZ>` 0) /\ y = ((A^j) / (!` j)))}` k)
28	18, 27	syl5eqel 1551	. 2 |- (A e. CC -> sum_k e. NN0 ((A^k) / (!` k)) e. CC)
29	1, 28	eqeltrd 1547	1 |- (A e. CC -> (exp` A) e. CC)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 955   e. wcel 957  E.wex 979  <.cop 2409   class class class wbr 2616  {copab 2663  ` cfv 3179  (class class class)co 3960  CCcc 5219  0cc0 5221   + caddc 5224   / cdiv 5281  NN0cn0 5284  ZZcz 5285  ZZ>cuz 6367   seq cseqz 6481   seq0 cseq0 6482  ^cexp 6518  !cfa 6897   ~~> cli 6942  sum_csu 6947  expce 7271

This theorem is referenced by:  eff 7291  efaddlem27 7342  efne0t 7347  eff2 7348  efsubt 7349  efexpt 7350  ef4p 7376  efcnlem2 7396  efcn 7399  reeff1o 7404  sinclt 7409  cosclt 7410  resinvalt 7411  recosvalt 7412  resinclt 7416  recosclt 7417  sinnegt 7420  cosnegt 7421  efivalt 7425  abseft 7461  efghgrpilem 8698  efif 8700  efif1lem4 8712  efielcircOLD 8719  efielcirc 8723  eff1i 8728  efper 8731  pilog 8752

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2690  ax-sep 2700  ax-nul 2707  ax-pow 2739  ax-pr 2776  ax-un 2863  ax-inf2 4612

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 980  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1586  df-nel 1587  df-ral 1648  df-rex 1649  df-reu 1650  df-rab 1651  df-v 1810  df-sbc 1940  df-csb 2000  df-dif 2047  df-un 2048  df-in 2049  df-ss 2051  df-pss 2053  df-nul 2279  df-if 2360  df-pw 2400  df-sn 2410  df-pr 2411  df-tp 2413  df-op 2414  df-uni 2501  df-int 2531  df-iun 2565  df-br 2617  df-opab 2664  df-tr 2678  df-eprel 2829  df-id 2832  df-po 2837  df-so 2847  df-fr 2914  df-we 2931  df-ord 2948  df-on 2949  df-lim 2950  df-suc 2951  df-om 3129  df-xp 3181  df-rel 3182  df-cnv 3183  df-co 3184  df-dm 3185  df-rn 3186  df-res 3187  df-ima 3188  df-fun 3189  df-fn 3190  df-f 3191  df-f1 3192  df-fo 3193  df-f1o 3194  df-fv 3195  df-rdg 3929  df-opr 3962  df-oprab 3963  df-1st 4076  df-2nd 4077  df-1o 4130  df-oadd 4132  df-omul 4133  df-er 4258  df-ec 4260  df-qs 4263  df-en 4364  df-dom 4365  df-sdom 4366  df-sup 4561  df-ni 4987  df-pli 4988  df-mi 4989  df-lti 4990  df-plpq 5022  df-mpq 5023  df-enq 5024  df-nq 5025  df-plq 5026  df-mq 5027  df-rq 5028  df-ltq 5029  df-1q 5030  df-np 5073  df-1p 5074  df-plp 5075  df-mp 5076  df-ltp 5077  df-plpr 5151  df-mpr 5152  df-enr 5153  df-nr 5154  df-plr 5155  df-mr 5156  df-ltr 5157  df-0r 5158  df-1r 5159  df-m1r 5160  df-c 5227  df-0 5228  df-1 5229  df-i 5230  df-r 5231  df-plus 5232  df-mul 5233  df-lt 5234  df-sub 5343  df-neg 5345  df-pnf 5474  df-mnf 5475  df-xr 5476  df-ltxr 5477  df-le 5478  df-div 5686  df-n 5887  df-2 5931  df-n0 6061  df-z 6097  df-fl 6186  df-seq1 6263  df-shft 6296  df-uz 6368  df-fz 6418  df-seqz 6483  df-seq0 6484  df-exp 6519  df-sqr 6621  df-re 6703  df-im 6704  df-cj 6705  df-abs 6706  df-fac 6898  df-clim 6943  df-sum 6948  df-ef 7276

Copyright terms: Public domain