Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  subfacval3 Structured version   Visualization version   GIF version

Theorem subfacval3 35030
Description: Another closed form expression for the subfactorial. The expression ⌊‘(𝑥 + 1 / 2) is a way of saying "rounded to the nearest integer". (Contributed by Mario Carneiro, 23-Jan-2015.)
Hypotheses
Ref Expression
derang.d 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥1-1-onto𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) ≠ 𝑦)}))
subfac.n 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))
Assertion
Ref Expression
subfacval3 (𝑁 ∈ ℕ → (𝑆𝑁) = (⌊‘(((!‘𝑁) / e) + (1 / 2))))
Distinct variable groups:   𝑓,𝑛,𝑥,𝑦,𝑁   𝐷,𝑛   𝑆,𝑛,𝑥,𝑦
Allowed substitution hints:   𝐷(𝑥,𝑦,𝑓)   𝑆(𝑓)

Proof of Theorem subfacval3
StepHypRef Expression
1 nnnn0 12525 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
2 derang.d . . . . . . . . 9 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥1-1-onto𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) ≠ 𝑦)}))
3 subfac.n . . . . . . . . 9 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))
42, 3subfacf 35016 . . . . . . . 8 𝑆:ℕ0⟶ℕ0
54ffvelcdmi 7089 . . . . . . 7 (𝑁 ∈ ℕ0 → (𝑆𝑁) ∈ ℕ0)
61, 5syl 17 . . . . . 6 (𝑁 ∈ ℕ → (𝑆𝑁) ∈ ℕ0)
76nn0zd 12630 . . . . 5 (𝑁 ∈ ℕ → (𝑆𝑁) ∈ ℤ)
87zred 12712 . . . 4 (𝑁 ∈ ℕ → (𝑆𝑁) ∈ ℝ)
9 faccl 14295 . . . . . . . 8 (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
101, 9syl 17 . . . . . . 7 (𝑁 ∈ ℕ → (!‘𝑁) ∈ ℕ)
1110nnred 12273 . . . . . 6 (𝑁 ∈ ℕ → (!‘𝑁) ∈ ℝ)
12 epr 16205 . . . . . 6 e ∈ ℝ+
13 rerpdivcl 13052 . . . . . 6 (((!‘𝑁) ∈ ℝ ∧ e ∈ ℝ+) → ((!‘𝑁) / e) ∈ ℝ)
1411, 12, 13sylancl 584 . . . . 5 (𝑁 ∈ ℕ → ((!‘𝑁) / e) ∈ ℝ)
15 halfre 12472 . . . . 5 (1 / 2) ∈ ℝ
16 readdcl 11232 . . . . 5 ((((!‘𝑁) / e) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (((!‘𝑁) / e) + (1 / 2)) ∈ ℝ)
1714, 15, 16sylancl 584 . . . 4 (𝑁 ∈ ℕ → (((!‘𝑁) / e) + (1 / 2)) ∈ ℝ)
18 elnn1uz2 12955 . . . . . . . 8 (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈ (ℤ‘2)))
19 fveq2 6893 . . . . . . . . . . . . . . . 16 (𝑁 = 1 → (!‘𝑁) = (!‘1))
20 fac1 14289 . . . . . . . . . . . . . . . 16 (!‘1) = 1
2119, 20eqtrdi 2782 . . . . . . . . . . . . . . 15 (𝑁 = 1 → (!‘𝑁) = 1)
2221oveq1d 7431 . . . . . . . . . . . . . 14 (𝑁 = 1 → ((!‘𝑁) / e) = (1 / e))
23 fveq2 6893 . . . . . . . . . . . . . . 15 (𝑁 = 1 → (𝑆𝑁) = (𝑆‘1))
242, 3subfac1 35019 . . . . . . . . . . . . . . 15 (𝑆‘1) = 0
2523, 24eqtrdi 2782 . . . . . . . . . . . . . 14 (𝑁 = 1 → (𝑆𝑁) = 0)
2622, 25oveq12d 7434 . . . . . . . . . . . . 13 (𝑁 = 1 → (((!‘𝑁) / e) − (𝑆𝑁)) = ((1 / e) − 0))
27 rpreccl 13048 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → (1 / e) ∈ ℝ+)
2812, 27ax-mp 5 . . . . . . . . . . . . . . . 16 (1 / e) ∈ ℝ+
29 rpre 13030 . . . . . . . . . . . . . . . 16 ((1 / e) ∈ ℝ+ → (1 / e) ∈ ℝ)
3028, 29ax-mp 5 . . . . . . . . . . . . . . 15 (1 / e) ∈ ℝ
3130recni 11269 . . . . . . . . . . . . . 14 (1 / e) ∈ ℂ
3231subid1i 11573 . . . . . . . . . . . . 13 ((1 / e) − 0) = (1 / e)
3326, 32eqtrdi 2782 . . . . . . . . . . . 12 (𝑁 = 1 → (((!‘𝑁) / e) − (𝑆𝑁)) = (1 / e))
3433fveq2d 6897 . . . . . . . . . . 11 (𝑁 = 1 → (abs‘(((!‘𝑁) / e) − (𝑆𝑁))) = (abs‘(1 / e)))
35 rpge0 13035 . . . . . . . . . . . . 13 ((1 / e) ∈ ℝ+ → 0 ≤ (1 / e))
3628, 35ax-mp 5 . . . . . . . . . . . 12 0 ≤ (1 / e)
37 absid 15296 . . . . . . . . . . . 12 (((1 / e) ∈ ℝ ∧ 0 ≤ (1 / e)) → (abs‘(1 / e)) = (1 / e))
3830, 36, 37mp2an 690 . . . . . . . . . . 11 (abs‘(1 / e)) = (1 / e)
3934, 38eqtrdi 2782 . . . . . . . . . 10 (𝑁 = 1 → (abs‘(((!‘𝑁) / e) − (𝑆𝑁))) = (1 / e))
40 egt2lt3 16203 . . . . . . . . . . . 12 (2 < e ∧ e < 3)
4140simpli 482 . . . . . . . . . . 11 2 < e
42 2re 12332 . . . . . . . . . . . 12 2 ∈ ℝ
43 ere 16086 . . . . . . . . . . . 12 e ∈ ℝ
44 2pos 12361 . . . . . . . . . . . 12 0 < 2
45 epos 16204 . . . . . . . . . . . 12 0 < e
4642, 43, 44, 45ltrecii 12176 . . . . . . . . . . 11 (2 < e ↔ (1 / e) < (1 / 2))
4741, 46mpbi 229 . . . . . . . . . 10 (1 / e) < (1 / 2)
4839, 47eqbrtrdi 5184 . . . . . . . . 9 (𝑁 = 1 → (abs‘(((!‘𝑁) / e) − (𝑆𝑁))) < (1 / 2))
49 eluz2nn 12914 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘2) → 𝑁 ∈ ℕ)
5014, 8resubcld 11683 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (((!‘𝑁) / e) − (𝑆𝑁)) ∈ ℝ)
5150recnd 11283 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (((!‘𝑁) / e) − (𝑆𝑁)) ∈ ℂ)
5249, 51syl 17 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘2) → (((!‘𝑁) / e) − (𝑆𝑁)) ∈ ℂ)
5352abscld 15436 . . . . . . . . . 10 (𝑁 ∈ (ℤ‘2) → (abs‘(((!‘𝑁) / e) − (𝑆𝑁))) ∈ ℝ)
5449nnrecred 12309 . . . . . . . . . 10 (𝑁 ∈ (ℤ‘2) → (1 / 𝑁) ∈ ℝ)
5515a1i 11 . . . . . . . . . 10 (𝑁 ∈ (ℤ‘2) → (1 / 2) ∈ ℝ)
562, 3subfaclim 35029 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (abs‘(((!‘𝑁) / e) − (𝑆𝑁))) < (1 / 𝑁))
5749, 56syl 17 . . . . . . . . . 10 (𝑁 ∈ (ℤ‘2) → (abs‘(((!‘𝑁) / e) − (𝑆𝑁))) < (1 / 𝑁))
58 eluzle 12881 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘2) → 2 ≤ 𝑁)
59 nnre 12265 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
60 nngt0 12289 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 0 < 𝑁)
61 lerec 12143 . . . . . . . . . . . . . 14 (((2 ∈ ℝ ∧ 0 < 2) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (2 ≤ 𝑁 ↔ (1 / 𝑁) ≤ (1 / 2)))
6242, 44, 61mpanl12 700 . . . . . . . . . . . . 13 ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → (2 ≤ 𝑁 ↔ (1 / 𝑁) ≤ (1 / 2)))
6359, 60, 62syl2anc 582 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (2 ≤ 𝑁 ↔ (1 / 𝑁) ≤ (1 / 2)))
6449, 63syl 17 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘2) → (2 ≤ 𝑁 ↔ (1 / 𝑁) ≤ (1 / 2)))
6558, 64mpbid 231 . . . . . . . . . 10 (𝑁 ∈ (ℤ‘2) → (1 / 𝑁) ≤ (1 / 2))
6653, 54, 55, 57, 65ltletrd 11415 . . . . . . . . 9 (𝑁 ∈ (ℤ‘2) → (abs‘(((!‘𝑁) / e) − (𝑆𝑁))) < (1 / 2))
6748, 66jaoi 855 . . . . . . . 8 ((𝑁 = 1 ∨ 𝑁 ∈ (ℤ‘2)) → (abs‘(((!‘𝑁) / e) − (𝑆𝑁))) < (1 / 2))
6818, 67sylbi 216 . . . . . . 7 (𝑁 ∈ ℕ → (abs‘(((!‘𝑁) / e) − (𝑆𝑁))) < (1 / 2))
6915a1i 11 . . . . . . . 8 (𝑁 ∈ ℕ → (1 / 2) ∈ ℝ)
7014, 8, 69absdifltd 15433 . . . . . . 7 (𝑁 ∈ ℕ → ((abs‘(((!‘𝑁) / e) − (𝑆𝑁))) < (1 / 2) ↔ (((𝑆𝑁) − (1 / 2)) < ((!‘𝑁) / e) ∧ ((!‘𝑁) / e) < ((𝑆𝑁) + (1 / 2)))))
7168, 70mpbid 231 . . . . . 6 (𝑁 ∈ ℕ → (((𝑆𝑁) − (1 / 2)) < ((!‘𝑁) / e) ∧ ((!‘𝑁) / e) < ((𝑆𝑁) + (1 / 2))))
7271simpld 493 . . . . 5 (𝑁 ∈ ℕ → ((𝑆𝑁) − (1 / 2)) < ((!‘𝑁) / e))
738, 69, 14ltsubaddd 11851 . . . . 5 (𝑁 ∈ ℕ → (((𝑆𝑁) − (1 / 2)) < ((!‘𝑁) / e) ↔ (𝑆𝑁) < (((!‘𝑁) / e) + (1 / 2))))
7472, 73mpbid 231 . . . 4 (𝑁 ∈ ℕ → (𝑆𝑁) < (((!‘𝑁) / e) + (1 / 2)))
758, 17, 74ltled 11403 . . 3 (𝑁 ∈ ℕ → (𝑆𝑁) ≤ (((!‘𝑁) / e) + (1 / 2)))
76 readdcl 11232 . . . . . 6 (((𝑆𝑁) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → ((𝑆𝑁) + (1 / 2)) ∈ ℝ)
778, 15, 76sylancl 584 . . . . 5 (𝑁 ∈ ℕ → ((𝑆𝑁) + (1 / 2)) ∈ ℝ)
7871simprd 494 . . . . 5 (𝑁 ∈ ℕ → ((!‘𝑁) / e) < ((𝑆𝑁) + (1 / 2)))
7914, 77, 69, 78ltadd1dd 11866 . . . 4 (𝑁 ∈ ℕ → (((!‘𝑁) / e) + (1 / 2)) < (((𝑆𝑁) + (1 / 2)) + (1 / 2)))
808recnd 11283 . . . . . 6 (𝑁 ∈ ℕ → (𝑆𝑁) ∈ ℂ)
8169recnd 11283 . . . . . 6 (𝑁 ∈ ℕ → (1 / 2) ∈ ℂ)
8280, 81, 81addassd 11277 . . . . 5 (𝑁 ∈ ℕ → (((𝑆𝑁) + (1 / 2)) + (1 / 2)) = ((𝑆𝑁) + ((1 / 2) + (1 / 2))))
83 ax-1cn 11207 . . . . . . 7 1 ∈ ℂ
84 2halves 12486 . . . . . . 7 (1 ∈ ℂ → ((1 / 2) + (1 / 2)) = 1)
8583, 84ax-mp 5 . . . . . 6 ((1 / 2) + (1 / 2)) = 1
8685oveq2i 7427 . . . . 5 ((𝑆𝑁) + ((1 / 2) + (1 / 2))) = ((𝑆𝑁) + 1)
8782, 86eqtrdi 2782 . . . 4 (𝑁 ∈ ℕ → (((𝑆𝑁) + (1 / 2)) + (1 / 2)) = ((𝑆𝑁) + 1))
8879, 87breqtrd 5171 . . 3 (𝑁 ∈ ℕ → (((!‘𝑁) / e) + (1 / 2)) < ((𝑆𝑁) + 1))
89 flbi 13830 . . . 4 (((((!‘𝑁) / e) + (1 / 2)) ∈ ℝ ∧ (𝑆𝑁) ∈ ℤ) → ((⌊‘(((!‘𝑁) / e) + (1 / 2))) = (𝑆𝑁) ↔ ((𝑆𝑁) ≤ (((!‘𝑁) / e) + (1 / 2)) ∧ (((!‘𝑁) / e) + (1 / 2)) < ((𝑆𝑁) + 1))))
9017, 7, 89syl2anc 582 . . 3 (𝑁 ∈ ℕ → ((⌊‘(((!‘𝑁) / e) + (1 / 2))) = (𝑆𝑁) ↔ ((𝑆𝑁) ≤ (((!‘𝑁) / e) + (1 / 2)) ∧ (((!‘𝑁) / e) + (1 / 2)) < ((𝑆𝑁) + 1))))
9175, 88, 90mpbir2and 711 . 2 (𝑁 ∈ ℕ → (⌊‘(((!‘𝑁) / e) + (1 / 2))) = (𝑆𝑁))
9291eqcomd 2732 1 (𝑁 ∈ ℕ → (𝑆𝑁) = (⌊‘(((!‘𝑁) / e) + (1 / 2))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wo 845   = wceq 1534  wcel 2099  {cab 2703  wne 2930  wral 3051   class class class wbr 5145  cmpt 5228  1-1-ontowf1o 6545  cfv 6546  (class class class)co 7416  Fincfn 8966  cc 11147  cr 11148  0cc0 11149  1c1 11150   + caddc 11152   < clt 11289  cle 11290  cmin 11485   / cdiv 11912  cn 12258  2c2 12313  3c3 12314  0cn0 12518  cz 12604  cuz 12868  +crp 13022  ...cfz 13532  cfl 13804  !cfa 14285  chash 14342  abscabs 15234  eceu 16059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7738  ax-inf2 9677  ax-cnex 11205  ax-resscn 11206  ax-1cn 11207  ax-icn 11208  ax-addcl 11209  ax-addrcl 11210  ax-mulcl 11211  ax-mulrcl 11212  ax-mulcom 11213  ax-addass 11214  ax-mulass 11215  ax-distr 11216  ax-i2m1 11217  ax-1ne0 11218  ax-1rid 11219  ax-rnegex 11220  ax-rrecex 11221  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224  ax-pre-ltadd 11225  ax-pre-mulgt0 11226  ax-pre-sup 11227
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-int 4947  df-iun 4995  df-br 5146  df-opab 5208  df-mpt 5229  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-se 5630  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-pred 6304  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-isom 6555  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7869  df-1st 7995  df-2nd 7996  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-1o 8488  df-2o 8489  df-oadd 8492  df-er 8726  df-map 8849  df-pm 8850  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-sup 9478  df-inf 9479  df-oi 9546  df-dju 9937  df-card 9975  df-pnf 11291  df-mnf 11292  df-xr 11293  df-ltxr 11294  df-le 11295  df-sub 11487  df-neg 11488  df-div 11913  df-nn 12259  df-2 12321  df-3 12322  df-4 12323  df-n0 12519  df-xnn0 12591  df-z 12605  df-uz 12869  df-q 12979  df-rp 13023  df-ico 13378  df-fz 13533  df-fzo 13676  df-fl 13806  df-seq 14016  df-exp 14076  df-fac 14286  df-bc 14315  df-hash 14343  df-shft 15067  df-cj 15099  df-re 15100  df-im 15101  df-sqrt 15235  df-abs 15236  df-limsup 15468  df-clim 15485  df-rlim 15486  df-sum 15686  df-ef 16064  df-e 16065
This theorem is referenced by:  derangfmla  35031
  Copyright terms: Public domain W3C validator