Metamath Proof Explorer

Theorem subfaclim

Description: The subfactorial converges rapidly to N ! / _e . This is part of Metamath 100 proof #88. (Contributed by Mario Carneiro, 23-Jan-2015)

Ref Expression
Hypotheses derang.d 
|- D = ( x e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
subfac.n 
|- S = ( n e. NN0 |-> ( D ` ( 1 ... n ) ) )
Assertion subfaclim 
|- ( N e. NN -> ( abs ` ( ( ( ! ` N ) / _e ) - ( S ` N ) ) ) < ( 1 / N ) )

Proof

Step Hyp Ref Expression
1 derang.d 
 |-  D = ( x e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
2 subfac.n 
 |-  S = ( n e. NN0 |-> ( D ` ( 1 ... n ) ) )
3 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
4 faccl 
 |-  ( N e. NN0 -> ( ! ` N ) e. NN )
5 3 4 syl 
 |-  ( N e. NN -> ( ! ` N ) e. NN )
6 5 nncnd 
 |-  ( N e. NN -> ( ! ` N ) e. CC )
7 ere 
 |-  _e e. RR
8 7 recni 
 |-  _e e. CC
9 epos 
 |-  0 < _e
10 7 9 gt0ne0ii 
 |-  _e =/= 0
11 divcl 
 |-  ( ( ( ! ` N ) e. CC /\ _e e. CC /\ _e =/= 0 ) -> ( ( ! ` N ) / _e ) e. CC )
12 8 10 11 mp3an23 
 |-  ( ( ! ` N ) e. CC -> ( ( ! ` N ) / _e ) e. CC )
13 6 12 syl 
 |-  ( N e. NN -> ( ( ! ` N ) / _e ) e. CC )
14 1 2 subfacf 
 |-  S : NN0 --> NN0
15 14 ffvelrni 
 |-  ( N e. NN0 -> ( S ` N ) e. NN0 )
16 3 15 syl 
 |-  ( N e. NN -> ( S ` N ) e. NN0 )
17 16 nn0cnd 
 |-  ( N e. NN -> ( S ` N ) e. CC )
18 13 17 subcld 
 |-  ( N e. NN -> ( ( ( ! ` N ) / _e ) - ( S ` N ) ) e. CC )
19 18 abscld 
 |-  ( N e. NN -> ( abs ` ( ( ( ! ` N ) / _e ) - ( S ` N ) ) ) e. RR )
20 peano2nn 
 |-  ( N e. NN -> ( N + 1 ) e. NN )
21 20 peano2nnd 
 |-  ( N e. NN -> ( ( N + 1 ) + 1 ) e. NN )
22 21 nnred 
 |-  ( N e. NN -> ( ( N + 1 ) + 1 ) e. RR )
23 20 20 nnmulcld 
 |-  ( N e. NN -> ( ( N + 1 ) x. ( N + 1 ) ) e. NN )
24 22 23 nndivred 
 |-  ( N e. NN -> ( ( ( N + 1 ) + 1 ) / ( ( N + 1 ) x. ( N + 1 ) ) ) e. RR )
25 nnrecre 
 |-  ( N e. NN -> ( 1 / N ) e. RR )
26 eqid 
 |-  ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ! ` n ) ) )
27 eqid 
 |-  ( n e. NN0 |-> ( ( ( abs ` -u 1 ) ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( ( abs ` -u 1 ) ^ n ) / ( ! ` n ) ) )
28 eqid 
 |-  ( n e. NN0 |-> ( ( ( ( abs ` -u 1 ) ^ ( N + 1 ) ) / ( ! ` ( N + 1 ) ) ) x. ( ( 1 / ( ( N + 1 ) + 1 ) ) ^ n ) ) ) = ( n e. NN0 |-> ( ( ( ( abs ` -u 1 ) ^ ( N + 1 ) ) / ( ! ` ( N + 1 ) ) ) x. ( ( 1 / ( ( N + 1 ) + 1 ) ) ^ n ) ) )
29 neg1cn 
 |-  -u 1 e. CC
30 29 a1i 
 |-  ( N e. NN -> -u 1 e. CC )
31 ax-1cn 
 |-  1 e. CC
32 31 absnegi 
 |-  ( abs ` -u 1 ) = ( abs ` 1 )
33 abs1 
 |-  ( abs ` 1 ) = 1
34 32 33 eqtri 
 |-  ( abs ` -u 1 ) = 1
35 1le1 
 |-  1 <_ 1
36 34 35 eqbrtri 
 |-  ( abs ` -u 1 ) <_ 1
37 36 a1i 
 |-  ( N e. NN -> ( abs ` -u 1 ) <_ 1 )
38 26 27 28 20 30 37 eftlub 
 |-  ( N e. NN -> ( abs ` sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ! ` n ) ) ) ` k ) ) <_ ( ( ( abs ` -u 1 ) ^ ( N + 1 ) ) x. ( ( ( N + 1 ) + 1 ) / ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) ) ) )
39 20 nnnn0d 
 |-  ( N e. NN -> ( N + 1 ) e. NN0 )
40 eluznn0 
 |-  ( ( ( N + 1 ) e. NN0 /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> k e. NN0 )
41 39 40 sylan 
 |-  ( ( N e. NN /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> k e. NN0 )
42 26 eftval 
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ! ` n ) ) ) ` k ) = ( ( -u 1 ^ k ) / ( ! ` k ) ) )
43 41 42 syl 
 |-  ( ( N e. NN /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ! ` n ) ) ) ` k ) = ( ( -u 1 ^ k ) / ( ! ` k ) ) )
44 43 sumeq2dv 
 |-  ( N e. NN -> sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ! ` n ) ) ) ` k ) = sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) )
45 44 fveq2d 
 |-  ( N e. NN -> ( abs ` sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ! ` n ) ) ) ` k ) ) = ( abs ` sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) )
46 34 oveq1i 
 |-  ( ( abs ` -u 1 ) ^ ( N + 1 ) ) = ( 1 ^ ( N + 1 ) )
