Metamath Proof Explorer

Theorem subfacval3

Description: Another closed form expression for the subfactorial. The expression |_( x + 1 / 2 ) is a way of saying "rounded to the nearest integer". (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 subfacval3 
|- ( N e. NN -> ( S ` N ) = ( |_ ` ( ( ( ! ` N ) / _e ) + ( 1 / 2 ) ) ) )

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 1 2 subfacf 
 |-  S : NN0 --> NN0
5 4 ffvelrni 
 |-  ( N e. NN0 -> ( S ` N ) e. NN0 )
6 3 5 syl 
 |-  ( N e. NN -> ( S ` N ) e. NN0 )
7 6 nn0zd 
 |-  ( N e. NN -> ( S ` N ) e. ZZ )
8 7 zred 
 |-  ( N e. NN -> ( S ` N ) e. RR )
9 faccl 
 |-  ( N e. NN0 -> ( ! ` N ) e. NN )
10 3 9 syl 
 |-  ( N e. NN -> ( ! ` N ) e. NN )
11 10 nnred 
 |-  ( N e. NN -> ( ! ` N ) e. RR )
12 epr 
 |-  _e e. RR+
13 rerpdivcl 
 |-  ( ( ( ! ` N ) e. RR /\ _e e. RR+ ) -> ( ( ! ` N ) / _e ) e. RR )
14 11 12 13 sylancl 
 |-  ( N e. NN -> ( ( ! ` N ) / _e ) e. RR )
15 halfre 
 |-  ( 1 / 2 ) e. RR
16 readdcl 
 |-  ( ( ( ( ! ` N ) / _e ) e. RR /\ ( 1 / 2 ) e. RR ) -> ( ( ( ! ` N ) / _e ) + ( 1 / 2 ) ) e. RR )
17 14 15 16 sylancl 
 |-  ( N e. NN -> ( ( ( ! ` N ) / _e ) + ( 1 / 2 ) ) e. RR )
18 elnn1uz2 
 |-  ( N e. NN <-> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
19 fveq2 
 |-  ( N = 1 -> ( ! ` N ) = ( ! ` 1 ) )
20 fac1 
 |-  ( ! ` 1 ) = 1
21 19 20 eqtrdi 
 |-  ( N = 1 -> ( ! ` N ) = 1 )
22 21 oveq1d 
 |-  ( N = 1 -> ( ( ! ` N ) / _e ) = ( 1 / _e ) )
23 fveq2 
 |-  ( N = 1 -> ( S ` N ) = ( S ` 1 ) )
24 1 2 subfac1 
 |-  ( S ` 1 ) = 0
25 23 24 eqtrdi 
 |-  ( N = 1 -> ( S ` N ) = 0 )
26 22 25 oveq12d 
 |-  ( N = 1 -> ( ( ( ! ` N ) / _e ) - ( S ` N ) ) = ( ( 1 / _e ) - 0 ) )
27 rpreccl 
 |-  ( _e e. RR+ -> ( 1 / _e ) e. RR+ )
28 12 27 ax-mp 
 |-  ( 1 / _e ) e. RR+
29 rpre 
 |-  ( ( 1 / _e ) e. RR+ -> ( 1 / _e ) e. RR )
30 28 29 ax-mp 
 |-  ( 1 / _e ) e. RR
31 30 recni 
 |-  ( 1 / _e ) e. CC
32 31 subid1i 
 |-  ( ( 1 / _e ) - 0 ) = ( 1 / _e )
33 26 32 eqtrdi 
 |-  ( N = 1 -> ( ( ( ! ` N ) / _e ) - ( S ` N ) ) = ( 1 / _e ) )
34 33 fveq2d 
 |-  ( N = 1 -> ( abs ` ( ( ( ! ` N ) / _e ) - ( S ` N ) ) ) = ( abs ` ( 1 / _e ) ) )
35 rpge0 
 |-  ( ( 1 / _e ) e. RR+ -> 0 <_ ( 1 / _e ) )
36 28 35 ax-mp 
 |-  0 <_ ( 1 / _e )
37 absid 
 |-  ( ( ( 1 / _e ) e. RR /\ 0 <_ ( 1 / _e ) ) -> ( abs ` ( 1 / _e ) ) = ( 1 / _e ) )
38 30 36 37 mp2an 
 |-  ( abs ` ( 1 / _e ) ) = ( 1 / _e )
39 34 38 eqtrdi 
 |-  ( N = 1 -> ( abs ` ( ( ( ! ` N ) / _e ) - ( S ` N ) ) ) = ( 1 / _e ) )
40 egt2lt3 
 |-  ( 2 < _e /\ _e < 3 )
41 40 simpli 
 |-  2 < _e
42 2re 
 |-  2 e. RR
43 ere 
 |-  _e e. RR
44 2pos 
 |-  0 < 2
45 epos 
 |-  0 < _e
46 42 43 44 45 ltrecii 
 |-  ( 2 < _e <-> ( 1 / _e ) < ( 1 / 2 ) )
47 41 46 mpbi 
 |-  ( 1 / _e ) < ( 1 / 2 )
48 39 47 eqbrtrdi 
 |-  ( N = 1 -> ( abs ` ( ( ( ! ` N ) / _e ) - ( S ` N ) ) ) < ( 1 / 2 ) )
49 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
50 14 8 resubcld 
 |-  ( N e. NN -> ( ( ( ! ` N ) / _e ) - ( S ` N ) ) e. RR )
51 50 recnd 
 |-  ( N e. NN -> ( ( ( ! ` N ) / _e ) - ( S ` N ) ) e. CC )
52 49 51 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( ! ` N ) / _e ) - ( S ` N ) ) e. CC )
53 52 abscld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( abs ` ( ( ( ! ` N ) / _e ) - ( S ` N ) ) ) e. RR )
54 49 nnrecred 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 / N ) e. RR )
55 15 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 / 2 ) e. RR )
56 1 2 subfaclim 
 |-  ( N e. NN -> ( abs ` ( ( ( ! ` N ) / _e ) - ( S ` N ) ) ) < ( 1 / N ) )
57 49 56 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( abs ` ( ( ( ! ` N ) / _e ) - ( S ` N ) ) ) < ( 1 / N ) )
58 eluzle 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 <_ N )
59 nnre 
 |-  ( N e. NN -> N e. RR )
