# Metamath Proof Explorer

## Theorem efcllem

Description: Lemma for efcl . The series that defines the exponential function converges, in the case where its argument is nonzero. The ratio test cvgrat is used to show convergence. (Contributed by NM, 26-Apr-2005) (Proof shortened by Mario Carneiro, 28-Apr-2014) (Proof shortened by AV, 9-Jul-2022)

Ref Expression
Hypothesis eftval.1 ${⊢}{F}=\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)$
Assertion efcllem ${⊢}{A}\in ℂ\to seq0\left(+,{F}\right)\in \mathrm{dom}⇝$

### Proof

Step Hyp Ref Expression
1 eftval.1 ${⊢}{F}=\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)$
2 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
3 eqid ${⊢}{ℤ}_{\ge ⌊2\left|{A}\right|⌋}={ℤ}_{\ge ⌊2\left|{A}\right|⌋}$
4 halfre ${⊢}\frac{1}{2}\in ℝ$
5 4 a1i ${⊢}{A}\in ℂ\to \frac{1}{2}\in ℝ$
6 halflt1 ${⊢}\frac{1}{2}<1$
7 6 a1i ${⊢}{A}\in ℂ\to \frac{1}{2}<1$
8 2re ${⊢}2\in ℝ$
9 abscl ${⊢}{A}\in ℂ\to \left|{A}\right|\in ℝ$
10 remulcl ${⊢}\left(2\in ℝ\wedge \left|{A}\right|\in ℝ\right)\to 2\left|{A}\right|\in ℝ$
11 8 9 10 sylancr ${⊢}{A}\in ℂ\to 2\left|{A}\right|\in ℝ$
12 8 a1i ${⊢}{A}\in ℂ\to 2\in ℝ$
13 0le2 ${⊢}0\le 2$
14 13 a1i ${⊢}{A}\in ℂ\to 0\le 2$
15 absge0 ${⊢}{A}\in ℂ\to 0\le \left|{A}\right|$
16 12 9 14 15 mulge0d ${⊢}{A}\in ℂ\to 0\le 2\left|{A}\right|$
17 flge0nn0 ${⊢}\left(2\left|{A}\right|\in ℝ\wedge 0\le 2\left|{A}\right|\right)\to ⌊2\left|{A}\right|⌋\in {ℕ}_{0}$
18 11 16 17 syl2anc ${⊢}{A}\in ℂ\to ⌊2\left|{A}\right|⌋\in {ℕ}_{0}$
19 1 eftval ${⊢}{k}\in {ℕ}_{0}\to {F}\left({k}\right)=\frac{{{A}}^{{k}}}{{k}!}$
20 19 adantl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {F}\left({k}\right)=\frac{{{A}}^{{k}}}{{k}!}$
21 eftcl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to \frac{{{A}}^{{k}}}{{k}!}\in ℂ$
22 20 21 eqeltrd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {F}\left({k}\right)\in ℂ$
23 9 adantr ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left|{A}\right|\in ℝ$
24 eluznn0 ${⊢}\left(⌊2\left|{A}\right|⌋\in {ℕ}_{0}\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {k}\in {ℕ}_{0}$
25 18 24 sylan ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {k}\in {ℕ}_{0}$
26 nn0p1nn ${⊢}{k}\in {ℕ}_{0}\to {k}+1\in ℕ$
27 25 26 syl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {k}+1\in ℕ$
28 23 27 nndivred ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \frac{\left|{A}\right|}{{k}+1}\in ℝ$
29 4 a1i ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \frac{1}{2}\in ℝ$
30 23 25 reexpcld ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {\left|{A}\right|}^{{k}}\in ℝ$
31 25 faccld ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {k}!\in ℕ$
32 30 31 nndivred ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \frac{{\left|{A}\right|}^{{k}}}{{k}!}\in ℝ$
33 expcl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {{A}}^{{k}}\in ℂ$
34 25 33 syldan ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {{A}}^{{k}}\in ℂ$
35 34 absge0d ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to 0\le \left|{{A}}^{{k}}\right|$
36 absexp ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to \left|{{A}}^{{k}}\right|={\left|{A}\right|}^{{k}}$
37 25 36 syldan ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left|{{A}}^{{k}}\right|={\left|{A}\right|}^{{k}}$
38 35 37 breqtrd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to 0\le {\left|{A}\right|}^{{k}}$
39 31 nnred ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {k}!\in ℝ$
40 31 nngt0d ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to 0<{k}!$
41 divge0 ${⊢}\left(\left({\left|{A}\right|}^{{k}}\in ℝ\wedge 0\le {\left|{A}\right|}^{{k}}\right)\wedge \left({k}!\in ℝ\wedge 0<{k}!\right)\right)\to 0\le \frac{{\left|{A}\right|}^{{k}}}{{k}!}$
42 30 38 39 40 41 syl22anc ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to 0\le \frac{{\left|{A}\right|}^{{k}}}{{k}!}$
43 11 adantr ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to 2\left|{A}\right|\in ℝ$
44 peano2nn0 ${⊢}⌊2\left|{A}\right|⌋\in {ℕ}_{0}\to ⌊2\left|{A}\right|⌋+1\in {ℕ}_{0}$
45 18 44 syl ${⊢}{A}\in ℂ\to ⌊2\left|{A}\right|⌋+1\in {ℕ}_{0}$
46 45 nn0red ${⊢}{A}\in ℂ\to ⌊2\left|{A}\right|⌋+1\in ℝ$
47 46 adantr ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to ⌊2\left|{A}\right|⌋+1\in ℝ$
48 27 nnred ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {k}+1\in ℝ$
49 flltp1 ${⊢}2\left|{A}\right|\in ℝ\to 2\left|{A}\right|<⌊2\left|{A}\right|⌋+1$
50 43 49 syl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to 2\left|{A}\right|<⌊2\left|{A}\right|⌋+1$
51 eluzp1p1 ${⊢}{k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\to {k}+1\in {ℤ}_{\ge \left(⌊2\left|{A}\right|⌋+1\right)}$
52 51 adantl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {k}+1\in {ℤ}_{\ge \left(⌊2\left|{A}\right|⌋+1\right)}$
53 eluzle ${⊢}{k}+1\in {ℤ}_{\ge \left(⌊2\left|{A}\right|⌋+1\right)}\to ⌊2\left|{A}\right|⌋+1\le {k}+1$
54 52 53 syl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to ⌊2\left|{A}\right|⌋+1\le {k}+1$
55 43 47 48 50 54 ltletrd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to 2\left|{A}\right|<{k}+1$
56 23 recnd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left|{A}\right|\in ℂ$
57 2cn ${⊢}2\in ℂ$
58 mulcom ${⊢}\left(\left|{A}\right|\in ℂ\wedge 2\in ℂ\right)\to \left|{A}\right|\cdot 2=2\left|{A}\right|$
59 56 57 58 sylancl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left|{A}\right|\cdot 2=2\left|{A}\right|$
60 27 nncnd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {k}+1\in ℂ$
61 60 mulid2d ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to 1\left({k}+1\right)={k}+1$
62 55 59 61 3brtr4d ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left|{A}\right|\cdot 2<1\left({k}+1\right)$
63 2rp ${⊢}2\in {ℝ}^{+}$
64 63 a1i ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to 2\in {ℝ}^{+}$
65 1red ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to 1\in ℝ$
66 27 nnrpd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {k}+1\in {ℝ}^{+}$
67 23 64 65 66 lt2mul2divd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left(\left|{A}\right|\cdot 2<1\left({k}+1\right)↔\frac{\left|{A}\right|}{{k}+1}<\frac{1}{2}\right)$
68 62 67 mpbid ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \frac{\left|{A}\right|}{{k}+1}<\frac{1}{2}$
69 ltle ${⊢}\left(\frac{\left|{A}\right|}{{k}+1}\in ℝ\wedge \frac{1}{2}\in ℝ\right)\to \left(\frac{\left|{A}\right|}{{k}+1}<\frac{1}{2}\to \frac{\left|{A}\right|}{{k}+1}\le \frac{1}{2}\right)$
70 28 4 69 sylancl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left(\frac{\left|{A}\right|}{{k}+1}<\frac{1}{2}\to \frac{\left|{A}\right|}{{k}+1}\le \frac{1}{2}\right)$
71 68 70 mpd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \frac{\left|{A}\right|}{{k}+1}\le \frac{1}{2}$
72 28 29 32 42 71 lemul2ad ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left(\frac{{\left|{A}\right|}^{{k}}}{{k}!}\right)\left(\frac{\left|{A}\right|}{{k}+1}\right)\le \left(\frac{{\left|{A}\right|}^{{k}}}{{k}!}\right)\left(\frac{1}{2}\right)$
73 peano2nn0 ${⊢}{k}\in {ℕ}_{0}\to {k}+1\in {ℕ}_{0}$
74 25 73 syl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {k}+1\in {ℕ}_{0}$
75 1 eftval ${⊢}{k}+1\in {ℕ}_{0}\to {F}\left({k}+1\right)=\frac{{{A}}^{{k}+1}}{\left({k}+1\right)!}$
76 74 75 syl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {F}\left({k}+1\right)=\frac{{{A}}^{{k}+1}}{\left({k}+1\right)!}$
77 76 fveq2d ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left|{F}\left({k}+1\right)\right|=\left|\frac{{{A}}^{{k}+1}}{\left({k}+1\right)!}\right|$
78 absexp ${⊢}\left({A}\in ℂ\wedge {k}+1\in {ℕ}_{0}\right)\to \left|{{A}}^{{k}+1}\right|={\left|{A}\right|}^{{k}+1}$
79 74 78 syldan ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left|{{A}}^{{k}+1}\right|={\left|{A}\right|}^{{k}+1}$
80 56 25 expp1d ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {\left|{A}\right|}^{{k}+1}={\left|{A}\right|}^{{k}}\left|{A}\right|$
81 79 80 eqtrd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left|{{A}}^{{k}+1}\right|={\left|{A}\right|}^{{k}}\left|{A}\right|$
82 74 faccld ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left({k}+1\right)!\in ℕ$
83 82 nnred ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left({k}+1\right)!\in ℝ$
84 82 nnnn0d ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left({k}+1\right)!\in {ℕ}_{0}$
85 84 nn0ge0d ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to 0\le \left({k}+1\right)!$
86 83 85 absidd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left|\left({k}+1\right)!\right|=\left({k}+1\right)!$
87 facp1 ${⊢}{k}\in {ℕ}_{0}\to \left({k}+1\right)!={k}!\left({k}+1\right)$
88 25 87 syl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left({k}+1\right)!={k}!\left({k}+1\right)$
89 86 88 eqtrd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left|\left({k}+1\right)!\right|={k}!\left({k}+1\right)$
90 81 89 oveq12d ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \frac{\left|{{A}}^{{k}+1}\right|}{\left|\left({k}+1\right)!\right|}=\frac{{\left|{A}\right|}^{{k}}\left|{A}\right|}{{k}!\left({k}+1\right)}$
91 expcl ${⊢}\left({A}\in ℂ\wedge {k}+1\in {ℕ}_{0}\right)\to {{A}}^{{k}+1}\in ℂ$
92 74 91 syldan ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {{A}}^{{k}+1}\in ℂ$
93 82 nncnd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left({k}+1\right)!\in ℂ$
94 82 nnne0d ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left({k}+1\right)!\ne 0$
95 92 93 94 absdivd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left|\frac{{{A}}^{{k}+1}}{\left({k}+1\right)!}\right|=\frac{\left|{{A}}^{{k}+1}\right|}{\left|\left({k}+1\right)!\right|}$
96 30 recnd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {\left|{A}\right|}^{{k}}\in ℂ$
97 31 nncnd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {k}!\in ℂ$
98 31 nnne0d ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {k}!\ne 0$
99 27 nnne0d ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {k}+1\ne 0$
100 96 97 56 60 98 99 divmuldivd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left(\frac{{\left|{A}\right|}^{{k}}}{{k}!}\right)\left(\frac{\left|{A}\right|}{{k}+1}\right)=\frac{{\left|{A}\right|}^{{k}}\left|{A}\right|}{{k}!\left({k}+1\right)}$
101 90 95 100 3eqtr4d ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left|\frac{{{A}}^{{k}+1}}{\left({k}+1\right)!}\right|=\left(\frac{{\left|{A}\right|}^{{k}}}{{k}!}\right)\left(\frac{\left|{A}\right|}{{k}+1}\right)$
102 77 101 eqtrd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left|{F}\left({k}+1\right)\right|=\left(\frac{{\left|{A}\right|}^{{k}}}{{k}!}\right)\left(\frac{\left|{A}\right|}{{k}+1}\right)$
103 halfcn ${⊢}\frac{1}{2}\in ℂ$
104 25 22 syldan ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {F}\left({k}\right)\in ℂ$
105 104 abscld ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left|{F}\left({k}\right)\right|\in ℝ$
106 105 recnd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left|{F}\left({k}\right)\right|\in ℂ$
107 mulcom ${⊢}\left(\frac{1}{2}\in ℂ\wedge \left|{F}\left({k}\right)\right|\in ℂ\right)\to \left(\frac{1}{2}\right)\left|{F}\left({k}\right)\right|=\left|{F}\left({k}\right)\right|\left(\frac{1}{2}\right)$
108 103 106 107 sylancr ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left(\frac{1}{2}\right)\left|{F}\left({k}\right)\right|=\left|{F}\left({k}\right)\right|\left(\frac{1}{2}\right)$
109 25 19 syl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to {F}\left({k}\right)=\frac{{{A}}^{{k}}}{{k}!}$
110 109 fveq2d ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left|{F}\left({k}\right)\right|=\left|\frac{{{A}}^{{k}}}{{k}!}\right|$
111 eftabs ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to \left|\frac{{{A}}^{{k}}}{{k}!}\right|=\frac{{\left|{A}\right|}^{{k}}}{{k}!}$
112 25 111 syldan ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left|\frac{{{A}}^{{k}}}{{k}!}\right|=\frac{{\left|{A}\right|}^{{k}}}{{k}!}$
113 110 112 eqtrd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left|{F}\left({k}\right)\right|=\frac{{\left|{A}\right|}^{{k}}}{{k}!}$
114 113 oveq1d ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left|{F}\left({k}\right)\right|\left(\frac{1}{2}\right)=\left(\frac{{\left|{A}\right|}^{{k}}}{{k}!}\right)\left(\frac{1}{2}\right)$
115 108 114 eqtrd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left(\frac{1}{2}\right)\left|{F}\left({k}\right)\right|=\left(\frac{{\left|{A}\right|}^{{k}}}{{k}!}\right)\left(\frac{1}{2}\right)$
116 72 102 115 3brtr4d ${⊢}\left({A}\in ℂ\wedge {k}\in {ℤ}_{\ge ⌊2\left|{A}\right|⌋}\right)\to \left|{F}\left({k}+1\right)\right|\le \left(\frac{1}{2}\right)\left|{F}\left({k}\right)\right|$
117 2 3 5 7 18 22 116 cvgrat ${⊢}{A}\in ℂ\to seq0\left(+,{F}\right)\in \mathrm{dom}⇝$