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=n0Ann!
Assertion efcllem Aseq0+Fdom

Proof

Step Hyp Ref Expression
1 eftval.1 F=n0Ann!
2 nn0uz 0=0
3 eqid 2A=2A
4 halfre 12
5 4 a1i A12
6 halflt1 12<1
7 6 a1i A12<1
8 2re 2
9 abscl AA
10 remulcl 2A2A
11 8 9 10 sylancr A2A
12 8 a1i A2
13 0le2 02
14 13 a1i A02
15 absge0 A0A
16 12 9 14 15 mulge0d A02A
17 flge0nn0 2A02A2A0
18 11 16 17 syl2anc A2A0
19 1 eftval k0Fk=Akk!
20 19 adantl Ak0Fk=Akk!
21 eftcl Ak0Akk!
22 20 21 eqeltrd Ak0Fk
23 9 adantr Ak2AA
24 eluznn0 2A0k2Ak0
25 18 24 sylan Ak2Ak0
26 nn0p1nn k0k+1
27 25 26 syl Ak2Ak+1
28 23 27 nndivred Ak2AAk+1
29 4 a1i Ak2A12
30 23 25 reexpcld Ak2AAk
31 25 faccld Ak2Ak!
32 30 31 nndivred Ak2AAkk!
33 expcl Ak0Ak
34 25 33 syldan Ak2AAk
35 34 absge0d Ak2A0Ak
36 absexp Ak0Ak=Ak
37 25 36 syldan Ak2AAk=Ak
38 35 37 breqtrd Ak2A0Ak
39 31 nnred Ak2Ak!
40 31 nngt0d Ak2A0<k!
41 divge0 Ak0Akk!0<k!0Akk!
42 30 38 39 40 41 syl22anc Ak2A0Akk!
43 11 adantr Ak2A2A
44 peano2nn0 2A02A+10
45 18 44 syl A2A+10
46 45 nn0red A2A+1
47 46 adantr Ak2A2A+1
48 27 nnred Ak2Ak+1
49 flltp1 2A2A<2A+1
50 43 49 syl Ak2A2A<2A+1
51 eluzp1p1 k2Ak+12A+1
52 51 adantl Ak2Ak+12A+1
53 eluzle k+12A+12A+1k+1
54 52 53 syl Ak2A2A+1k+1
55 43 47 48 50 54 ltletrd Ak2A2A<k+1
56 23 recnd Ak2AA
57 2cn 2
58 mulcom A2A2=2A
59 56 57 58 sylancl Ak2AA2=2A
60 27 nncnd Ak2Ak+1
61 60 mulid2d Ak2A1k+1=k+1
62 55 59 61 3brtr4d Ak2AA2<1k+1
63 2rp 2+
64 63 a1i Ak2A2+
65 1red Ak2A1
66 27 nnrpd Ak2Ak+1+
67 23 64 65 66 lt2mul2divd Ak2AA2<1k+1Ak+1<12
68 62 67 mpbid Ak2AAk+1<12
69 ltle Ak+112Ak+1<12Ak+112
70 28 4 69 sylancl Ak2AAk+1<12Ak+112
71 68 70 mpd Ak2AAk+112
72 28 29 32 42 71 lemul2ad Ak2AAkk!Ak+1Akk!12
73 peano2nn0 k0k+10
74 25 73 syl Ak2Ak+10
75 1 eftval k+10Fk+1=Ak+1k+1!
76 74 75 syl Ak2AFk+1=Ak+1k+1!
77 76 fveq2d Ak2AFk+1=Ak+1k+1!
78 absexp Ak+10Ak+1=Ak+1
79 74 78 syldan Ak2AAk+1=Ak+1
80 56 25 expp1d Ak2AAk+1=AkA
81 79 80 eqtrd Ak2AAk+1=AkA
82 74 faccld Ak2Ak+1!
83 82 nnred Ak2Ak+1!
84 82 nnnn0d Ak2Ak+1!0
85 84 nn0ge0d Ak2A0k+1!
86 83 85 absidd Ak2Ak+1!=k+1!
87 facp1 k0k+1!=k!k+1
88 25 87 syl Ak2Ak+1!=k!k+1
89 86 88 eqtrd Ak2Ak+1!=k!k+1
90 81 89 oveq12d Ak2AAk+1k+1!=AkAk!k+1
91 expcl Ak+10Ak+1
92 74 91 syldan Ak2AAk+1
93 82 nncnd Ak2Ak+1!
94 82 nnne0d Ak2Ak+1!0
95 92 93 94 absdivd Ak2AAk+1k+1!=Ak+1k+1!
96 30 recnd Ak2AAk
97 31 nncnd Ak2Ak!
98 31 nnne0d Ak2Ak!0
99 27 nnne0d Ak2Ak+10
100 96 97 56 60 98 99 divmuldivd Ak2AAkk!Ak+1=AkAk!k+1
101 90 95 100 3eqtr4d Ak2AAk+1k+1!=Akk!Ak+1
102 77 101 eqtrd Ak2AFk+1=Akk!Ak+1
103 halfcn 12
104 25 22 syldan Ak2AFk
105 104 abscld Ak2AFk
106 105 recnd Ak2AFk
107 mulcom 12Fk12Fk=Fk12
108 103 106 107 sylancr Ak2A12Fk=Fk12
109 25 19 syl Ak2AFk=Akk!
110 109 fveq2d Ak2AFk=Akk!
111 eftabs Ak0Akk!=Akk!
112 25 111 syldan Ak2AAkk!=Akk!
113 110 112 eqtrd Ak2AFk=Akk!
114 113 oveq1d Ak2AFk12=Akk!12
115 108 114 eqtrd Ak2A12Fk=Akk!12
116 72 102 115 3brtr4d Ak2AFk+112Fk
117 2 3 5 7 18 22 116 cvgrat Aseq0+Fdom