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 = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
Assertion efcllem 
|- ( A e. CC -> seq 0 ( + , F ) e. dom ~~> )

Proof

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