47 20 nnzd 
 |-  ( N e. NN -> ( N + 1 ) e. ZZ )
48 1exp 
 |-  ( ( N + 1 ) e. ZZ -> ( 1 ^ ( N + 1 ) ) = 1 )
49 47 48 syl 
 |-  ( N e. NN -> ( 1 ^ ( N + 1 ) ) = 1 )
50 46 49 syl5eq 
 |-  ( N e. NN -> ( ( abs ` -u 1 ) ^ ( N + 1 ) ) = 1 )
51 50 oveq1d 
 |-  ( N e. NN -> ( ( ( abs ` -u 1 ) ^ ( N + 1 ) ) x. ( ( ( N + 1 ) + 1 ) / ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) ) ) = ( 1 x. ( ( ( N + 1 ) + 1 ) / ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) ) ) )
52 faccl 
 |-  ( ( N + 1 ) e. NN0 -> ( ! ` ( N + 1 ) ) e. NN )
53 39 52 syl 
 |-  ( N e. NN -> ( ! ` ( N + 1 ) ) e. NN )
54 53 20 nnmulcld 
 |-  ( N e. NN -> ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) e. NN )
55 22 54 nndivred 
 |-  ( N e. NN -> ( ( ( N + 1 ) + 1 ) / ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) ) e. RR )
56 55 recnd 
 |-  ( N e. NN -> ( ( ( N + 1 ) + 1 ) / ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) ) e. CC )
57 56 mulid2d 
 |-  ( N e. NN -> ( 1 x. ( ( ( N + 1 ) + 1 ) / ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) ) ) = ( ( ( N + 1 ) + 1 ) / ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) ) )
