Theorem efcllem 16090

Description: Lemma for efcl 16095. The series that defines the exponential function converges, in the case where its argument is nonzero. The ratio test cvgrat 15896 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.)

Hypothesis

Ref	Expression
eftval.1	⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))

Assertion

Ref	Expression
efcllem	⊢ (𝐴 ∈ ℂ → seq0( + , 𝐹) ∈ dom ⇝ )

Distinct variable group:   𝐴,𝑛

Allowed substitution hint:   𝐹(𝑛)

Proof of Theorem efcllem

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nn0uz 12874	. 2 ⊢ ℕ0 = (ℤ≥‘0)
2		eqid 2761	. 2 ⊢ (ℤ≥‘(⌊‘(2 · (abs‘𝐴)))) = (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))
3		halfre 12431	. . 3 ⊢ (1 / 2) ∈ ℝ
4	3	a1i 11	. 2 ⊢ (𝐴 ∈ ℂ → (1 / 2) ∈ ℝ)
5		halflt1 12435	. . 3 ⊢ (1 / 2) < 1
6	5	a1i 11	. 2 ⊢ (𝐴 ∈ ℂ → (1 / 2) < 1)
7		2re 12289	. . . 4 ⊢ 2 ∈ ℝ
8		abscl 15288	. . . 4 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
9		remulcl 11155	. . . 4 ⊢ ((2 ∈ ℝ ∧ (abs‘𝐴) ∈ ℝ) → (2 · (abs‘𝐴)) ∈ ℝ)
10	7, 8, 9	sylancr 596	. . 3 ⊢ (𝐴 ∈ ℂ → (2 · (abs‘𝐴)) ∈ ℝ)
11	7	a1i 11	. . . 4 ⊢ (𝐴 ∈ ℂ → 2 ∈ ℝ)
12		0le2 12317	. . . . 5 ⊢ 0 ≤ 2
13	12	a1i 11	. . . 4 ⊢ (𝐴 ∈ ℂ → 0 ≤ 2)
14		absge0 15297	. . . 4 ⊢ (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴))
15	11, 8, 13, 14	mulge0d 11761	. . 3 ⊢ (𝐴 ∈ ℂ → 0 ≤ (2 · (abs‘𝐴)))
16		flge0nn0 13827	. . 3 ⊢ (((2 · (abs‘𝐴)) ∈ ℝ ∧ 0 ≤ (2 · (abs‘𝐴))) → (⌊‘(2 · (abs‘𝐴))) ∈ ℕ0)
17	10, 15, 16	syl2anc 593	. 2 ⊢ (𝐴 ∈ ℂ → (⌊‘(2 · (abs‘𝐴))) ∈ ℕ0)
18		eftval.1	. . . . 5 ⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))
19	18	eftval 16089	. . . 4 ⊢ (𝑘 ∈ ℕ0 → (𝐹‘𝑘) = ((𝐴↑𝑘) / (!‘𝑘)))
20	19	adantl 485	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) = ((𝐴↑𝑘) / (!‘𝑘)))
21		eftcl 16086	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝐴↑𝑘) / (!‘𝑘)) ∈ ℂ)
22	20, 21	eqeltrd 2861	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ∈ ℂ)
23	8	adantr 484	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘𝐴) ∈ ℝ)
24		eluznn0 12915	. . . . . . 7 ⊢ (((⌊‘(2 · (abs‘𝐴))) ∈ ℕ0 ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 𝑘 ∈ ℕ0)
25	17, 24	sylan 589	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 𝑘 ∈ ℕ0)
26		nn0p1nn 12517	. . . . . 6 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ)
27	25, 26	syl 17	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ∈ ℕ)
28	23, 27	nndivred 12264	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴) / (𝑘 + 1)) ∈ ℝ)
29	3	a1i 11	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (1 / 2) ∈ ℝ)
30	23, 25	reexpcld 14173	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴)↑𝑘) ∈ ℝ)
31	25	faccld 14294	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘𝑘) ∈ ℕ)
32	30, 31	nndivred 12264	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (((abs‘𝐴)↑𝑘) / (!‘𝑘)) ∈ ℝ)
33		expcl 14089	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴↑𝑘) ∈ ℂ)
34	25, 33	syldan 600	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝐴↑𝑘) ∈ ℂ)
35	34	absge0d 15457	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 0 ≤ (abs‘(𝐴↑𝑘)))
36		absexp 15314	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (abs‘(𝐴↑𝑘)) = ((abs‘𝐴)↑𝑘))
37	25, 36	syldan 600	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐴↑𝑘)) = ((abs‘𝐴)↑𝑘))
38	35, 37	breqtrd 5125	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 0 ≤ ((abs‘𝐴)↑𝑘))
39	31	nnred 12222	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘𝑘) ∈ ℝ)
40	31	nngt0d 12259	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 0 < (!‘𝑘))
41		divge0 12058	. . . . 5 ⊢ (((((abs‘𝐴)↑𝑘) ∈ ℝ ∧ 0 ≤ ((abs‘𝐴)↑𝑘)) ∧ ((!‘𝑘) ∈ ℝ ∧ 0 < (!‘𝑘))) → 0 ≤ (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
42	30, 38, 39, 40, 41	syl22anc 849	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 0 ≤ (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
43	10	adantr 484	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (2 · (abs‘𝐴)) ∈ ℝ)
44		peano2nn0 12518	. . . . . . . . . . 11 ⊢ ((⌊‘(2 · (abs‘𝐴))) ∈ ℕ0 → ((⌊‘(2 · (abs‘𝐴))) + 1) ∈ ℕ0)
45	17, 44	syl 17	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((⌊‘(2 · (abs‘𝐴))) + 1) ∈ ℕ0)
46	45	nn0red 12540	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((⌊‘(2 · (abs‘𝐴))) + 1) ∈ ℝ)
47	46	adantr 484	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((⌊‘(2 · (abs‘𝐴))) + 1) ∈ ℝ)
48	27	nnred 12222	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ∈ ℝ)
49		flltp1 13807	. . . . . . . . 9 ⊢ ((2 · (abs‘𝐴)) ∈ ℝ → (2 · (abs‘𝐴)) < ((⌊‘(2 · (abs‘𝐴))) + 1))
50	43, 49	syl 17	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (2 · (abs‘𝐴)) < ((⌊‘(2 · (abs‘𝐴))) + 1))
51		eluzp1p1 12864	. . . . . . . . . 10 ⊢ (𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴)))) → (𝑘 + 1) ∈ (ℤ≥‘((⌊‘(2 · (abs‘𝐴))) + 1)))
52	51	adantl 485	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ∈ (ℤ≥‘((⌊‘(2 · (abs‘𝐴))) + 1)))
53		eluzle 12849	. . . . . . . . 9 ⊢ ((𝑘 + 1) ∈ (ℤ≥‘((⌊‘(2 · (abs‘𝐴))) + 1)) → ((⌊‘(2 · (abs‘𝐴))) + 1) ≤ (𝑘 + 1))
54	52, 53	syl 17	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((⌊‘(2 · (abs‘𝐴))) + 1) ≤ (𝑘 + 1))
55	43, 47, 48, 50, 54	ltletrd 11340	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (2 · (abs‘𝐴)) < (𝑘 + 1))
56	23	recnd 11207	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘𝐴) ∈ ℂ)
57		2cn 12290	. . . . . . . 8 ⊢ 2 ∈ ℂ
58		mulcom 11156	. . . . . . . 8 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 2 ∈ ℂ) → ((abs‘𝐴) · 2) = (2 · (abs‘𝐴)))
59	56, 57, 58	sylancl 595	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴) · 2) = (2 · (abs‘𝐴)))
60	27	nncnd 12223	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ∈ ℂ)
61	60	mullidd 11197	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (1 · (𝑘 + 1)) = (𝑘 + 1))
62	55, 59, 61	3brtr4d 5131	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴) · 2) < (1 · (𝑘 + 1)))
63		2rp 12995	. . . . . . . 8 ⊢ 2 ∈ ℝ+
64	63	a1i 11	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 2 ∈ ℝ+)
65		1red 11179	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 1 ∈ ℝ)
66	27	nnrpd 13032	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ∈ ℝ+)
67	23, 64, 65, 66	lt2mul2divd 13103	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (((abs‘𝐴) · 2) < (1 · (𝑘 + 1)) ↔ ((abs‘𝐴) / (𝑘 + 1)) < (1 / 2)))
68	62, 67	mpbid 234	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴) / (𝑘 + 1)) < (1 / 2))
69		ltle 11268	. . . . . 6 ⊢ ((((abs‘𝐴) / (𝑘 + 1)) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (((abs‘𝐴) / (𝑘 + 1)) < (1 / 2) → ((abs‘𝐴) / (𝑘 + 1)) ≤ (1 / 2)))
70	28, 3, 69	sylancl 595	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (((abs‘𝐴) / (𝑘 + 1)) < (1 / 2) → ((abs‘𝐴) / (𝑘 + 1)) ≤ (1 / 2)))
71	68, 70	mpd 15	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴) / (𝑘 + 1)) ≤ (1 / 2))
72	28, 29, 32, 42, 71	lemul2ad 12129	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · ((abs‘𝐴) / (𝑘 + 1))) ≤ ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · (1 / 2)))
73		peano2nn0 12518	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
74	25, 73	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ∈ ℕ0)
75	18	eftval 16089	. . . . . 6 ⊢ ((𝑘 + 1) ∈ ℕ0 → (𝐹‘(𝑘 + 1)) = ((𝐴↑(𝑘 + 1)) / (!‘(𝑘 + 1))))
76	74, 75	syl 17	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝐹‘(𝑘 + 1)) = ((𝐴↑(𝑘 + 1)) / (!‘(𝑘 + 1))))
77	76	fveq2d 6867	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘(𝑘 + 1))) = (abs‘((𝐴↑(𝑘 + 1)) / (!‘(𝑘 + 1)))))
78		absexp 15314	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (𝑘 + 1) ∈ ℕ0) → (abs‘(𝐴↑(𝑘 + 1))) = ((abs‘𝐴)↑(𝑘 + 1)))
79	74, 78	syldan 600	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐴↑(𝑘 + 1))) = ((abs‘𝐴)↑(𝑘 + 1)))
80	56, 25	expp1d 14157	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴)↑(𝑘 + 1)) = (((abs‘𝐴)↑𝑘) · (abs‘𝐴)))
81	79, 80	eqtrd 2796	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐴↑(𝑘 + 1))) = (((abs‘𝐴)↑𝑘) · (abs‘𝐴)))
82	74	faccld 14294	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘(𝑘 + 1)) ∈ ℕ)
83	82	nnred 12222	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘(𝑘 + 1)) ∈ ℝ)
84	82	nnnn0d 12539	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘(𝑘 + 1)) ∈ ℕ0)
85	84	nn0ge0d 12542	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 0 ≤ (!‘(𝑘 + 1)))
86	83, 85	absidd 15433	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(!‘(𝑘 + 1))) = (!‘(𝑘 + 1)))
87		facp1 14288	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1)))
88	25, 87	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1)))
89	86, 88	eqtrd 2796	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(!‘(𝑘 + 1))) = ((!‘𝑘) · (𝑘 + 1)))
90	81, 89	oveq12d 7410	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘(𝐴↑(𝑘 + 1))) / (abs‘(!‘(𝑘 + 1)))) = ((((abs‘𝐴)↑𝑘) · (abs‘𝐴)) / ((!‘𝑘) · (𝑘 + 1))))
91		expcl 14089	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (𝑘 + 1) ∈ ℕ0) → (𝐴↑(𝑘 + 1)) ∈ ℂ)
92	74, 91	syldan 600	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝐴↑(𝑘 + 1)) ∈ ℂ)
93	82	nncnd 12223	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘(𝑘 + 1)) ∈ ℂ)
94	82	nnne0d 12260	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘(𝑘 + 1)) ≠ 0)
95	92, 93, 94	absdivd 15468	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘((𝐴↑(𝑘 + 1)) / (!‘(𝑘 + 1)))) = ((abs‘(𝐴↑(𝑘 + 1))) / (abs‘(!‘(𝑘 + 1)))))
96	30	recnd 11207	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴)↑𝑘) ∈ ℂ)
97	31	nncnd 12223	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘𝑘) ∈ ℂ)
98	31	nnne0d 12260	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘𝑘) ≠ 0)
99	27	nnne0d 12260	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ≠ 0)
100	96, 97, 56, 60, 98, 99	divmuldivd 12005	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · ((abs‘𝐴) / (𝑘 + 1))) = ((((abs‘𝐴)↑𝑘) · (abs‘𝐴)) / ((!‘𝑘) · (𝑘 + 1))))
101	90, 95, 100	3eqtr4d 2806	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘((𝐴↑(𝑘 + 1)) / (!‘(𝑘 + 1)))) = ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · ((abs‘𝐴) / (𝑘 + 1))))
102	77, 101	eqtrd 2796	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘(𝑘 + 1))) = ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · ((abs‘𝐴) / (𝑘 + 1))))
103		halfcn 12432	. . . . 5 ⊢ (1 / 2) ∈ ℂ
104	25, 22	syldan 600	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝐹‘𝑘) ∈ ℂ)
105	104	abscld 15449	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘𝑘)) ∈ ℝ)
106	105	recnd 11207	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘𝑘)) ∈ ℂ)
107		mulcom 11156	. . . . 5 ⊢ (((1 / 2) ∈ ℂ ∧ (abs‘(𝐹‘𝑘)) ∈ ℂ) → ((1 / 2) · (abs‘(𝐹‘𝑘))) = ((abs‘(𝐹‘𝑘)) · (1 / 2)))
108	103, 106, 107	sylancr 596	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((1 / 2) · (abs‘(𝐹‘𝑘))) = ((abs‘(𝐹‘𝑘)) · (1 / 2)))
109	25, 19	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝐹‘𝑘) = ((𝐴↑𝑘) / (!‘𝑘)))
110	109	fveq2d 6867	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘𝑘)) = (abs‘((𝐴↑𝑘) / (!‘𝑘))))
111		eftabs 16088	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (abs‘((𝐴↑𝑘) / (!‘𝑘))) = (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
112	25, 111	syldan 600	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘((𝐴↑𝑘) / (!‘𝑘))) = (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
113	110, 112	eqtrd 2796	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘𝑘)) = (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
114	113	oveq1d 7407	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘(𝐹‘𝑘)) · (1 / 2)) = ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · (1 / 2)))
115	108, 114	eqtrd 2796	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((1 / 2) · (abs‘(𝐹‘𝑘))) = ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · (1 / 2)))
116	72, 102, 115	3brtr4d 5131	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘(𝑘 + 1))) ≤ ((1 / 2) · (abs‘(𝐹‘𝑘))))
117	1, 2, 4, 6, 17, 22, 116	cvgrat 15896	1 ⊢ (𝐴 ∈ ℂ → seq0( + , 𝐹) ∈ dom ⇝ )

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141   class class class wbr 5099   ↦ cmpt 5180  dom cdm 5645  ‘cfv 6517  (class class class)co 7392  ℂcc 11068  ℝcr 11069  0cc0 11070  1c1 11071   + caddc 11073   · cmul 11075   < clt 11213   ≤ cle 11214   / cdiv 11841  ℕcn 12207  2c2 12269  ℕ₀cn0 12478  ℤ_≥cuz 12836  ℝ⁺crp 12990  ⌊cfl 13797  seqcseq 14011  ↑cexp 14071  !cfa 14283  abscabs 15244   ⇝ cli 15494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714  ax-inf2 9593  ax-cnex 11126  ax-resscn 11127  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-addrcl 11131  ax-mulcl 11132  ax-mulrcl 11133  ax-mulcom 11134  ax-addass 11135  ax-mulass 11136  ax-distr 11137  ax-i2m1 11138  ax-1ne0 11139  ax-1rid 11140  ax-rnegex 11141  ax-rrecex 11142  ax-cnre 11143  ax-pre-lttri 11144  ax-pre-lttrn 11145  ax-pre-ltadd 11146  ax-pre-mulgt0 11147  ax-pre-sup 11148

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-int 4905  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5540  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-se 5599  df-we 5600  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-pred 6284  df-ord 6345  df-on 6346  df-lim 6347  df-suc 6348  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-isom 6526  df-riota 7349  df-ov 7395  df-oprab 7396  df-mpo 7397  df-om 7843  df-1st 7966  df-2nd 7967  df-frecs 8257  df-wrecs 8288  df-recs 8337  df-rdg 8376  df-1o 8432  df-er 8673  df-pm 8806  df-en 8924  df-dom 8925  df-sdom 8926  df-fin 8927  df-sup 9385  df-inf 9386  df-oi 9455  df-card 9894  df-pnf 11215  df-mnf 11216  df-xr 11217  df-ltxr 11218  df-le 11219  df-sub 11413  df-neg 11414  df-div 11842  df-nn 12208  df-2 12277  df-3 12278  df-n0 12479  df-z 12566  df-uz 12837  df-rp 12991  df-ico 13352  df-fz 13510  df-fzo 13657  df-fl 13799  df-seq 14012  df-exp 14072  df-fac 14284  df-hash 14341  df-shft 15077  df-cj 15109  df-re 15110  df-im 15111  df-sqrt 15245  df-abs 15246  df-limsup 15481  df-clim 15498  df-rlim 15499  df-sum 15697

This theorem is referenced by:  eff  16094  efcvg  16098  reefcl  16100  efaddlem  16106  eftlcvg  16121  effsumlt  16126  eflegeo  16136  eirrlem  16219  expfac  46195