Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stirlinglem12 Structured version   Visualization version   GIF version

Theorem stirlinglem12 39630
 Description: The sequence 𝐵 is bounded below. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
Hypotheses
Ref Expression
stirlinglem12.1 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))
stirlinglem12.2 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴𝑛)))
stirlinglem12.3 𝐹 = (𝑛 ∈ ℕ ↦ (1 / (𝑛 · (𝑛 + 1))))
Assertion
Ref Expression
stirlinglem12 (𝑁 ∈ ℕ → ((𝐵‘1) − (1 / 4)) ≤ (𝐵𝑁))
Distinct variable group:   𝑛,𝑁
Allowed substitution hints:   𝐴(𝑛)   𝐵(𝑛)   𝐹(𝑛)

Proof of Theorem stirlinglem12
Dummy variables 𝑖 𝑗 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1nn 10982 . . . . 5 1 ∈ ℕ
2 stirlinglem12.1 . . . . . . 7 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))
32stirlinglem2 39620 . . . . . 6 (1 ∈ ℕ → (𝐴‘1) ∈ ℝ+)
4 relogcl 24239 . . . . . 6 ((𝐴‘1) ∈ ℝ+ → (log‘(𝐴‘1)) ∈ ℝ)
51, 3, 4mp2b 10 . . . . 5 (log‘(𝐴‘1)) ∈ ℝ
6 nfcv 2761 . . . . . 6 𝑛1
7 nfcv 2761 . . . . . . 7 𝑛log
8 nfmpt1 4712 . . . . . . . . 9 𝑛(𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))
92, 8nfcxfr 2759 . . . . . . . 8 𝑛𝐴
109, 6nffv 6160 . . . . . . 7 𝑛(𝐴‘1)
117, 10nffv 6160 . . . . . 6 𝑛(log‘(𝐴‘1))
12 fveq2 6153 . . . . . . 7 (𝑛 = 1 → (𝐴𝑛) = (𝐴‘1))
1312fveq2d 6157 . . . . . 6 (𝑛 = 1 → (log‘(𝐴𝑛)) = (log‘(𝐴‘1)))
14 stirlinglem12.2 . . . . . 6 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴𝑛)))
156, 11, 13, 14fvmptf 6262 . . . . 5 ((1 ∈ ℕ ∧ (log‘(𝐴‘1)) ∈ ℝ) → (𝐵‘1) = (log‘(𝐴‘1)))
161, 5, 15mp2an 707 . . . 4 (𝐵‘1) = (log‘(𝐴‘1))
1716, 5eqeltri 2694 . . 3 (𝐵‘1) ∈ ℝ
1817a1i 11 . 2 (𝑁 ∈ ℕ → (𝐵‘1) ∈ ℝ)
192stirlinglem2 39620 . . . . 5 (𝑁 ∈ ℕ → (𝐴𝑁) ∈ ℝ+)
2019relogcld 24286 . . . 4 (𝑁 ∈ ℕ → (log‘(𝐴𝑁)) ∈ ℝ)
21 nfcv 2761 . . . . 5 𝑛𝑁
229, 21nffv 6160 . . . . . 6 𝑛(𝐴𝑁)
237, 22nffv 6160 . . . . 5 𝑛(log‘(𝐴𝑁))
24 fveq2 6153 . . . . . 6 (𝑛 = 𝑁 → (𝐴𝑛) = (𝐴𝑁))
2524fveq2d 6157 . . . . 5 (𝑛 = 𝑁 → (log‘(𝐴𝑛)) = (log‘(𝐴𝑁)))
2621, 23, 25, 14fvmptf 6262 . . . 4 ((𝑁 ∈ ℕ ∧ (log‘(𝐴𝑁)) ∈ ℝ) → (𝐵𝑁) = (log‘(𝐴𝑁)))
2720, 26mpdan 701 . . 3 (𝑁 ∈ ℕ → (𝐵𝑁) = (log‘(𝐴𝑁)))
2827, 20eqeltrd 2698 . 2 (𝑁 ∈ ℕ → (𝐵𝑁) ∈ ℝ)
29 4re 11048 . . . 4 4 ∈ ℝ
30 4ne0 11068 . . . 4 4 ≠ 0
3129, 30rereccli 10741 . . 3 (1 / 4) ∈ ℝ
3231a1i 11 . 2 (𝑁 ∈ ℕ → (1 / 4) ∈ ℝ)
33 fveq2 6153 . . . . 5 (𝑘 = 𝑗 → (𝐵𝑘) = (𝐵𝑗))
34 fveq2 6153 . . . . 5 (𝑘 = (𝑗 + 1) → (𝐵𝑘) = (𝐵‘(𝑗 + 1)))
35 fveq2 6153 . . . . 5 (𝑘 = 1 → (𝐵𝑘) = (𝐵‘1))
36 fveq2 6153 . . . . 5 (𝑘 = 𝑁 → (𝐵𝑘) = (𝐵𝑁))
37 elnnuz 11675 . . . . . 6 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ‘1))
3837biimpi 206 . . . . 5 (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ‘1))
39 elfznn 12319 . . . . . . . 8 (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ)
402stirlinglem2 39620 . . . . . . . . . 10 (𝑘 ∈ ℕ → (𝐴𝑘) ∈ ℝ+)
4139, 40syl 17 . . . . . . . . 9 (𝑘 ∈ (1...𝑁) → (𝐴𝑘) ∈ ℝ+)
4241relogcld 24286 . . . . . . . 8 (𝑘 ∈ (1...𝑁) → (log‘(𝐴𝑘)) ∈ ℝ)
43 nfcv 2761 . . . . . . . . 9 𝑛𝑘
449, 43nffv 6160 . . . . . . . . . 10 𝑛(𝐴𝑘)
457, 44nffv 6160 . . . . . . . . 9 𝑛(log‘(𝐴𝑘))
46 fveq2 6153 . . . . . . . . . 10 (𝑛 = 𝑘 → (𝐴𝑛) = (𝐴𝑘))
4746fveq2d 6157 . . . . . . . . 9 (𝑛 = 𝑘 → (log‘(𝐴𝑛)) = (log‘(𝐴𝑘)))
4843, 45, 47, 14fvmptf 6262 . . . . . . . 8 ((𝑘 ∈ ℕ ∧ (log‘(𝐴𝑘)) ∈ ℝ) → (𝐵𝑘) = (log‘(𝐴𝑘)))
4939, 42, 48syl2anc 692 . . . . . . 7 (𝑘 ∈ (1...𝑁) → (𝐵𝑘) = (log‘(𝐴𝑘)))
5049adantl 482 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (𝐵𝑘) = (log‘(𝐴𝑘)))
5141rpcnd 11825 . . . . . . . 8 (𝑘 ∈ (1...𝑁) → (𝐴𝑘) ∈ ℂ)
5251adantl 482 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (𝐴𝑘) ∈ ℂ)
5340rpne0d 11828 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝐴𝑘) ≠ 0)
5439, 53syl 17 . . . . . . . 8 (𝑘 ∈ (1...𝑁) → (𝐴𝑘) ≠ 0)
5554adantl 482 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (𝐴𝑘) ≠ 0)
5652, 55logcld 24234 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (log‘(𝐴𝑘)) ∈ ℂ)
5750, 56eqeltrd 2698 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (𝐵𝑘) ∈ ℂ)
5833, 34, 35, 36, 38, 57telfsumo 14468 . . . 4 (𝑁 ∈ ℕ → Σ𝑗 ∈ (1..^𝑁)((𝐵𝑗) − (𝐵‘(𝑗 + 1))) = ((𝐵‘1) − (𝐵𝑁)))
59 nnz 11350 . . . . . 6 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
60 fzoval 12419 . . . . . 6 (𝑁 ∈ ℤ → (1..^𝑁) = (1...(𝑁 − 1)))
6159, 60syl 17 . . . . 5 (𝑁 ∈ ℕ → (1..^𝑁) = (1...(𝑁 − 1)))
6261sumeq1d 14372 . . . 4 (𝑁 ∈ ℕ → Σ𝑗 ∈ (1..^𝑁)((𝐵𝑗) − (𝐵‘(𝑗 + 1))) = Σ𝑗 ∈ (1...(𝑁 − 1))((𝐵𝑗) − (𝐵‘(𝑗 + 1))))
6358, 62eqtr3d 2657 . . 3 (𝑁 ∈ ℕ → ((𝐵‘1) − (𝐵𝑁)) = Σ𝑗 ∈ (1...(𝑁 − 1))((𝐵𝑗) − (𝐵‘(𝑗 + 1))))
64 fzfid 12719 . . . . 5 (𝑁 ∈ ℕ → (1...(𝑁 − 1)) ∈ Fin)
65 elfznn 12319 . . . . . . . 8 (𝑗 ∈ (1...(𝑁 − 1)) → 𝑗 ∈ ℕ)
6665adantl 482 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → 𝑗 ∈ ℕ)
672stirlinglem2 39620 . . . . . . . . . 10 (𝑗 ∈ ℕ → (𝐴𝑗) ∈ ℝ+)
6867relogcld 24286 . . . . . . . . 9 (𝑗 ∈ ℕ → (log‘(𝐴𝑗)) ∈ ℝ)
69 nfcv 2761 . . . . . . . . . 10 𝑛𝑗
709, 69nffv 6160 . . . . . . . . . . 11 𝑛(𝐴𝑗)
717, 70nffv 6160 . . . . . . . . . 10 𝑛(log‘(𝐴𝑗))
72 fveq2 6153 . . . . . . . . . . 11 (𝑛 = 𝑗 → (𝐴𝑛) = (𝐴𝑗))
7372fveq2d 6157 . . . . . . . . . 10 (𝑛 = 𝑗 → (log‘(𝐴𝑛)) = (log‘(𝐴𝑗)))
7469, 71, 73, 14fvmptf 6262 . . . . . . . . 9 ((𝑗 ∈ ℕ ∧ (log‘(𝐴𝑗)) ∈ ℝ) → (𝐵𝑗) = (log‘(𝐴𝑗)))
7568, 74mpdan 701 . . . . . . . 8 (𝑗 ∈ ℕ → (𝐵𝑗) = (log‘(𝐴𝑗)))
7675, 68eqeltrd 2698 . . . . . . 7 (𝑗 ∈ ℕ → (𝐵𝑗) ∈ ℝ)
7766, 76syl 17 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (𝐵𝑗) ∈ ℝ)
78 peano2nn 10983 . . . . . . . . . 10 (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
792stirlinglem2 39620 . . . . . . . . . . . 12 ((𝑗 + 1) ∈ ℕ → (𝐴‘(𝑗 + 1)) ∈ ℝ+)
8078, 79syl 17 . . . . . . . . . . 11 (𝑗 ∈ ℕ → (𝐴‘(𝑗 + 1)) ∈ ℝ+)
8180relogcld 24286 . . . . . . . . . 10 (𝑗 ∈ ℕ → (log‘(𝐴‘(𝑗 + 1))) ∈ ℝ)
82 nfcv 2761 . . . . . . . . . . 11 𝑛(𝑗 + 1)
839, 82nffv 6160 . . . . . . . . . . . 12 𝑛(𝐴‘(𝑗 + 1))
847, 83nffv 6160 . . . . . . . . . . 11 𝑛(log‘(𝐴‘(𝑗 + 1)))
85 fveq2 6153 . . . . . . . . . . . 12 (𝑛 = (𝑗 + 1) → (𝐴𝑛) = (𝐴‘(𝑗 + 1)))
8685fveq2d 6157 . . . . . . . . . . 11 (𝑛 = (𝑗 + 1) → (log‘(𝐴𝑛)) = (log‘(𝐴‘(𝑗 + 1))))
8782, 84, 86, 14fvmptf 6262 . . . . . . . . . 10 (((𝑗 + 1) ∈ ℕ ∧ (log‘(𝐴‘(𝑗 + 1))) ∈ ℝ) → (𝐵‘(𝑗 + 1)) = (log‘(𝐴‘(𝑗 + 1))))
8878, 81, 87syl2anc 692 . . . . . . . . 9 (𝑗 ∈ ℕ → (𝐵‘(𝑗 + 1)) = (log‘(𝐴‘(𝑗 + 1))))
8988, 81eqeltrd 2698 . . . . . . . 8 (𝑗 ∈ ℕ → (𝐵‘(𝑗 + 1)) ∈ ℝ)
9065, 89syl 17 . . . . . . 7 (𝑗 ∈ (1...(𝑁 − 1)) → (𝐵‘(𝑗 + 1)) ∈ ℝ)
9190adantl 482 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (𝐵‘(𝑗 + 1)) ∈ ℝ)
9277, 91resubcld 10409 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → ((𝐵𝑗) − (𝐵‘(𝑗 + 1))) ∈ ℝ)
9364, 92fsumrecl 14405 . . . 4 (𝑁 ∈ ℕ → Σ𝑗 ∈ (1...(𝑁 − 1))((𝐵𝑗) − (𝐵‘(𝑗 + 1))) ∈ ℝ)
9431a1i 11 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (1 / 4) ∈ ℝ)
9565nnred 10986 . . . . . . . . 9 (𝑗 ∈ (1...(𝑁 − 1)) → 𝑗 ∈ ℝ)
96 1red 10006 . . . . . . . . . 10 (𝑗 ∈ (1...(𝑁 − 1)) → 1 ∈ ℝ)
9795, 96readdcld 10020 . . . . . . . . 9 (𝑗 ∈ (1...(𝑁 − 1)) → (𝑗 + 1) ∈ ℝ)
9895, 97remulcld 10021 . . . . . . . 8 (𝑗 ∈ (1...(𝑁 − 1)) → (𝑗 · (𝑗 + 1)) ∈ ℝ)
9995recnd 10019 . . . . . . . . 9 (𝑗 ∈ (1...(𝑁 − 1)) → 𝑗 ∈ ℂ)
100 1cnd 10007 . . . . . . . . . 10 (𝑗 ∈ (1...(𝑁 − 1)) → 1 ∈ ℂ)
10199, 100addcld 10010 . . . . . . . . 9 (𝑗 ∈ (1...(𝑁 − 1)) → (𝑗 + 1) ∈ ℂ)
10265nnne0d 11016 . . . . . . . . 9 (𝑗 ∈ (1...(𝑁 − 1)) → 𝑗 ≠ 0)
10378nnne0d 11016 . . . . . . . . . 10 (𝑗 ∈ ℕ → (𝑗 + 1) ≠ 0)
10465, 103syl 17 . . . . . . . . 9 (𝑗 ∈ (1...(𝑁 − 1)) → (𝑗 + 1) ≠ 0)
10599, 101, 102, 104mulne0d 10630 . . . . . . . 8 (𝑗 ∈ (1...(𝑁 − 1)) → (𝑗 · (𝑗 + 1)) ≠ 0)
10698, 105rereccld 10803 . . . . . . 7 (𝑗 ∈ (1...(𝑁 − 1)) → (1 / (𝑗 · (𝑗 + 1))) ∈ ℝ)
107106adantl 482 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (1 / (𝑗 · (𝑗 + 1))) ∈ ℝ)
10894, 107remulcld 10021 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → ((1 / 4) · (1 / (𝑗 · (𝑗 + 1)))) ∈ ℝ)
10964, 108fsumrecl 14405 . . . 4 (𝑁 ∈ ℕ → Σ𝑗 ∈ (1...(𝑁 − 1))((1 / 4) · (1 / (𝑗 · (𝑗 + 1)))) ∈ ℝ)
110 eqid 2621 . . . . . . 7 (𝑖 ∈ ℕ ↦ ((1 / ((2 · 𝑖) + 1)) · ((1 / ((2 · 𝑗) + 1))↑(2 · 𝑖)))) = (𝑖 ∈ ℕ ↦ ((1 / ((2 · 𝑖) + 1)) · ((1 / ((2 · 𝑗) + 1))↑(2 · 𝑖))))
111 eqid 2621 . . . . . . 7 (𝑖 ∈ ℕ ↦ ((1 / (((2 · 𝑗) + 1)↑2))↑𝑖)) = (𝑖 ∈ ℕ ↦ ((1 / (((2 · 𝑗) + 1)↑2))↑𝑖))
1122, 14, 110, 111stirlinglem10 39628 . . . . . 6 (𝑗 ∈ ℕ → ((𝐵𝑗) − (𝐵‘(𝑗 + 1))) ≤ ((1 / 4) · (1 / (𝑗 · (𝑗 + 1)))))
11366, 112syl 17 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → ((𝐵𝑗) − (𝐵‘(𝑗 + 1))) ≤ ((1 / 4) · (1 / (𝑗 · (𝑗 + 1)))))
11464, 92, 108, 113fsumle 14465 . . . 4 (𝑁 ∈ ℕ → Σ𝑗 ∈ (1...(𝑁 − 1))((𝐵𝑗) − (𝐵‘(𝑗 + 1))) ≤ Σ𝑗 ∈ (1...(𝑁 − 1))((1 / 4) · (1 / (𝑗 · (𝑗 + 1)))))
11564, 107fsumrecl 14405 . . . . . 6 (𝑁 ∈ ℕ → Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) ∈ ℝ)
116 1red 10006 . . . . . 6 (𝑁 ∈ ℕ → 1 ∈ ℝ)
117 4pos 11067 . . . . . . . . 9 0 < 4
11829, 117elrpii 11786 . . . . . . . 8 4 ∈ ℝ+
119118a1i 11 . . . . . . 7 (𝑁 ∈ ℕ → 4 ∈ ℝ+)
120 0red 9992 . . . . . . . 8 (𝑁 ∈ ℕ → 0 ∈ ℝ)
121 0lt1 10501 . . . . . . . . 9 0 < 1
122121a1i 11 . . . . . . . 8 (𝑁 ∈ ℕ → 0 < 1)
123120, 116, 122ltled 10136 . . . . . . 7 (𝑁 ∈ ℕ → 0 ≤ 1)
124116, 119, 123divge0d 11863 . . . . . 6 (𝑁 ∈ ℕ → 0 ≤ (1 / 4))
125 eqid 2621 . . . . . . . . . 10 (ℤ𝑁) = (ℤ𝑁)
126 eluznn 11709 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑗 ∈ ℕ)
127 stirlinglem12.3 . . . . . . . . . . . . 13 𝐹 = (𝑛 ∈ ℕ ↦ (1 / (𝑛 · (𝑛 + 1))))
128127a1i 11 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → 𝐹 = (𝑛 ∈ ℕ ↦ (1 / (𝑛 · (𝑛 + 1)))))
129 simpr 477 . . . . . . . . . . . . . 14 ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → 𝑛 = 𝑗)
130129oveq1d 6625 . . . . . . . . . . . . . 14 ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → (𝑛 + 1) = (𝑗 + 1))
131129, 130oveq12d 6628 . . . . . . . . . . . . 13 ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → (𝑛 · (𝑛 + 1)) = (𝑗 · (𝑗 + 1)))
132131oveq2d 6626 . . . . . . . . . . . 12 ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → (1 / (𝑛 · (𝑛 + 1))) = (1 / (𝑗 · (𝑗 + 1))))
133 id 22 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
134 nnre 10978 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ → 𝑗 ∈ ℝ)
135 1red 10006 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ → 1 ∈ ℝ)
136134, 135readdcld 10020 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℝ)
137134, 136remulcld 10021 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ → (𝑗 · (𝑗 + 1)) ∈ ℝ)
138 nncn 10979 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ → 𝑗 ∈ ℂ)
139 1cnd 10007 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ → 1 ∈ ℂ)
140138, 139addcld 10010 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℂ)
141 nnne0 11004 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ → 𝑗 ≠ 0)
142138, 140, 141, 103mulne0d 10630 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ → (𝑗 · (𝑗 + 1)) ≠ 0)
143137, 142rereccld 10803 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → (1 / (𝑗 · (𝑗 + 1))) ∈ ℝ)
144128, 132, 133, 143fvmptd 6250 . . . . . . . . . . 11 (𝑗 ∈ ℕ → (𝐹𝑗) = (1 / (𝑗 · (𝑗 + 1))))
145126, 144syl 17 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑁)) → (𝐹𝑗) = (1 / (𝑗 · (𝑗 + 1))))
146126nnred 10986 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑗 ∈ ℝ)
147 1red 10006 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑁)) → 1 ∈ ℝ)
148146, 147readdcld 10020 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑁)) → (𝑗 + 1) ∈ ℝ)
149146, 148remulcld 10021 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑁)) → (𝑗 · (𝑗 + 1)) ∈ ℝ)
150146recnd 10019 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑗 ∈ ℂ)
151 1cnd 10007 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑁)) → 1 ∈ ℂ)
152150, 151addcld 10010 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑁)) → (𝑗 + 1) ∈ ℂ)
153126nnne0d 11016 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑗 ≠ 0)
154126, 103syl 17 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑁)) → (𝑗 + 1) ≠ 0)
155150, 152, 153, 154mulne0d 10630 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑁)) → (𝑗 · (𝑗 + 1)) ≠ 0)
156149, 155rereccld 10803 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑁)) → (1 / (𝑗 · (𝑗 + 1))) ∈ ℝ)
157 seqeq1 12751 . . . . . . . . . . . . 13 (𝑁 = 1 → seq𝑁( + , 𝐹) = seq1( + , 𝐹))
158127trireciplem 14526 . . . . . . . . . . . . . 14 seq1( + , 𝐹) ⇝ 1
159 climrel 14164 . . . . . . . . . . . . . . 15 Rel ⇝
160159releldmi 5327 . . . . . . . . . . . . . 14 (seq1( + , 𝐹) ⇝ 1 → seq1( + , 𝐹) ∈ dom ⇝ )
161158, 160mp1i 13 . . . . . . . . . . . . 13 (𝑁 = 1 → seq1( + , 𝐹) ∈ dom ⇝ )
162157, 161eqeltrd 2698 . . . . . . . . . . . 12 (𝑁 = 1 → seq𝑁( + , 𝐹) ∈ dom ⇝ )
163162adantl 482 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
164 simpl 473 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1) → 𝑁 ∈ ℕ)
165 simpr 477 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1) → ¬ 𝑁 = 1)
166 elnn1uz2 11716 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈ (ℤ‘2)))
167164, 166sylib 208 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1) → (𝑁 = 1 ∨ 𝑁 ∈ (ℤ‘2)))
168167ord 392 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1) → (¬ 𝑁 = 1 → 𝑁 ∈ (ℤ‘2)))
169165, 168mpd 15 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1) → 𝑁 ∈ (ℤ‘2))
170 uz2m1nn 11714 . . . . . . . . . . . . 13 (𝑁 ∈ (ℤ‘2) → (𝑁 − 1) ∈ ℕ)
171169, 170syl 17 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1) → (𝑁 − 1) ∈ ℕ)
172 nncn 10979 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
173172adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ) → 𝑁 ∈ ℂ)
174 1cnd 10007 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ) → 1 ∈ ℂ)
175173, 174npcand 10347 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ) → ((𝑁 − 1) + 1) = 𝑁)
176175eqcomd 2627 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ) → 𝑁 = ((𝑁 − 1) + 1))
177176seqeq1d 12754 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ) → seq𝑁( + , 𝐹) = seq((𝑁 − 1) + 1)( + , 𝐹))
178 nnuz 11674 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
179 id 22 . . . . . . . . . . . . . . . 16 ((𝑁 − 1) ∈ ℕ → (𝑁 − 1) ∈ ℕ)
180143recnd 10019 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → (1 / (𝑗 · (𝑗 + 1))) ∈ ℂ)
181144, 180eqeltrd 2698 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ → (𝐹𝑗) ∈ ℂ)
182181adantl 482 . . . . . . . . . . . . . . . 16 (((𝑁 − 1) ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) ∈ ℂ)
183158a1i 11 . . . . . . . . . . . . . . . 16 ((𝑁 − 1) ∈ ℕ → seq1( + , 𝐹) ⇝ 1)
184178, 179, 182, 183clim2ser 14326 . . . . . . . . . . . . . . 15 ((𝑁 − 1) ∈ ℕ → seq((𝑁 − 1) + 1)( + , 𝐹) ⇝ (1 − (seq1( + , 𝐹)‘(𝑁 − 1))))
185184adantl 482 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ) → seq((𝑁 − 1) + 1)( + , 𝐹) ⇝ (1 − (seq1( + , 𝐹)‘(𝑁 − 1))))
186177, 185eqbrtrd 4640 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ) → seq𝑁( + , 𝐹) ⇝ (1 − (seq1( + , 𝐹)‘(𝑁 − 1))))
187159releldmi 5327 . . . . . . . . . . . . 13 (seq𝑁( + , 𝐹) ⇝ (1 − (seq1( + , 𝐹)‘(𝑁 − 1))) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
188186, 187syl 17 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
189164, 171, 188syl2anc 692 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
190163, 189pm2.61dan 831 . . . . . . . . . 10 (𝑁 ∈ ℕ → seq𝑁( + , 𝐹) ∈ dom ⇝ )
191125, 59, 145, 156, 190isumrecl 14431 . . . . . . . . 9 (𝑁 ∈ ℕ → Σ𝑗 ∈ (ℤ𝑁)(1 / (𝑗 · (𝑗 + 1))) ∈ ℝ)
192126nnrpd 11821 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑗 ∈ ℝ+)
193192rpge0d 11827 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑁)) → 0 ≤ 𝑗)
194146, 193ge0p1rpd 11853 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑁)) → (𝑗 + 1) ∈ ℝ+)
195192, 194rpmulcld 11839 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑁)) → (𝑗 · (𝑗 + 1)) ∈ ℝ+)
196123adantr 481 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑁)) → 0 ≤ 1)
197147, 195, 196divge0d 11863 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑁)) → 0 ≤ (1 / (𝑗 · (𝑗 + 1))))
198125, 59, 145, 156, 190, 197isumge0 14432 . . . . . . . . 9 (𝑁 ∈ ℕ → 0 ≤ Σ𝑗 ∈ (ℤ𝑁)(1 / (𝑗 · (𝑗 + 1))))
199120, 191, 115, 198leadd2dd 10593 . . . . . . . 8 (𝑁 ∈ ℕ → (Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) + 0) ≤ (Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) + Σ𝑗 ∈ (ℤ𝑁)(1 / (𝑗 · (𝑗 + 1)))))
200115recnd 10019 . . . . . . . . . 10 (𝑁 ∈ ℕ → Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) ∈ ℂ)
201200addid1d 10187 . . . . . . . . 9 (𝑁 ∈ ℕ → (Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) + 0) = Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))))
202201eqcomd 2627 . . . . . . . 8 (𝑁 ∈ ℕ → Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) = (Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) + 0))
203 id 22 . . . . . . . . 9 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ)
204144adantl 482 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) = (1 / (𝑗 · (𝑗 + 1))))
205138adantl 482 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℂ)
206 1cnd 10007 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 1 ∈ ℂ)
207205, 206addcld 10010 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℂ)
208205, 207mulcld 10011 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝑗 · (𝑗 + 1)) ∈ ℂ)
209141adantl 482 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ≠ 0)
210103adantl 482 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ≠ 0)
211205, 207, 209, 210mulne0d 10630 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝑗 · (𝑗 + 1)) ≠ 0)
212208, 211reccld 10745 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (1 / (𝑗 · (𝑗 + 1))) ∈ ℂ)
213158, 160mp1i 13 . . . . . . . . 9 (𝑁 ∈ ℕ → seq1( + , 𝐹) ∈ dom ⇝ )
214178, 125, 203, 204, 212, 213isumsplit 14504 . . . . . . . 8 (𝑁 ∈ ℕ → Σ𝑗 ∈ ℕ (1 / (𝑗 · (𝑗 + 1))) = (Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) + Σ𝑗 ∈ (ℤ𝑁)(1 / (𝑗 · (𝑗 + 1)))))
215199, 202, 2143brtr4d 4650 . . . . . . 7 (𝑁 ∈ ℕ → Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) ≤ Σ𝑗 ∈ ℕ (1 / (𝑗 · (𝑗 + 1))))
216 1zzd 11359 . . . . . . . . 9 (⊤ → 1 ∈ ℤ)
217144adantl 482 . . . . . . . . 9 ((⊤ ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) = (1 / (𝑗 · (𝑗 + 1))))
218180adantl 482 . . . . . . . . 9 ((⊤ ∧ 𝑗 ∈ ℕ) → (1 / (𝑗 · (𝑗 + 1))) ∈ ℂ)
219158a1i 11 . . . . . . . . 9 (⊤ → seq1( + , 𝐹) ⇝ 1)
220178, 216, 217, 218, 219isumclim 14423 . . . . . . . 8 (⊤ → Σ𝑗 ∈ ℕ (1 / (𝑗 · (𝑗 + 1))) = 1)
221220trud 1490 . . . . . . 7 Σ𝑗 ∈ ℕ (1 / (𝑗 · (𝑗 + 1))) = 1
222215, 221syl6breq 4659 . . . . . 6 (𝑁 ∈ ℕ → Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) ≤ 1)
223115, 116, 32, 124, 222lemul2ad 10915 . . . . 5 (𝑁 ∈ ℕ → ((1 / 4) · Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1)))) ≤ ((1 / 4) · 1))
224 4cn 11049 . . . . . . . 8 4 ∈ ℂ
225224a1i 11 . . . . . . 7 (𝑁 ∈ ℕ → 4 ∈ ℂ)
226117a1i 11 . . . . . . . 8 (𝑁 ∈ ℕ → 0 < 4)
227226gt0ne0d 10543 . . . . . . 7 (𝑁 ∈ ℕ → 4 ≠ 0)
228225, 227reccld 10745 . . . . . 6 (𝑁 ∈ ℕ → (1 / 4) ∈ ℂ)
229107recnd 10019 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (1 / (𝑗 · (𝑗 + 1))) ∈ ℂ)
23064, 228, 229fsummulc2 14451 . . . . 5 (𝑁 ∈ ℕ → ((1 / 4) · Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1)))) = Σ𝑗 ∈ (1...(𝑁 − 1))((1 / 4) · (1 / (𝑗 · (𝑗 + 1)))))
231228mulid1d 10008 . . . . 5 (𝑁 ∈ ℕ → ((1 / 4) · 1) = (1 / 4))
232223, 230, 2313brtr3d 4649 . . . 4 (𝑁 ∈ ℕ → Σ𝑗 ∈ (1...(𝑁 − 1))((1 / 4) · (1 / (𝑗 · (𝑗 + 1)))) ≤ (1 / 4))
23393, 109, 32, 114, 232letrd 10145 . . 3 (𝑁 ∈ ℕ → Σ𝑗 ∈ (1...(𝑁 − 1))((𝐵𝑗) − (𝐵‘(𝑗 + 1))) ≤ (1 / 4))
23463, 233eqbrtrd 4640 . 2 (𝑁 ∈ ℕ → ((𝐵‘1) − (𝐵𝑁)) ≤ (1 / 4))
23518, 28, 32, 234subled 10581 1 (𝑁 ∈ ℕ → ((𝐵‘1) − (1 / 4)) ≤ (𝐵𝑁))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 383   ∧ wa 384   = wceq 1480  ⊤wtru 1481   ∈ wcel 1987   ≠ wne 2790   class class class wbr 4618   ↦ cmpt 4678  dom cdm 5079  ‘cfv 5852  (class class class)co 6610  ℂcc 9885  ℝcr 9886  0cc0 9887  1c1 9888   + caddc 9890   · cmul 9892   < clt 10025   ≤ cle 10026   − cmin 10217   / cdiv 10635  ℕcn 10971  2c2 11021  4c4 11023  ℤcz 11328  ℤ≥cuz 11638  ℝ+crp 11783  ...cfz 12275  ..^cfzo 12413  seqcseq 12748  ↑cexp 12807  !cfa 13007  √csqrt 13914   ⇝ cli 14156  Σcsu 14357  eceu 14725  logclog 24218 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8489  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964  ax-pre-sup 9965  ax-addf 9966  ax-mulf 9967 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-om 7020  df-1st 7120  df-2nd 7121  df-supp 7248  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-pm 7812  df-ixp 7860  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-fsupp 8227  df-fi 8268  df-sup 8299  df-inf 8300  df-oi 8366  df-card 8716  df-cda 8941  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-div 10636  df-nn 10972  df-2 11030  df-3 11031  df-4 11032  df-5 11033  df-6 11034  df-7 11035  df-8 11036  df-9 11037  df-n0 11244  df-xnn0 11315  df-z 11329  df-dec 11445  df-uz 11639  df-q 11740  df-rp 11784  df-xneg 11897  df-xadd 11898  df-xmul 11899  df-ioo 12128  df-ioc 12129  df-ico 12130  df-icc 12131  df-fz 12276  df-fzo 12414  df-fl 12540  df-mod 12616  df-seq 12749  df-exp 12808  df-fac 13008  df-bc 13037  df-hash 13065  df-shft 13748  df-cj 13780  df-re 13781  df-im 13782  df-sqrt 13916  df-abs 13917  df-limsup 14143  df-clim 14160  df-rlim 14161  df-sum 14358  df-ef 14730  df-e 14731  df-sin 14732  df-cos 14733  df-tan 14734  df-pi 14735  df-dvds 14915  df-struct 15790  df-ndx 15791  df-slot 15792  df-base 15793  df-sets 15794  df-ress 15795  df-plusg 15882  df-mulr 15883  df-starv 15884  df-sca 15885  df-vsca 15886  df-ip 15887  df-tset 15888  df-ple 15889  df-ds 15892  df-unif 15893  df-hom 15894  df-cco 15895  df-rest 16011  df-topn 16012  df-0g 16030  df-gsum 16031  df-topgen 16032  df-pt 16033  df-prds 16036  df-xrs 16090  df-qtop 16095  df-imas 16096  df-xps 16098  df-mre 16174  df-mrc 16175  df-acs 16177  df-mgm 17170  df-sgrp 17212  df-mnd 17223  df-submnd 17264  df-mulg 17469  df-cntz 17678  df-cmn 18123  df-psmet 19666  df-xmet 19667  df-met 19668  df-bl 19669  df-mopn 19670  df-fbas 19671  df-fg 19672  df-cnfld 19675  df-top 20627  df-topon 20644  df-topsp 20657  df-bases 20670  df-cld 20742  df-ntr 20743  df-cls 20744  df-nei 20821  df-lp 20859  df-perf 20860  df-cn 20950  df-cnp 20951  df-haus 21038  df-cmp 21109  df-tx 21284  df-hmeo 21477  df-fil 21569  df-fm 21661  df-flim 21662  df-flf 21663  df-xms 22044  df-ms 22045  df-tms 22046  df-cncf 22600  df-limc 23549  df-dv 23550  df-ulm 24048  df-log 24220  df-cxp 24221 This theorem is referenced by:  stirlinglem13  39631
 Copyright terms: Public domain W3C validator