58 51 57 eqtrd 
 |-  ( N e. NN -> ( ( ( abs ` -u 1 ) ^ ( N + 1 ) ) x. ( ( ( N + 1 ) + 1 ) / ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) ) ) = ( ( ( N + 1 ) + 1 ) / ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) ) )
59 38 45 58 3brtr3d 
 |-  ( N e. NN -> ( abs ` sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) <_ ( ( ( N + 1 ) + 1 ) / ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) ) )
60 eqid 
 |-  ( ZZ>= ` ( N + 1 ) ) = ( ZZ>= ` ( N + 1 ) )
61 eftcl 
 |-  ( ( -u 1 e. CC /\ k e. NN0 ) -> ( ( -u 1 ^ k ) / ( ! ` k ) ) e. CC )
62 29 61 mpan 
 |-  ( k e. NN0 -> ( ( -u 1 ^ k ) / ( ! ` k ) ) e. CC )
63 41 62 syl 
 |-  ( ( N e. NN /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( -u 1 ^ k ) / ( ! ` k ) ) e. CC )
64 26 eftlcvg 
 |-  ( ( -u 1 e. CC /\ ( N + 1 ) e. NN0 ) -> seq ( N + 1 ) ( + , ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ! ` n ) ) ) ) e. dom ~~> )
65 29 39 64 sylancr 
 |-  ( N e. NN -> seq ( N + 1 ) ( + , ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ! ` n ) ) ) ) e. dom ~~> )
66 60 47 43 63 65 isumcl 
 |-  ( N e. NN -> sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) e. CC )
67 66 abscld 
 |-  ( N e. NN -> ( abs ` sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) e. RR )
68 5 nnred 
 |-  ( N e. NN -> ( ! ` N ) e. RR )
69 5 nngt0d 
 |-  ( N e. NN -> 0 < ( ! ` N ) )
70 lemul2 
 |-  ( ( ( abs ` sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) e. RR /\ ( ( ( N + 1 ) + 1 ) / ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) ) e. RR /\ ( ( ! ` N ) e. RR /\ 0 < ( ! ` N ) ) ) -> ( ( abs ` sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) <_ ( ( ( N + 1 ) + 1 ) / ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) ) <-> ( ( ! ` N ) x. ( abs ` sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) ) <_ ( ( ! ` N ) x. ( ( ( N + 1 ) + 1 ) / ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) ) ) ) )
71 67 55 68 69 70 syl112anc 
 |-  ( N e. NN -> ( ( abs ` sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) <_ ( ( ( N + 1 ) + 1 ) / ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) ) <-> ( ( ! ` N ) x. ( abs ` sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) ) <_ ( ( ! ` N ) x. ( ( ( N + 1 ) + 1 ) / ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) ) ) ) )
72 59 71 mpbid 
 |-  ( N e. NN -> ( ( ! ` N ) x. ( abs ` sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) ) <_ ( ( ! ` N ) x. ( ( ( N + 1 ) + 1 ) / ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) ) ) )
73 1 2 subfacval2 
 |-  ( N e. NN0 -> ( S ` N ) = ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) )
74 3 73 syl 
 |-  ( N e. NN -> ( S ` N ) = ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) )
75 nncn 
 |-  ( N e. NN -> N e. CC )
76 pncan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
77 75 31 76 sylancl 
 |-  ( N e. NN -> ( ( N + 1 ) - 1 ) = N )
78 77 oveq2d 
 |-  ( N e. NN -> ( 0 ... ( ( N + 1 ) - 1 ) ) = ( 0 ... N ) )
79 78 sumeq1d 
 |-  ( N e. NN -> sum_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) = sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) / ( ! ` k ) ) )
80 79 oveq2d 
 |-  ( N e. NN -> ( ( ! ` N ) x. sum_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) = ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) )
81 74 80 eqtr4d 
 |-  ( N e. NN -> ( S ` N ) = ( ( ! ` N ) x. sum_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) )
82 81 oveq1d 
 |-  ( N e. NN -> ( ( S ` N ) + ( ( ! ` N ) x. sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) ) = ( ( ( ! ` N ) x. sum_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) + ( ( ! ` N ) x. sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) ) )
