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 = (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})$
	Assertion	efcllem	$⊢ A \in ℂ \to seq 0 (+ F) \in dom ⇝$

Proof

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

Metamath Proof Explorer

Theorem efcllem

Proof