60 nngt0 
 |-  ( N e. NN -> 0 < N )
61 lerec 
 |-  ( ( ( 2 e. RR /\ 0 < 2 ) /\ ( N e. RR /\ 0 < N ) ) -> ( 2 <_ N <-> ( 1 / N ) <_ ( 1 / 2 ) ) )
62 42 44 61 mpanl12 
 |-  ( ( N e. RR /\ 0 < N ) -> ( 2 <_ N <-> ( 1 / N ) <_ ( 1 / 2 ) ) )
63 59 60 62 syl2anc 
 |-  ( N e. NN -> ( 2 <_ N <-> ( 1 / N ) <_ ( 1 / 2 ) ) )
64 49 63 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 <_ N <-> ( 1 / N ) <_ ( 1 / 2 ) ) )
65 58 64 mpbid 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 / N ) <_ ( 1 / 2 ) )
66 53 54 55 57 65 ltletrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( abs ` ( ( ( ! ` N ) / _e ) - ( S ` N ) ) ) < ( 1 / 2 ) )
67 48 66 jaoi 
 |-  ( ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) -> ( abs ` ( ( ( ! ` N ) / _e ) - ( S ` N ) ) ) < ( 1 / 2 ) )
68 18 67 sylbi 
 |-  ( N e. NN -> ( abs ` ( ( ( ! ` N ) / _e ) - ( S ` N ) ) ) < ( 1 / 2 ) )
69 15 a1i 
 |-  ( N e. NN -> ( 1 / 2 ) e. RR )
70 14 8 69 absdifltd 
 |-  ( N e. NN -> ( ( abs ` ( ( ( ! ` N ) / _e ) - ( S ` N ) ) ) < ( 1 / 2 ) <-> ( ( ( S ` N ) - ( 1 / 2 ) ) < ( ( ! ` N ) / _e ) /\ ( ( ! ` N ) / _e ) < ( ( S ` N ) + ( 1 / 2 ) ) ) ) )