83 divrec 
 |-  ( ( ( ! ` N ) e. CC /\ _e e. CC /\ _e =/= 0 ) -> ( ( ! ` N ) / _e ) = ( ( ! ` N ) x. ( 1 / _e ) ) )
84 8 10 83 mp3an23 
 |-  ( ( ! ` N ) e. CC -> ( ( ! ` N ) / _e ) = ( ( ! ` N ) x. ( 1 / _e ) ) )
85 6 84 syl 
 |-  ( N e. NN -> ( ( ! ` N ) / _e ) = ( ( ! ` N ) x. ( 1 / _e ) ) )
86 df-e 
 |-  _e = ( exp ` 1 )
87 86 oveq2i 
 |-  ( 1 / _e ) = ( 1 / ( exp ` 1 ) )
88 efneg 
 |-  ( 1 e. CC -> ( exp ` -u 1 ) = ( 1 / ( exp ` 1 ) ) )
89 31 88 ax-mp 
 |-  ( exp ` -u 1 ) = ( 1 / ( exp ` 1 ) )
90 efval 
 |-  ( -u 1 e. CC -> ( exp ` -u 1 ) = sum_ k e. NN0 ( ( -u 1 ^ k ) / ( ! ` k ) ) )
91 29 90 ax-mp 
 |-  ( exp ` -u 1 ) = sum_ k e. NN0 ( ( -u 1 ^ k ) / ( ! ` k ) )
92 87 89 91 3eqtr2i 
 |-  ( 1 / _e ) = sum_ k e. NN0 ( ( -u 1 ^ k ) / ( ! ` k ) )
93 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
94 42 adantl 
 |-  ( ( N e. NN /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ! ` n ) ) ) ` k ) = ( ( -u 1 ^ k ) / ( ! ` k ) ) )
95 62 adantl 
 |-  ( ( N e. NN /\ k e. NN0 ) -> ( ( -u 1 ^ k ) / ( ! ` k ) ) e. CC )
96 0nn0 
 |-  0 e. NN0
97 26 eftlcvg 
 |-  ( ( -u 1 e. CC /\ 0 e. NN0 ) -> seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ! ` n ) ) ) ) e. dom ~~> )
98 29 96 97 mp2an 
 |-  seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ! ` n ) ) ) ) e. dom ~~>
99 98 a1i 
 |-  ( N e. NN -> seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ! ` n ) ) ) ) e. dom ~~> )
100 93 60 39 94 95 99 isumsplit 
 |-  ( N e. NN -> sum_ k e. NN0 ( ( -u 1 ^ k ) / ( ! ` k ) ) = ( sum_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) + sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) )
101 92 100 syl5eq 
 |-  ( N e. NN -> ( 1 / _e ) = ( sum_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) + sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) )
102 101 oveq2d 
 |-  ( N e. NN -> ( ( ! ` N ) x. ( 1 / _e ) ) = ( ( ! ` N ) x. ( sum_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) + sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) ) )
103 fzfid 
 |-  ( N e. NN -> ( 0 ... ( ( N + 1 ) - 1 ) ) e. Fin )
104 elfznn0 
 |-  ( k e. ( 0 ... ( ( N + 1 ) - 1 ) ) -> k e. NN0 )
105 104 adantl 
 |-  ( ( N e. NN /\ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ) -> k e. NN0 )
106 29 105 61 sylancr 
 |-  ( ( N e. NN /\ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ) -> ( ( -u 1 ^ k ) / ( ! ` k ) ) e. CC )
107 103 106 fsumcl 
 |-  ( N e. NN -> sum_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) e. CC )
108 6 107 66 adddid 
 |-  ( N e. NN -> ( ( ! ` N ) x. ( sum_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) + sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) ) = ( ( ( ! ` N ) x. sum_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) + ( ( ! ` N ) x. sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) ) )
109 85 102 108 3eqtrd 
 |-  ( N e. NN -> ( ( ! ` N ) / _e ) = ( ( ( ! ` N ) x. sum_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) + ( ( ! ` N ) x. sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) ) )
