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 Fin f | f : x 1-1 onto x y x f y y
subfac.n S = n 0 D 1 n
Assertion subfacval3 N S N = N ! e + 1 2

Proof

Step Hyp Ref Expression
1 derang.d D = x Fin f | f : x 1-1 onto x y x f y y
2 subfac.n S = n 0 D 1 n
3 nnnn0 N N 0
4 1 2 subfacf S : 0 0
5 4 ffvelrni N 0 S N 0
6 3 5 syl N S N 0
7 6 nn0zd N S N
8 7 zred N S N
9 faccl N 0 N !
10 3 9 syl N N !
11 10 nnred N N !
12 epr e +
13 rerpdivcl N ! e + N ! e
14 11 12 13 sylancl N N ! e
15 halfre 1 2
16 readdcl N ! e 1 2 N ! e + 1 2
17 14 15 16 sylancl N N ! e + 1 2
18 elnn1uz2 N N = 1 N 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 + 1 e +
28 12 27 ax-mp 1 e +
29 rpre 1 e + 1 e
30 28 29 ax-mp 1 e
31 30 recni 1 e
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 N ! e S N = 1 e
35 rpge0 1 e + 0 1 e
36 28 35 ax-mp 0 1 e
37 absid 1 e 0 1 e 1 e = 1 e
38 30 36 37 mp2an 1 e = 1 e
39 34 38 eqtrdi N = 1 N ! e S N = 1 e
40 egt2lt3 2 < e e < 3
41 40 simpli 2 < e
42 2re 2
43 ere e
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 N ! e S N < 1 2
49 eluz2nn N 2 N
50 14 8 resubcld N N ! e S N
51 50 recnd N N ! e S N
52 49 51 syl N 2 N ! e S N
53 52 abscld N 2 N ! e S N
54 49 nnrecred N 2 1 N
55 15 a1i N 2 1 2
56 1 2 subfaclim N N ! e S N < 1 N
57 49 56 syl N 2 N ! e S N < 1 N
58 eluzle N 2 2 N
59 nnre N N
60 nngt0 N 0 < N
61 lerec 2 0 < 2 N 0 < N 2 N 1 N 1 2
62 42 44 61 mpanl12 N 0 < N 2 N 1 N 1 2
63 59 60 62 syl2anc N 2 N 1 N 1 2
64 49 63 syl N 2 2 N 1 N 1 2
65 58 64 mpbid N 2 1 N 1 2
66 53 54 55 57 65 ltletrd N 2 N ! e S N < 1 2
67 48 66 jaoi N = 1 N 2 N ! e S N < 1 2
68 18 67 sylbi N N ! e S N < 1 2
69 15 a1i N 1 2
70 14 8 69 absdifltd N N ! e S N < 1 2 S N 1 2 < N ! e N ! e < S N + 1 2
71 68 70 mpbid N S N 1 2 < N ! e N ! e < S N + 1 2
72 71 simpld N S N 1 2 < N ! e
73 8 69 14 ltsubaddd N S N 1 2 < N ! e S N < N ! e + 1 2
74 72 73 mpbid N S N < N ! e + 1 2
75 8 17 74 ltled N S N N ! e + 1 2
76 readdcl S N 1 2 S N + 1 2
77 8 15 76 sylancl N S N + 1 2
78 71 simprd N N ! e < S N + 1 2
79 14 77 69 78 ltadd1dd N N ! e + 1 2 < S N + 1 2 + 1 2
80 8 recnd N S N
81 69 recnd N 1 2
82 80 81 81 addassd N S N + 1 2 + 1 2 = S N + 1 2 + 1 2
83 ax-1cn 1
84 2halves 1 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 S N + 1 2 + 1 2 = S N + 1
88 79 87 breqtrd N N ! e + 1 2 < S N + 1
89 flbi N ! e + 1 2 S N 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 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 N ! e + 1 2 = S N
92 91 eqcomd N S N = N ! e + 1 2