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 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥1-1-onto𝑥 ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) ≠ 𝑦 ) } ) )
subfac.n 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) )
Assertion subfacval3 ( 𝑁 ∈ ℕ → ( 𝑆𝑁 ) = ( ⌊ ‘ ( ( ( ! ‘ 𝑁 ) / e ) + ( 1 / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 derang.d 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥1-1-onto𝑥 ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) ≠ 𝑦 ) } ) )
2 subfac.n 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) )
3 nnnn0 ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
4 1 2 subfacf 𝑆 : ℕ0 ⟶ ℕ0
5 4 ffvelrni ( 𝑁 ∈ ℕ0 → ( 𝑆𝑁 ) ∈ ℕ0 )
6 3 5 syl ( 𝑁 ∈ ℕ → ( 𝑆𝑁 ) ∈ ℕ0 )
7 6 nn0zd ( 𝑁 ∈ ℕ → ( 𝑆𝑁 ) ∈ ℤ )
8 7 zred ( 𝑁 ∈ ℕ → ( 𝑆𝑁 ) ∈ ℝ )
9 faccl ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ )
10 3 9 syl ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) ∈ ℕ )
11 10 nnred ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) ∈ ℝ )
12 epr e ∈ ℝ+
13 rerpdivcl ( ( ( ! ‘ 𝑁 ) ∈ ℝ ∧ e ∈ ℝ+ ) → ( ( ! ‘ 𝑁 ) / e ) ∈ ℝ )
14 11 12 13 sylancl ( 𝑁 ∈ ℕ → ( ( ! ‘ 𝑁 ) / e ) ∈ ℝ )
15 halfre ( 1 / 2 ) ∈ ℝ
16 readdcl ( ( ( ( ! ‘ 𝑁 ) / e ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( ( ( ! ‘ 𝑁 ) / e ) + ( 1 / 2 ) ) ∈ ℝ )
17 14 15 16 sylancl ( 𝑁 ∈ ℕ → ( ( ( ! ‘ 𝑁 ) / e ) + ( 1 / 2 ) ) ∈ ℝ )
18 elnn1uz2 ( 𝑁 ∈ ℕ ↔ ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ ‘ 2 ) ) )
19 fveq2 ( 𝑁 = 1 → ( ! ‘ 𝑁 ) = ( ! ‘ 1 ) )
20 fac1 ( ! ‘ 1 ) = 1
21 19 20 eqtrdi ( 𝑁 = 1 → ( ! ‘ 𝑁 ) = 1 )
22 21 oveq1d ( 𝑁 = 1 → ( ( ! ‘ 𝑁 ) / e ) = ( 1 / e ) )
23 fveq2 ( 𝑁 = 1 → ( 𝑆𝑁 ) = ( 𝑆 ‘ 1 ) )
24 1 2 subfac1 ( 𝑆 ‘ 1 ) = 0
25 23 24 eqtrdi ( 𝑁 = 1 → ( 𝑆𝑁 ) = 0 )
26 22 25 oveq12d ( 𝑁 = 1 → ( ( ( ! ‘ 𝑁 ) / e ) − ( 𝑆𝑁 ) ) = ( ( 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 ( 𝑁 = 1 → ( ( ( ! ‘ 𝑁 ) / e ) − ( 𝑆𝑁 ) ) = ( 1 / e ) )
34 33 fveq2d ( 𝑁 = 1 → ( abs ‘ ( ( ( ! ‘ 𝑁 ) / e ) − ( 𝑆𝑁 ) ) ) = ( abs ‘ ( 1 / e ) ) )
35 rpge0 ( ( 1 / e ) ∈ ℝ+ → 0 ≤ ( 1 / e ) )
36 28 35 ax-mp 0 ≤ ( 1 / e )
37 absid ( ( ( 1 / e ) ∈ ℝ ∧ 0 ≤ ( 1 / e ) ) → ( abs ‘ ( 1 / e ) ) = ( 1 / e ) )
38 30 36 37 mp2an ( abs ‘ ( 1 / e ) ) = ( 1 / e )
39 34 38 eqtrdi ( 𝑁 = 1 → ( abs ‘ ( ( ( ! ‘ 𝑁 ) / e ) − ( 𝑆𝑁 ) ) ) = ( 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 ( 𝑁 = 1 → ( abs ‘ ( ( ( ! ‘ 𝑁 ) / e ) − ( 𝑆𝑁 ) ) ) < ( 1 / 2 ) )
49 eluz2nn ( 𝑁 ∈ ( ℤ ‘ 2 ) → 𝑁 ∈ ℕ )
50 14 8 resubcld ( 𝑁 ∈ ℕ → ( ( ( ! ‘ 𝑁 ) / e ) − ( 𝑆𝑁 ) ) ∈ ℝ )
51 50 recnd ( 𝑁 ∈ ℕ → ( ( ( ! ‘ 𝑁 ) / e ) − ( 𝑆𝑁 ) ) ∈ ℂ )
52 49 51 syl ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( ( ( ! ‘ 𝑁 ) / e ) − ( 𝑆𝑁 ) ) ∈ ℂ )
53 52 abscld ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( abs ‘ ( ( ( ! ‘ 𝑁 ) / e ) − ( 𝑆𝑁 ) ) ) ∈ ℝ )
54 49 nnrecred ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 1 / 𝑁 ) ∈ ℝ )
55 15 a1i ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 1 / 2 ) ∈ ℝ )
56 1 2 subfaclim ( 𝑁 ∈ ℕ → ( abs ‘ ( ( ( ! ‘ 𝑁 ) / e ) − ( 𝑆𝑁 ) ) ) < ( 1 / 𝑁 ) )
57 49 56 syl ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( abs ‘ ( ( ( ! ‘ 𝑁 ) / e ) − ( 𝑆𝑁 ) ) ) < ( 1 / 𝑁 ) )
58 eluzle ( 𝑁 ∈ ( ℤ ‘ 2 ) → 2 ≤ 𝑁 )
59 nnre ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
60 nngt0 ( 𝑁 ∈ ℕ → 0 < 𝑁 )
61 lerec ( ( ( 2 ∈ ℝ ∧ 0 < 2 ) ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( 2 ≤ 𝑁 ↔ ( 1 / 𝑁 ) ≤ ( 1 / 2 ) ) )
62 42 44 61 mpanl12 ( ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) → ( 2 ≤ 𝑁 ↔ ( 1 / 𝑁 ) ≤ ( 1 / 2 ) ) )
63 59 60 62 syl2anc ( 𝑁 ∈ ℕ → ( 2 ≤ 𝑁 ↔ ( 1 / 𝑁 ) ≤ ( 1 / 2 ) ) )
64 49 63 syl ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 2 ≤ 𝑁 ↔ ( 1 / 𝑁 ) ≤ ( 1 / 2 ) ) )
65 58 64 mpbid ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 1 / 𝑁 ) ≤ ( 1 / 2 ) )
66 53 54 55 57 65 ltletrd ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( abs ‘ ( ( ( ! ‘ 𝑁 ) / e ) − ( 𝑆𝑁 ) ) ) < ( 1 / 2 ) )
67 48 66 jaoi ( ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ ‘ 2 ) ) → ( abs ‘ ( ( ( ! ‘ 𝑁 ) / e ) − ( 𝑆𝑁 ) ) ) < ( 1 / 2 ) )
68 18 67 sylbi ( 𝑁 ∈ ℕ → ( abs ‘ ( ( ( ! ‘ 𝑁 ) / e ) − ( 𝑆𝑁 ) ) ) < ( 1 / 2 ) )
69 15 a1i ( 𝑁 ∈ ℕ → ( 1 / 2 ) ∈ ℝ )
70 14 8 69 absdifltd ( 𝑁 ∈ ℕ → ( ( abs ‘ ( ( ( ! ‘ 𝑁 ) / e ) − ( 𝑆𝑁 ) ) ) < ( 1 / 2 ) ↔ ( ( ( 𝑆𝑁 ) − ( 1 / 2 ) ) < ( ( ! ‘ 𝑁 ) / e ) ∧ ( ( ! ‘ 𝑁 ) / e ) < ( ( 𝑆𝑁 ) + ( 1 / 2 ) ) ) ) )
71 68 70 mpbid ( 𝑁 ∈ ℕ → ( ( ( 𝑆𝑁 ) − ( 1 / 2 ) ) < ( ( ! ‘ 𝑁 ) / e ) ∧ ( ( ! ‘ 𝑁 ) / e ) < ( ( 𝑆𝑁 ) + ( 1 / 2 ) ) ) )
72 71 simpld ( 𝑁 ∈ ℕ → ( ( 𝑆𝑁 ) − ( 1 / 2 ) ) < ( ( ! ‘ 𝑁 ) / e ) )
73 8 69 14 ltsubaddd ( 𝑁 ∈ ℕ → ( ( ( 𝑆𝑁 ) − ( 1 / 2 ) ) < ( ( ! ‘ 𝑁 ) / e ) ↔ ( 𝑆𝑁 ) < ( ( ( ! ‘ 𝑁 ) / e ) + ( 1 / 2 ) ) ) )
74 72 73 mpbid ( 𝑁 ∈ ℕ → ( 𝑆𝑁 ) < ( ( ( ! ‘ 𝑁 ) / e ) + ( 1 / 2 ) ) )
75 8 17 74 ltled ( 𝑁 ∈ ℕ → ( 𝑆𝑁 ) ≤ ( ( ( ! ‘ 𝑁 ) / e ) + ( 1 / 2 ) ) )
76 readdcl ( ( ( 𝑆𝑁 ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( ( 𝑆𝑁 ) + ( 1 / 2 ) ) ∈ ℝ )
77 8 15 76 sylancl ( 𝑁 ∈ ℕ → ( ( 𝑆𝑁 ) + ( 1 / 2 ) ) ∈ ℝ )
78 71 simprd ( 𝑁 ∈ ℕ → ( ( ! ‘ 𝑁 ) / e ) < ( ( 𝑆𝑁 ) + ( 1 / 2 ) ) )
79 14 77 69 78 ltadd1dd ( 𝑁 ∈ ℕ → ( ( ( ! ‘ 𝑁 ) / e ) + ( 1 / 2 ) ) < ( ( ( 𝑆𝑁 ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) )
80 8 recnd ( 𝑁 ∈ ℕ → ( 𝑆𝑁 ) ∈ ℂ )
81 69 recnd ( 𝑁 ∈ ℕ → ( 1 / 2 ) ∈ ℂ )
82 80 81 81 addassd ( 𝑁 ∈ ℕ → ( ( ( 𝑆𝑁 ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( 𝑆𝑁 ) + ( ( 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 ( ( 𝑆𝑁 ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( 𝑆𝑁 ) + 1 )
87 82 86 eqtrdi ( 𝑁 ∈ ℕ → ( ( ( 𝑆𝑁 ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( 𝑆𝑁 ) + 1 ) )
88 79 87 breqtrd ( 𝑁 ∈ ℕ → ( ( ( ! ‘ 𝑁 ) / e ) + ( 1 / 2 ) ) < ( ( 𝑆𝑁 ) + 1 ) )
89 flbi ( ( ( ( ( ! ‘ 𝑁 ) / e ) + ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑆𝑁 ) ∈ ℤ ) → ( ( ⌊ ‘ ( ( ( ! ‘ 𝑁 ) / e ) + ( 1 / 2 ) ) ) = ( 𝑆𝑁 ) ↔ ( ( 𝑆𝑁 ) ≤ ( ( ( ! ‘ 𝑁 ) / e ) + ( 1 / 2 ) ) ∧ ( ( ( ! ‘ 𝑁 ) / e ) + ( 1 / 2 ) ) < ( ( 𝑆𝑁 ) + 1 ) ) ) )
90 17 7 89 syl2anc ( 𝑁 ∈ ℕ → ( ( ⌊ ‘ ( ( ( ! ‘ 𝑁 ) / e ) + ( 1 / 2 ) ) ) = ( 𝑆𝑁 ) ↔ ( ( 𝑆𝑁 ) ≤ ( ( ( ! ‘ 𝑁 ) / e ) + ( 1 / 2 ) ) ∧ ( ( ( ! ‘ 𝑁 ) / e ) + ( 1 / 2 ) ) < ( ( 𝑆𝑁 ) + 1 ) ) ) )
91 75 88 90 mpbir2and ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( ( ( ! ‘ 𝑁 ) / e ) + ( 1 / 2 ) ) ) = ( 𝑆𝑁 ) )
92 91 eqcomd ( 𝑁 ∈ ℕ → ( 𝑆𝑁 ) = ( ⌊ ‘ ( ( ( ! ‘ 𝑁 ) / e ) + ( 1 / 2 ) ) ) )