110 82 109 eqtr4d 
 |-  ( N e. NN -> ( ( S ` N ) + ( ( ! ` N ) x. sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) ) = ( ( ! ` N ) / _e ) )
111 6 66 mulcld 
 |-  ( N e. NN -> ( ( ! ` N ) x. sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) e. CC )
112 13 17 111 subaddd 
 |-  ( N e. NN -> ( ( ( ( ! ` N ) / _e ) - ( S ` N ) ) = ( ( ! ` N ) x. sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) <-> ( ( S ` N ) + ( ( ! ` N ) x. sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) ) = ( ( ! ` N ) / _e ) ) )
113 110 112 mpbird 
 |-  ( N e. NN -> ( ( ( ! ` N ) / _e ) - ( S ` N ) ) = ( ( ! ` N ) x. sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) )
114 113 fveq2d 
 |-  ( N e. NN -> ( abs ` ( ( ( ! ` N ) / _e ) - ( S ` N ) ) ) = ( abs ` ( ( ! ` N ) x. sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) ) )
115 6 66 absmuld 
 |-  ( N e. NN -> ( abs ` ( ( ! ` N ) x. sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) ) = ( ( abs ` ( ! ` N ) ) x. ( abs ` sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) ) )
116 5 nnnn0d 
 |-  ( N e. NN -> ( ! ` N ) e. NN0 )
117 116 nn0ge0d 
 |-  ( N e. NN -> 0 <_ ( ! ` N ) )
118 68 117 absidd 
 |-  ( N e. NN -> ( abs ` ( ! ` N ) ) = ( ! ` N ) )
119 118 oveq1d 
 |-  ( N e. NN -> ( ( abs ` ( ! ` N ) ) x. ( abs ` sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) ) = ( ( ! ` N ) x. ( abs ` sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) ) )
120 114 115 119 3eqtrd 
 |-  ( N e. NN -> ( abs ` ( ( ( ! ` N ) / _e ) - ( S ` N ) ) ) = ( ( ! ` N ) x. ( abs ` sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) ) )
121 facp1 
 |-  ( N e. NN0 -> ( ! ` ( N + 1 ) ) = ( ( ! ` N ) x. ( N + 1 ) ) )
122 3 121 syl 
 |-  ( N e. NN -> ( ! ` ( N + 1 ) ) = ( ( ! ` N ) x. ( N + 1 ) ) )
123 122 oveq1d 
 |-  ( N e. NN -> ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) = ( ( ( ! ` N ) x. ( N + 1 ) ) x. ( N + 1 ) ) )
124 20 nncnd 
 |-  ( N e. NN -> ( N + 1 ) e. CC )
125 6 124 124 mulassd 
 |-  ( N e. NN -> ( ( ( ! ` N ) x. ( N + 1 ) ) x. ( N + 1 ) ) = ( ( ! ` N ) x. ( ( N + 1 ) x. ( N + 1 ) ) ) )
126 123 125 eqtr2d 
 |-  ( N e. NN -> ( ( ! ` N ) x. ( ( N + 1 ) x. ( N + 1 ) ) ) = ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) )
127 126 oveq2d 
 |-  ( N e. NN -> ( ( ( ! ` N ) x. ( ( N + 1 ) + 1 ) ) / ( ( ! ` N ) x. ( ( N + 1 ) x. ( N + 1 ) ) ) ) = ( ( ( ! ` N ) x. ( ( N + 1 ) + 1 ) ) / ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) ) )
128 21 nncnd 
 |-  ( N e. NN -> ( ( N + 1 ) + 1 ) e. CC )
129 23 nncnd 
 |-  ( N e. NN -> ( ( N + 1 ) x. ( N + 1 ) ) e. CC )
130 23 nnne0d 
 |-  ( N e. NN -> ( ( N + 1 ) x. ( N + 1 ) ) =/= 0 )
131 5 nnne0d 
 |-  ( N e. NN -> ( ! ` N ) =/= 0 )
132 128 129 6 130 131 divcan5d 
 |-  ( N e. NN -> ( ( ( ! ` N ) x. ( ( N + 1 ) + 1 ) ) / ( ( ! ` N ) x. ( ( N + 1 ) x. ( N + 1 ) ) ) ) = ( ( ( N + 1 ) + 1 ) / ( ( N + 1 ) x. ( N + 1 ) ) ) )
133 54 nncnd 
 |-  ( N e. NN -> ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) e. CC )
134 54 nnne0d 
 |-  ( N e. NN -> ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) =/= 0 )
