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	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
Assertion	efcllem	⊢ ( 𝐴 ∈ ℂ → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )

Proof

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