71 68 70 mpbid 
 |-  ( N e. NN -> ( ( ( S ` N ) - ( 1 / 2 ) ) < ( ( ! ` N ) / _e ) /\ ( ( ! ` N ) / _e ) < ( ( S ` N ) + ( 1 / 2 ) ) ) )
72 71 simpld 
 |-  ( N e. NN -> ( ( S ` N ) - ( 1 / 2 ) ) < ( ( ! ` N ) / _e ) )
73 8 69 14 ltsubaddd 
 |-  ( N e. NN -> ( ( ( S ` N ) - ( 1 / 2 ) ) < ( ( ! ` N ) / _e ) <-> ( S ` N ) < ( ( ( ! ` N ) / _e ) + ( 1 / 2 ) ) ) )
74 72 73 mpbid 
 |-  ( N e. NN -> ( S ` N ) < ( ( ( ! ` N ) / _e ) + ( 1 / 2 ) ) )
75 8 17 74 ltled 
 |-  ( N e. NN -> ( S ` N ) <_ ( ( ( ! ` N ) / _e ) + ( 1 / 2 ) ) )
76 readdcl 
 |-  ( ( ( S ` N ) e. RR /\ ( 1 / 2 ) e. RR ) -> ( ( S ` N ) + ( 1 / 2 ) ) e. RR )
77 8 15 76 sylancl 
 |-  ( N e. NN -> ( ( S ` N ) + ( 1 / 2 ) ) e. RR )
78 71 simprd 
 |-  ( N e. NN -> ( ( ! ` N ) / _e ) < ( ( S ` N ) + ( 1 / 2 ) ) )
79 14 77 69 78 ltadd1dd 
 |-  ( N e. NN -> ( ( ( ! ` N ) / _e ) + ( 1 / 2 ) ) < ( ( ( S ` N ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) )
80 8 recnd 
 |-  ( N e. NN -> ( S ` N ) e. CC )
81 69 recnd 
 |-  ( N e. NN -> ( 1 / 2 ) e. CC )
82 80 81 81 addassd 
 |-  ( N e. NN -> ( ( ( S ` N ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( S ` N ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) )
83 ax-1cn 
 |-  1 e. CC
84 2halves 
 |-  ( 1 e. CC -> ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 )
85 83 84 ax-mp 
 |-  ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1
86 85 oveq2i 
 |-  ( ( S ` N ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( S ` N ) + 1 )
87 82 86 eqtrdi 
 |-  ( N e. NN -> ( ( ( S ` N ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( S ` N ) + 1 ) )
88 79 87 breqtrd 
 |-  ( N e. NN -> ( ( ( ! ` N ) / _e ) + ( 1 / 2 ) ) < ( ( S ` N ) + 1 ) )
89 flbi 
 |-  ( ( ( ( ( ! ` N ) / _e ) + ( 1 / 2 ) ) e. RR /\ ( S ` N ) e. ZZ ) -> ( ( |_ ` ( ( ( ! ` N ) / _e ) + ( 1 / 2 ) ) ) = ( S ` N ) <-> ( ( S ` N ) <_ ( ( ( ! ` N ) / _e ) + ( 1 / 2 ) ) /\ ( ( ( ! ` N ) / _e ) + ( 1 / 2 ) ) < ( ( S ` N ) + 1 ) ) ) )
90 17 7 89 syl2anc 
 |-  ( N e. NN -> ( ( |_ ` ( ( ( ! ` N ) / _e ) + ( 1 / 2 ) ) ) = ( S ` N ) <-> ( ( S ` N ) <_ ( ( ( ! ` N ) / _e ) + ( 1 / 2 ) ) /\ ( ( ( ! ` N ) / _e ) + ( 1 / 2 ) ) < ( ( S ` N ) + 1 ) ) ) )
91 75 88 90 mpbir2and 
 |-  ( N e. NN -> ( |_ ` ( ( ( ! ` N ) / _e ) + ( 1 / 2 ) ) ) = ( S ` N ) )
92 91 eqcomd 
 |-  ( N e. NN -> ( S ` N ) = ( |_ ` ( ( ( ! ` N ) / _e ) + ( 1 / 2 ) ) ) )