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 ffvelcdmi ⊢ ( 𝑁 ∈ ℕ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 ) ) ) )