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 ⊢ 𝐹 = ( 𝑛 ∈ ℕ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 mulid2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 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 ⇝ )