135 6 128 133 134 divassd 
 |-  ( N e. NN -> ( ( ( ! ` N ) x. ( ( N + 1 ) + 1 ) ) / ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) ) = ( ( ! ` N ) x. ( ( ( N + 1 ) + 1 ) / ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) ) ) )
136 127 132 135 3eqtr3d 
 |-  ( N e. NN -> ( ( ( N + 1 ) + 1 ) / ( ( N + 1 ) x. ( N + 1 ) ) ) = ( ( ! ` N ) x. ( ( ( N + 1 ) + 1 ) / ( ( ! ` ( N + 1 ) ) x. ( N + 1 ) ) ) ) )
137 72 120 136 3brtr4d 
 |-  ( N e. NN -> ( abs ` ( ( ( ! ` N ) / _e ) - ( S ` N ) ) ) <_ ( ( ( N + 1 ) + 1 ) / ( ( N + 1 ) x. ( N + 1 ) ) ) )
138 nnmulcl 
 |-  ( ( ( ( N + 1 ) + 1 ) e. NN /\ N e. NN ) -> ( ( ( N + 1 ) + 1 ) x. N ) e. NN )
139 21 138 mpancom 
 |-  ( N e. NN -> ( ( ( N + 1 ) + 1 ) x. N ) e. NN )
140 139 nnred 
 |-  ( N e. NN -> ( ( ( N + 1 ) + 1 ) x. N ) e. RR )
141 140 ltp1d 
 |-  ( N e. NN -> ( ( ( N + 1 ) + 1 ) x. N ) < ( ( ( ( N + 1 ) + 1 ) x. N ) + 1 ) )
142 129 mulid2d 
 |-  ( N e. NN -> ( 1 x. ( ( N + 1 ) x. ( N + 1 ) ) ) = ( ( N + 1 ) x. ( N + 1 ) ) )
143 31 a1i 
 |-  ( N e. NN -> 1 e. CC )
144 75 143 124 adddird 
 |-  ( N e. NN -> ( ( N + 1 ) x. ( N + 1 ) ) = ( ( N x. ( N + 1 ) ) + ( 1 x. ( N + 1 ) ) ) )
145 75 124 mulcomd 
 |-  ( N e. NN -> ( N x. ( N + 1 ) ) = ( ( N + 1 ) x. N ) )
146 124 mulid2d 
 |-  ( N e. NN -> ( 1 x. ( N + 1 ) ) = ( N + 1 ) )
147 145 146 oveq12d 
 |-  ( N e. NN -> ( ( N x. ( N + 1 ) ) + ( 1 x. ( N + 1 ) ) ) = ( ( ( N + 1 ) x. N ) + ( N + 1 ) ) )
148 124 143 75 adddird 
 |-  ( N e. NN -> ( ( ( N + 1 ) + 1 ) x. N ) = ( ( ( N + 1 ) x. N ) + ( 1 x. N ) ) )
149 148 oveq1d 
 |-  ( N e. NN -> ( ( ( ( N + 1 ) + 1 ) x. N ) + 1 ) = ( ( ( ( N + 1 ) x. N ) + ( 1 x. N ) ) + 1 ) )
150 75 mulid2d 
 |-  ( N e. NN -> ( 1 x. N ) = N )
151 150 oveq2d 
 |-  ( N e. NN -> ( ( ( N + 1 ) x. N ) + ( 1 x. N ) ) = ( ( ( N + 1 ) x. N ) + N ) )
152 151 oveq1d 
 |-  ( N e. NN -> ( ( ( ( N + 1 ) x. N ) + ( 1 x. N ) ) + 1 ) = ( ( ( ( N + 1 ) x. N ) + N ) + 1 ) )
153 124 75 mulcld 
 |-  ( N e. NN -> ( ( N + 1 ) x. N ) e. CC )
154 153 75 143 addassd 
 |-  ( N e. NN -> ( ( ( ( N + 1 ) x. N ) + N ) + 1 ) = ( ( ( N + 1 ) x. N ) + ( N + 1 ) ) )
155 149 152 154 3eqtrd 
 |-  ( N e. NN -> ( ( ( ( N + 1 ) + 1 ) x. N ) + 1 ) = ( ( ( N + 1 ) x. N ) + ( N + 1 ) ) )
156 147 155 eqtr4d 
 |-  ( N e. NN -> ( ( N x. ( N + 1 ) ) + ( 1 x. ( N + 1 ) ) ) = ( ( ( ( N + 1 ) + 1 ) x. N ) + 1 ) )
157 142 144 156 3eqtrd 
 |-  ( N e. NN -> ( 1 x. ( ( N + 1 ) x. ( N + 1 ) ) ) = ( ( ( ( N + 1 ) + 1 ) x. N ) + 1 ) )
158 141 157 breqtrrd 
 |-  ( N e. NN -> ( ( ( N + 1 ) + 1 ) x. N ) < ( 1 x. ( ( N + 1 ) x. ( N + 1 ) ) ) )
159 nnre 
 |-  ( N e. NN -> N e. RR )
160 nngt0 
 |-  ( N e. NN -> 0 < N )
161 159 160 jca 
 |-  ( N e. NN -> ( N e. RR /\ 0 < N ) )
162 1red 
 |-  ( N e. NN -> 1 e. RR )
163 nnre 
 |-  ( ( ( N + 1 ) x. ( N + 1 ) ) e. NN -> ( ( N + 1 ) x. ( N + 1 ) ) e. RR )
164 nngt0 
 |-  ( ( ( N + 1 ) x. ( N + 1 ) ) e. NN -> 0 < ( ( N + 1 ) x. ( N + 1 ) ) )
165 163 164 jca 
 |-  ( ( ( N + 1 ) x. ( N + 1 ) ) e. NN -> ( ( ( N + 1 ) x. ( N + 1 ) ) e. RR /\ 0 < ( ( N + 1 ) x. ( N + 1 ) ) ) )
166 23 165 syl 
 |-  ( N e. NN -> ( ( ( N + 1 ) x. ( N + 1 ) ) e. RR /\ 0 < ( ( N + 1 ) x. ( N + 1 ) ) ) )
167 lt2mul2div 
 |-  ( ( ( ( ( N + 1 ) + 1 ) e. RR /\ ( N e. RR /\ 0 < N ) ) /\ ( 1 e. RR /\ ( ( ( N + 1 ) x. ( N + 1 ) ) e. RR /\ 0 < ( ( N + 1 ) x. ( N + 1 ) ) ) ) ) -> ( ( ( ( N + 1 ) + 1 ) x. N ) < ( 1 x. ( ( N + 1 ) x. ( N + 1 ) ) ) <-> ( ( ( N + 1 ) + 1 ) / ( ( N + 1 ) x. ( N + 1 ) ) ) < ( 1 / N ) ) )
168 22 161 162 166 167 syl22anc 
 |-  ( N e. NN -> ( ( ( ( N + 1 ) + 1 ) x. N ) < ( 1 x. ( ( N + 1 ) x. ( N + 1 ) ) ) <-> ( ( ( N + 1 ) + 1 ) / ( ( N + 1 ) x. ( N + 1 ) ) ) < ( 1 / N ) ) )
169 158 168 mpbid 
 |-  ( N e. NN -> ( ( ( N + 1 ) + 1 ) / ( ( N + 1 ) x. ( N + 1 ) ) ) < ( 1 / N ) )
170 19 24 25 137 169 lelttrd 
 |-  ( N e. NN -> ( abs ` ( ( ( ! ` N ) / _e ) - ( S ` N ) ) ) < ( 1 / N ) )