Proof of Theorem subfacval3
| Step | Hyp | Ref
| Expression |
| 1 | | nnnn0 12533 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
| 2 | | derang.d |
. . . . . . . . 9
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)})) |
| 3 | | subfac.n |
. . . . . . . . 9
⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛))) |
| 4 | 2, 3 | subfacf 35180 |
. . . . . . . 8
⊢ 𝑆:ℕ0⟶ℕ0 |
| 5 | 4 | ffvelcdmi 7103 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑆‘𝑁) ∈
ℕ0) |
| 6 | 1, 5 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑆‘𝑁) ∈
ℕ0) |
| 7 | 6 | nn0zd 12639 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝑆‘𝑁) ∈ ℤ) |
| 8 | 7 | zred 12722 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑆‘𝑁) ∈ ℝ) |
| 9 | | faccl 14322 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
| 10 | 1, 9 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(!‘𝑁) ∈
ℕ) |
| 11 | 10 | nnred 12281 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(!‘𝑁) ∈
ℝ) |
| 12 | | epr 16244 |
. . . . . 6
⊢ e ∈
ℝ+ |
| 13 | | rerpdivcl 13065 |
. . . . . 6
⊢
(((!‘𝑁) ∈
ℝ ∧ e ∈ ℝ+) → ((!‘𝑁) / e) ∈ ℝ) |
| 14 | 11, 12, 13 | sylancl 586 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
((!‘𝑁) / e) ∈
ℝ) |
| 15 | | halfre 12480 |
. . . . 5
⊢ (1 / 2)
∈ ℝ |
| 16 | | readdcl 11238 |
. . . . 5
⊢
((((!‘𝑁) / e)
∈ ℝ ∧ (1 / 2) ∈ ℝ) → (((!‘𝑁) / e) + (1 / 2)) ∈
ℝ) |
| 17 | 14, 15, 16 | sylancl 586 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(((!‘𝑁) / e) + (1 /
2)) ∈ ℝ) |
| 18 | | elnn1uz2 12967 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈
(ℤ≥‘2))) |
| 19 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 = 1 → (!‘𝑁) =
(!‘1)) |
| 20 | | fac1 14316 |
. . . . . . . . . . . . . . . 16
⊢
(!‘1) = 1 |
| 21 | 19, 20 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 = 1 → (!‘𝑁) = 1) |
| 22 | 21 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ (𝑁 = 1 → ((!‘𝑁) / e) = (1 /
e)) |
| 23 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 = 1 → (𝑆‘𝑁) = (𝑆‘1)) |
| 24 | 2, 3 | subfac1 35183 |
. . . . . . . . . . . . . . 15
⊢ (𝑆‘1) = 0 |
| 25 | 23, 24 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
⊢ (𝑁 = 1 → (𝑆‘𝑁) = 0) |
| 26 | 22, 25 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ (𝑁 = 1 → (((!‘𝑁) / e) − (𝑆‘𝑁)) = ((1 / e) − 0)) |
| 27 | | rpreccl 13061 |
. . . . . . . . . . . . . . . . 17
⊢ (e ∈
ℝ+ → (1 / e) ∈ ℝ+) |
| 28 | 12, 27 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (1 / e)
∈ ℝ+ |
| 29 | | rpre 13043 |
. . . . . . . . . . . . . . . 16
⊢ ((1 / e)
∈ ℝ+ → (1 / e) ∈ ℝ) |
| 30 | 28, 29 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (1 / e)
∈ ℝ |
| 31 | 30 | recni 11275 |
. . . . . . . . . . . . . 14
⊢ (1 / e)
∈ ℂ |
| 32 | 31 | subid1i 11581 |
. . . . . . . . . . . . 13
⊢ ((1 / e)
− 0) = (1 / e) |
| 33 | 26, 32 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (𝑁 = 1 → (((!‘𝑁) / e) − (𝑆‘𝑁)) = (1 / e)) |
| 34 | 33 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑁 = 1 →
(abs‘(((!‘𝑁) /
e) − (𝑆‘𝑁))) = (abs‘(1 /
e))) |
| 35 | | rpge0 13048 |
. . . . . . . . . . . . 13
⊢ ((1 / e)
∈ ℝ+ → 0 ≤ (1 / e)) |
| 36 | 28, 35 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ 0 ≤ (1
/ e) |
| 37 | | absid 15335 |
. . . . . . . . . . . 12
⊢ (((1 / e)
∈ ℝ ∧ 0 ≤ (1 / e)) → (abs‘(1 / e)) = (1 /
e)) |
| 38 | 30, 36, 37 | mp2an 692 |
. . . . . . . . . . 11
⊢
(abs‘(1 / e)) = (1 / e) |
| 39 | 34, 38 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝑁 = 1 →
(abs‘(((!‘𝑁) /
e) − (𝑆‘𝑁))) = (1 / e)) |
| 40 | | egt2lt3 16242 |
. . . . . . . . . . . 12
⊢ (2 < e
∧ e < 3) |
| 41 | 40 | simpli 483 |
. . . . . . . . . . 11
⊢ 2 <
e |
| 42 | | 2re 12340 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
| 43 | | ere 16125 |
. . . . . . . . . . . 12
⊢ e ∈
ℝ |
| 44 | | 2pos 12369 |
. . . . . . . . . . . 12
⊢ 0 <
2 |
| 45 | | epos 16243 |
. . . . . . . . . . . 12
⊢ 0 <
e |
| 46 | 42, 43, 44, 45 | ltrecii 12184 |
. . . . . . . . . . 11
⊢ (2 < e
↔ (1 / e) < (1 / 2)) |
| 47 | 41, 46 | mpbi 230 |
. . . . . . . . . 10
⊢ (1 / e)
< (1 / 2) |
| 48 | 39, 47 | eqbrtrdi 5182 |
. . . . . . . . 9
⊢ (𝑁 = 1 →
(abs‘(((!‘𝑁) /
e) − (𝑆‘𝑁))) < (1 /
2)) |
| 49 | | eluz2nn 12924 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℕ) |
| 50 | 14, 8 | resubcld 11691 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ →
(((!‘𝑁) / e) −
(𝑆‘𝑁)) ∈ ℝ) |
| 51 | 50 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ →
(((!‘𝑁) / e) −
(𝑆‘𝑁)) ∈ ℂ) |
| 52 | 49, 51 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → (((!‘𝑁) / e) − (𝑆‘𝑁)) ∈ ℂ) |
| 53 | 52 | abscld 15475 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (abs‘(((!‘𝑁) / e) − (𝑆‘𝑁))) ∈ ℝ) |
| 54 | 49 | nnrecred 12317 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (1 / 𝑁) ∈ ℝ) |
| 55 | 15 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (1 / 2) ∈
ℝ) |
| 56 | 2, 3 | subfaclim 35193 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(abs‘(((!‘𝑁) /
e) − (𝑆‘𝑁))) < (1 / 𝑁)) |
| 57 | 49, 56 | syl 17 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (abs‘(((!‘𝑁) / e) − (𝑆‘𝑁))) < (1 / 𝑁)) |
| 58 | | eluzle 12891 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ≤ 𝑁) |
| 59 | | nnre 12273 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
| 60 | | nngt0 12297 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
| 61 | | lerec 12151 |
. . . . . . . . . . . . . 14
⊢ (((2
∈ ℝ ∧ 0 < 2) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (2 ≤ 𝑁 ↔ (1 / 𝑁) ≤ (1 / 2))) |
| 62 | 42, 44, 61 | mpanl12 702 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℝ ∧ 0 <
𝑁) → (2 ≤ 𝑁 ↔ (1 / 𝑁) ≤ (1 / 2))) |
| 63 | 59, 60, 62 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (2 ≤
𝑁 ↔ (1 / 𝑁) ≤ (1 /
2))) |
| 64 | 49, 63 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 ≤ 𝑁 ↔ (1 / 𝑁) ≤ (1 / 2))) |
| 65 | 58, 64 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (1 / 𝑁) ≤ (1 / 2)) |
| 66 | 53, 54, 55, 57, 65 | ltletrd 11421 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → (abs‘(((!‘𝑁) / e) − (𝑆‘𝑁))) < (1 / 2)) |
| 67 | 48, 66 | jaoi 858 |
. . . . . . . 8
⊢ ((𝑁 = 1 ∨ 𝑁 ∈ (ℤ≥‘2))
→ (abs‘(((!‘𝑁) / e) − (𝑆‘𝑁))) < (1 / 2)) |
| 68 | 18, 67 | sylbi 217 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(abs‘(((!‘𝑁) /
e) − (𝑆‘𝑁))) < (1 /
2)) |
| 69 | 15 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (1 / 2)
∈ ℝ) |
| 70 | 14, 8, 69 | absdifltd 15472 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
((abs‘(((!‘𝑁) /
e) − (𝑆‘𝑁))) < (1 / 2) ↔ (((𝑆‘𝑁) − (1 / 2)) < ((!‘𝑁) / e) ∧ ((!‘𝑁) / e) < ((𝑆‘𝑁) + (1 / 2))))) |
| 71 | 68, 70 | mpbid 232 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (((𝑆‘𝑁) − (1 / 2)) < ((!‘𝑁) / e) ∧ ((!‘𝑁) / e) < ((𝑆‘𝑁) + (1 / 2)))) |
| 72 | 71 | simpld 494 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((𝑆‘𝑁) − (1 / 2)) < ((!‘𝑁) / e)) |
| 73 | 8, 69, 14 | ltsubaddd 11859 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((𝑆‘𝑁) − (1 / 2)) < ((!‘𝑁) / e) ↔ (𝑆‘𝑁) < (((!‘𝑁) / e) + (1 / 2)))) |
| 74 | 72, 73 | mpbid 232 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑆‘𝑁) < (((!‘𝑁) / e) + (1 / 2))) |
| 75 | 8, 17, 74 | ltled 11409 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝑆‘𝑁) ≤ (((!‘𝑁) / e) + (1 / 2))) |
| 76 | | readdcl 11238 |
. . . . . 6
⊢ (((𝑆‘𝑁) ∈ ℝ ∧ (1 / 2) ∈
ℝ) → ((𝑆‘𝑁) + (1 / 2)) ∈
ℝ) |
| 77 | 8, 15, 76 | sylancl 586 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((𝑆‘𝑁) + (1 / 2)) ∈
ℝ) |
| 78 | 71 | simprd 495 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
((!‘𝑁) / e) <
((𝑆‘𝑁) + (1 / 2))) |
| 79 | 14, 77, 69, 78 | ltadd1dd 11874 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(((!‘𝑁) / e) + (1 /
2)) < (((𝑆‘𝑁) + (1 / 2)) + (1 /
2))) |
| 80 | 8 | recnd 11289 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑆‘𝑁) ∈ ℂ) |
| 81 | 69 | recnd 11289 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (1 / 2)
∈ ℂ) |
| 82 | 80, 81, 81 | addassd 11283 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((𝑆‘𝑁) + (1 / 2)) + (1 / 2)) = ((𝑆‘𝑁) + ((1 / 2) + (1 / 2)))) |
| 83 | | ax-1cn 11213 |
. . . . . . 7
⊢ 1 ∈
ℂ |
| 84 | | 2halves 12494 |
. . . . . . 7
⊢ (1 ∈
ℂ → ((1 / 2) + (1 / 2)) = 1) |
| 85 | 83, 84 | ax-mp 5 |
. . . . . 6
⊢ ((1 / 2)
+ (1 / 2)) = 1 |
| 86 | 85 | oveq2i 7442 |
. . . . 5
⊢ ((𝑆‘𝑁) + ((1 / 2) + (1 / 2))) = ((𝑆‘𝑁) + 1) |
| 87 | 82, 86 | eqtrdi 2793 |
. . . 4
⊢ (𝑁 ∈ ℕ → (((𝑆‘𝑁) + (1 / 2)) + (1 / 2)) = ((𝑆‘𝑁) + 1)) |
| 88 | 79, 87 | breqtrd 5169 |
. . 3
⊢ (𝑁 ∈ ℕ →
(((!‘𝑁) / e) + (1 /
2)) < ((𝑆‘𝑁) + 1)) |
| 89 | | flbi 13856 |
. . . 4
⊢
(((((!‘𝑁) / e)
+ (1 / 2)) ∈ ℝ ∧ (𝑆‘𝑁) ∈ ℤ) →
((⌊‘(((!‘𝑁) / e) + (1 / 2))) = (𝑆‘𝑁) ↔ ((𝑆‘𝑁) ≤ (((!‘𝑁) / e) + (1 / 2)) ∧ (((!‘𝑁) / e) + (1 / 2)) < ((𝑆‘𝑁) + 1)))) |
| 90 | 17, 7, 89 | syl2anc 584 |
. . 3
⊢ (𝑁 ∈ ℕ →
((⌊‘(((!‘𝑁) / e) + (1 / 2))) = (𝑆‘𝑁) ↔ ((𝑆‘𝑁) ≤ (((!‘𝑁) / e) + (1 / 2)) ∧ (((!‘𝑁) / e) + (1 / 2)) < ((𝑆‘𝑁) + 1)))) |
| 91 | 75, 88, 90 | mpbir2and 713 |
. 2
⊢ (𝑁 ∈ ℕ →
(⌊‘(((!‘𝑁) / e) + (1 / 2))) = (𝑆‘𝑁)) |
| 92 | 91 | eqcomd 2743 |
1
⊢ (𝑁 ∈ ℕ → (𝑆‘𝑁) = (⌊‘(((!‘𝑁) / e) + (1 /
2)))) |