Metamath Proof Explorer

Theorem stirlinglem12

Description: The sequence B is bounded below. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem12.1 ⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
stirlinglem12.2 ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) )
stirlinglem12.3 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
Assertion stirlinglem12 ( 𝑁 ∈ ℕ → ( ( 𝐵 ‘ 1 ) − ( 1 / 4 ) ) ≤ ( 𝐵 ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 stirlinglem12.1 ⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
2 stirlinglem12.2 ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) )
3 stirlinglem12.3 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
4 1nn ⊢ 1 ∈ ℕ
5 1 stirlinglem2 ⊢ ( 1 ∈ ℕ → ( 𝐴 ‘ 1 ) ∈ ℝ+ )
6 relogcl ⊢ ( ( 𝐴 ‘ 1 ) ∈ ℝ+ → ( log ‘ ( 𝐴 ‘ 1 ) ) ∈ ℝ )
7 4 5 6 mp2b ⊢ ( log ‘ ( 𝐴 ‘ 1 ) ) ∈ ℝ
8 nfcv ⊢ Ⅎ 𝑛 1
9 nfcv ⊢ Ⅎ 𝑛 log
10 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
11 1 10 nfcxfr ⊢ Ⅎ 𝑛 𝐴
12 11 8 nffv ⊢ Ⅎ 𝑛 ( 𝐴 ‘ 1 )
13 9 12 nffv ⊢ Ⅎ 𝑛 ( log ‘ ( 𝐴 ‘ 1 ) )
14 2fveq3 ⊢ ( 𝑛 = 1 → ( log ‘ ( 𝐴 ‘ 𝑛 ) ) = ( log ‘ ( 𝐴 ‘ 1 ) ) )
15 8 13 14 2 fvmptf ⊢ ( ( 1 ∈ ℕ ∧ ( log ‘ ( 𝐴 ‘ 1 ) ) ∈ ℝ ) → ( 𝐵 ‘ 1 ) = ( log ‘ ( 𝐴 ‘ 1 ) ) )
16 4 7 15 mp2an ⊢ ( 𝐵 ‘ 1 ) = ( log ‘ ( 𝐴 ‘ 1 ) )
17 16 7 eqeltri ⊢ ( 𝐵 ‘ 1 ) ∈ ℝ
18 17 a1i ⊢ ( 𝑁 ∈ ℕ → ( 𝐵 ‘ 1 ) ∈ ℝ )
19 1 stirlinglem2 ⊢ ( 𝑁 ∈ ℕ → ( 𝐴 ‘ 𝑁 ) ∈ ℝ+ )
20 19 relogcld ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( 𝐴 ‘ 𝑁 ) ) ∈ ℝ )
21 nfcv ⊢ Ⅎ 𝑛 𝑁
22 11 21 nffv ⊢ Ⅎ 𝑛 ( 𝐴 ‘ 𝑁 )
23 9 22 nffv ⊢ Ⅎ 𝑛 ( log ‘ ( 𝐴 ‘ 𝑁 ) )
24 2fveq3 ⊢ ( 𝑛 = 𝑁 → ( log ‘ ( 𝐴 ‘ 𝑛 ) ) = ( log ‘ ( 𝐴 ‘ 𝑁 ) ) )
25 21 23 24 2 fvmptf ⊢ ( ( 𝑁 ∈ ℕ ∧ ( log ‘ ( 𝐴 ‘ 𝑁 ) ) ∈ ℝ ) → ( 𝐵 ‘ 𝑁 ) = ( log ‘ ( 𝐴 ‘ 𝑁 ) ) )
26 20 25 mpdan ⊢ ( 𝑁 ∈ ℕ → ( 𝐵 ‘ 𝑁 ) = ( log ‘ ( 𝐴 ‘ 𝑁 ) ) )
27 26 20 eqeltrd ⊢ ( 𝑁 ∈ ℕ → ( 𝐵 ‘ 𝑁 ) ∈ ℝ )
28 4re ⊢ 4 ∈ ℝ
29 4ne0 ⊢ 4 ≠ 0
30 28 29 rereccli ⊢ ( 1 / 4 ) ∈ ℝ
31 30 a1i ⊢ ( 𝑁 ∈ ℕ → ( 1 / 4 ) ∈ ℝ )
32 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑗 ) )
33 fveq2 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ ( 𝑗 + 1 ) ) )
34 fveq2 ⊢ ( 𝑘 = 1 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 1 ) )
35 fveq2 ⊢ ( 𝑘 = 𝑁 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑁 ) )
36 elnnuz ⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
37 36 biimpi ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
38 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℕ )
39 1 stirlinglem2 ⊢ ( 𝑘 ∈ ℕ → ( 𝐴 ‘ 𝑘 ) ∈ ℝ+ )
40 38 39 syl ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ+ )
41 40 relogcld ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( log ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ )
42 nfcv ⊢ Ⅎ 𝑛 𝑘
43 11 42 nffv ⊢ Ⅎ 𝑛 ( 𝐴 ‘ 𝑘 )
44 9 43 nffv ⊢ Ⅎ 𝑛 ( log ‘ ( 𝐴 ‘ 𝑘 ) )
45 2fveq3 ⊢ ( 𝑛 = 𝑘 → ( log ‘ ( 𝐴 ‘ 𝑛 ) ) = ( log ‘ ( 𝐴 ‘ 𝑘 ) ) )
46 42 44 45 2 fvmptf ⊢ ( ( 𝑘 ∈ ℕ ∧ ( log ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ ) → ( 𝐵 ‘ 𝑘 ) = ( log ‘ ( 𝐴 ‘ 𝑘 ) ) )
47 38 41 46 syl2anc ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝐵 ‘ 𝑘 ) = ( log ‘ ( 𝐴 ‘ 𝑘 ) ) )
48 47 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑘 ) = ( log ‘ ( 𝐴 ‘ 𝑘 ) ) )
49 40 rpcnd ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
50 49 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
51 39 rpne0d ⊢ ( 𝑘 ∈ ℕ → ( 𝐴 ‘ 𝑘 ) ≠ 0 )
52 38 51 syl ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝐴 ‘ 𝑘 ) ≠ 0 )
53 52 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑘 ) ≠ 0 )
54 50 53 logcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( log ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℂ )
55 48 54 eqeltrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℂ )
56 32 33 34 35 37 55 telfsumo ⊢ ( 𝑁 ∈ ℕ → Σ 𝑗 ∈ ( 1 ..^ 𝑁 ) ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ ( 𝑗 + 1 ) ) ) = ( ( 𝐵 ‘ 1 ) − ( 𝐵 ‘ 𝑁 ) ) )
57 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
58 fzoval ⊢ ( 𝑁 ∈ ℤ → ( 1 ..^ 𝑁 ) = ( 1 ... ( 𝑁 − 1 ) ) )
59 57 58 syl ⊢ ( 𝑁 ∈ ℕ → ( 1 ..^ 𝑁 ) = ( 1 ... ( 𝑁 − 1 ) ) )
60 59 sumeq1d ⊢ ( 𝑁 ∈ ℕ → Σ 𝑗 ∈ ( 1 ..^ 𝑁 ) ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ ( 𝑗 + 1 ) ) ) = Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ ( 𝑗 + 1 ) ) ) )
61 56 60 eqtr3d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐵 ‘ 1 ) − ( 𝐵 ‘ 𝑁 ) ) = Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ ( 𝑗 + 1 ) ) ) )
62 fzfid ⊢ ( 𝑁 ∈ ℕ → ( 1 ... ( 𝑁 − 1 ) ) ∈ Fin )
63 elfznn ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑗 ∈ ℕ )
64 63 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑗 ∈ ℕ )
65 1 stirlinglem2 ⊢ ( 𝑗 ∈ ℕ → ( 𝐴 ‘ 𝑗 ) ∈ ℝ+ )
66 65 relogcld ⊢ ( 𝑗 ∈ ℕ → ( log ‘ ( 𝐴 ‘ 𝑗 ) ) ∈ ℝ )
67 nfcv ⊢ Ⅎ 𝑛 𝑗
68 11 67 nffv ⊢ Ⅎ 𝑛 ( 𝐴 ‘ 𝑗 )
69 9 68 nffv ⊢ Ⅎ 𝑛 ( log ‘ ( 𝐴 ‘ 𝑗 ) )
70 2fveq3 ⊢ ( 𝑛 = 𝑗 → ( log ‘ ( 𝐴 ‘ 𝑛 ) ) = ( log ‘ ( 𝐴 ‘ 𝑗 ) ) )
71 67 69 70 2 fvmptf ⊢ ( ( 𝑗 ∈ ℕ ∧ ( log ‘ ( 𝐴 ‘ 𝑗 ) ) ∈ ℝ ) → ( 𝐵 ‘ 𝑗 ) = ( log ‘ ( 𝐴 ‘ 𝑗 ) ) )
72 66 71 mpdan ⊢ ( 𝑗 ∈ ℕ → ( 𝐵 ‘ 𝑗 ) = ( log ‘ ( 𝐴 ‘ 𝑗 ) ) )
73 72 66 eqeltrd ⊢ ( 𝑗 ∈ ℕ → ( 𝐵 ‘ 𝑗 ) ∈ ℝ )
74 64 73 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝐵 ‘ 𝑗 ) ∈ ℝ )
75 peano2nn ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℕ )
76 1 stirlinglem2 ⊢ ( ( 𝑗 + 1 ) ∈ ℕ → ( 𝐴 ‘ ( 𝑗 + 1 ) ) ∈ ℝ+ )
77 75 76 syl ⊢ ( 𝑗 ∈ ℕ → ( 𝐴 ‘ ( 𝑗 + 1 ) ) ∈ ℝ+ )
78 77 relogcld ⊢ ( 𝑗 ∈ ℕ → ( log ‘ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ )
79 nfcv ⊢ Ⅎ 𝑛 ( 𝑗 + 1 )
80 11 79 nffv ⊢ Ⅎ 𝑛 ( 𝐴 ‘ ( 𝑗 + 1 ) )
81 9 80 nffv ⊢ Ⅎ 𝑛 ( log ‘ ( 𝐴 ‘ ( 𝑗 + 1 ) ) )
82 2fveq3 ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( log ‘ ( 𝐴 ‘ 𝑛 ) ) = ( log ‘ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) )
83 79 81 82 2 fvmptf ⊢ ( ( ( 𝑗 + 1 ) ∈ ℕ ∧ ( log ‘ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ ) → ( 𝐵 ‘ ( 𝑗 + 1 ) ) = ( log ‘ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) )
84 75 78 83 syl2anc ⊢ ( 𝑗 ∈ ℕ → ( 𝐵 ‘ ( 𝑗 + 1 ) ) = ( log ‘ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) )
85 84 78 eqeltrd ⊢ ( 𝑗 ∈ ℕ → ( 𝐵 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
86 63 85 syl ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 𝐵 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
87 86 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝐵 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
88 74 87 resubcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ )
89 62 88 fsumrecl ⊢ ( 𝑁 ∈ ℕ → Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ )
90 30 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 1 / 4 ) ∈ ℝ )
91 63 nnred ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑗 ∈ ℝ )
92 1red ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 1 ∈ ℝ )
93 91 92 readdcld ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 𝑗 + 1 ) ∈ ℝ )
94 91 93 remulcld ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 𝑗 · ( 𝑗 + 1 ) ) ∈ ℝ )
95 91 recnd ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑗 ∈ ℂ )
96 1cnd ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 1 ∈ ℂ )
97 95 96 addcld ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 𝑗 + 1 ) ∈ ℂ )
98 63 nnne0d ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑗 ≠ 0 )
99 75 nnne0d ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ≠ 0 )
100 63 99 syl ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 𝑗 + 1 ) ≠ 0 )
101 95 97 98 100 mulne0d ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 𝑗 · ( 𝑗 + 1 ) ) ≠ 0 )
102 94 101 rereccld ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ∈ ℝ )
103 102 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ∈ ℝ )
104 90 103 remulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 1 / 4 ) · ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ) ∈ ℝ )
105 62 104 fsumrecl ⊢ ( 𝑁 ∈ ℕ → Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 1 / 4 ) · ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ) ∈ ℝ )
106 eqid ⊢ ( 𝑖 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑖 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) ↑ ( 2 · 𝑖 ) ) ) ) = ( 𝑖 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑖 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) ↑ ( 2 · 𝑖 ) ) ) )
107 eqid ⊢ ( 𝑖 ∈ ℕ ↦ ( ( 1 / ( ( ( 2 · 𝑗 ) + 1 ) ↑ 2 ) ) ↑ 𝑖 ) ) = ( 𝑖 ∈ ℕ ↦ ( ( 1 / ( ( ( 2 · 𝑗 ) + 1 ) ↑ 2 ) ) ↑ 𝑖 ) )
108 1 2 106 107 stirlinglem10 ⊢ ( 𝑗 ∈ ℕ → ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ ( 𝑗 + 1 ) ) ) ≤ ( ( 1 / 4 ) · ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ) )
109 64 108 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ ( 𝑗 + 1 ) ) ) ≤ ( ( 1 / 4 ) · ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ) )
110 62 88 104 109 fsumle ⊢ ( 𝑁 ∈ ℕ → Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ ( 𝑗 + 1 ) ) ) ≤ Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 1 / 4 ) · ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ) )
111 62 103 fsumrecl ⊢ ( 𝑁 ∈ ℕ → Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ∈ ℝ )
112 1red ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℝ )
113 4pos ⊢ 0 < 4
114 28 113 elrpii ⊢ 4 ∈ ℝ+
115 114 a1i ⊢ ( 𝑁 ∈ ℕ → 4 ∈ ℝ+ )
116 0red ⊢ ( 𝑁 ∈ ℕ → 0 ∈ ℝ )
117 0lt1 ⊢ 0 < 1
118 117 a1i ⊢ ( 𝑁 ∈ ℕ → 0 < 1 )
119 116 112 118 ltled ⊢ ( 𝑁 ∈ ℕ → 0 ≤ 1 )
120 112 115 119 divge0d ⊢ ( 𝑁 ∈ ℕ → 0 ≤ ( 1 / 4 ) )
121 eqid ⊢ ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝑁 )
122 eluznn ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑗 ∈ ℕ )
123 3 a1i ⊢ ( 𝑗 ∈ ℕ → 𝐹 = ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
124 simpr ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑛 = 𝑗 ) → 𝑛 = 𝑗 )
125 124 oveq1d ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑛 = 𝑗 ) → ( 𝑛 + 1 ) = ( 𝑗 + 1 ) )
126 124 125 oveq12d ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑛 = 𝑗 ) → ( 𝑛 · ( 𝑛 + 1 ) ) = ( 𝑗 · ( 𝑗 + 1 ) ) )
127 126 oveq2d ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑛 = 𝑗 ) → ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) = ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) )
128 id ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℕ )
129 nnre ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℝ )
130 1red ⊢ ( 𝑗 ∈ ℕ → 1 ∈ ℝ )
131 129 130 readdcld ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℝ )
132 129 131 remulcld ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 · ( 𝑗 + 1 ) ) ∈ ℝ )
133 nncn ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℂ )
134 1cnd ⊢ ( 𝑗 ∈ ℕ → 1 ∈ ℂ )
135 133 134 addcld ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℂ )
136 nnne0 ⊢ ( 𝑗 ∈ ℕ → 𝑗 ≠ 0 )
137 133 135 136 99 mulne0d ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 · ( 𝑗 + 1 ) ) ≠ 0 )
138 132 137 rereccld ⊢ ( 𝑗 ∈ ℕ → ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ∈ ℝ )
139 123 127 128 138 fvmptd ⊢ ( 𝑗 ∈ ℕ → ( 𝐹 ‘ 𝑗 ) = ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) )
140 122 139 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑗 ) = ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) )
141 122 nnred ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑗 ∈ ℝ )
142 1red ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 1 ∈ ℝ )
143 141 142 readdcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑗 + 1 ) ∈ ℝ )
144 141 143 remulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑗 · ( 𝑗 + 1 ) ) ∈ ℝ )
145 141 recnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑗 ∈ ℂ )
146 1cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 1 ∈ ℂ )
147 145 146 addcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑗 + 1 ) ∈ ℂ )
148 122 nnne0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑗 ≠ 0 )
149 122 99 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑗 + 1 ) ≠ 0 )
150 145 147 148 149 mulne0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑗 · ( 𝑗 + 1 ) ) ≠ 0 )
151 144 150 rereccld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ∈ ℝ )
152 seqeq1 ⊢ ( 𝑁 = 1 → seq 𝑁 ( + , 𝐹 ) = seq 1 ( + , 𝐹 ) )
153 3 trireciplem ⊢ seq 1 ( + , 𝐹 ) ⇝ 1
154 climrel ⊢ Rel ⇝
155 154 releldmi ⊢ ( seq 1 ( + , 𝐹 ) ⇝ 1 → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
156 153 155 mp1i ⊢ ( 𝑁 = 1 → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
157 152 156 eqeltrd ⊢ ( 𝑁 = 1 → seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
158 157 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑁 = 1 ) → seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
159 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1 ) → 𝑁 ∈ ℕ )
160 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1 ) → ¬ 𝑁 = 1 )
161 elnn1uz2 ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) )
162 159 161 sylib ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1 ) → ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) )
163 162 ord ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1 ) → ( ¬ 𝑁 = 1 → 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) )
164 160 163 mpd ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1 ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
165 uz2m1nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 1 ) ∈ ℕ )
166 164 165 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1 ) → ( 𝑁 − 1 ) ∈ ℕ )
167 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
168 167 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 − 1 ) ∈ ℕ ) → 𝑁 ∈ ℂ )
169 1cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 − 1 ) ∈ ℕ ) → 1 ∈ ℂ )
170 168 169 npcand ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 − 1 ) ∈ ℕ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
171 170 eqcomd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 − 1 ) ∈ ℕ ) → 𝑁 = ( ( 𝑁 − 1 ) + 1 ) )
172 171 seqeq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 − 1 ) ∈ ℕ ) → seq 𝑁 ( + , 𝐹 ) = seq ( ( 𝑁 − 1 ) + 1 ) ( + , 𝐹 ) )
173 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
174 id ⊢ ( ( 𝑁 − 1 ) ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ )
175 138 recnd ⊢ ( 𝑗 ∈ ℕ → ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ∈ ℂ )
176 139 175 eqeltrd ⊢ ( 𝑗 ∈ ℕ → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
177 176 adantl ⊢ ( ( ( 𝑁 − 1 ) ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
178 153 a1i ⊢ ( ( 𝑁 − 1 ) ∈ ℕ → seq 1 ( + , 𝐹 ) ⇝ 1 )
179 173 174 177 178 clim2ser ⊢ ( ( 𝑁 − 1 ) ∈ ℕ → seq ( ( 𝑁 − 1 ) + 1 ) ( + , 𝐹 ) ⇝ ( 1 − ( seq 1 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ) )
180 179 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 − 1 ) ∈ ℕ ) → seq ( ( 𝑁 − 1 ) + 1 ) ( + , 𝐹 ) ⇝ ( 1 − ( seq 1 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ) )
181 172 180 eqbrtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 − 1 ) ∈ ℕ ) → seq 𝑁 ( + , 𝐹 ) ⇝ ( 1 − ( seq 1 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ) )
182 154 releldmi ⊢ ( seq 𝑁 ( + , 𝐹 ) ⇝ ( 1 − ( seq 1 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ) → seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
183 181 182 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 − 1 ) ∈ ℕ ) → seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
184 159 166 183 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1 ) → seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
185 158 184 pm2.61dan ⊢ ( 𝑁 ∈ ℕ → seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
186 121 57 140 151 185 isumrecl ⊢ ( 𝑁 ∈ ℕ → Σ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ∈ ℝ )
187 122 nnrpd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑗 ∈ ℝ+ )
188 187 rpge0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 ≤ 𝑗 )
189 141 188 ge0p1rpd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑗 + 1 ) ∈ ℝ+ )
190 187 189 rpmulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑗 · ( 𝑗 + 1 ) ) ∈ ℝ+ )
191 119 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 ≤ 1 )
192 142 190 191 divge0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 ≤ ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) )
193 121 57 140 151 185 192 isumge0 ⊢ ( 𝑁 ∈ ℕ → 0 ≤ Σ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) )
194 116 186 111 193 leadd2dd ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) + 0 ) ≤ ( Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) + Σ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ) )
195 111 recnd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ∈ ℂ )
196 195 addid1d ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) + 0 ) = Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) )
197 196 eqcomd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) = ( Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) + 0 ) )
198 id ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ )
199 139 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) = ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) )
200 133 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℂ )
201 1cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 1 ∈ ℂ )
202 200 201 addcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 𝑗 + 1 ) ∈ ℂ )
203 200 202 mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 𝑗 · ( 𝑗 + 1 ) ) ∈ ℂ )
204 136 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 𝑗 ≠ 0 )
205 99 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 𝑗 + 1 ) ≠ 0 )
206 200 202 204 205 mulne0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 𝑗 · ( 𝑗 + 1 ) ) ≠ 0 )
207 203 206 reccld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ∈ ℂ )
208 153 155 mp1i ⊢ ( 𝑁 ∈ ℕ → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
209 173 121 198 199 207 208 isumsplit ⊢ ( 𝑁 ∈ ℕ → Σ 𝑗 ∈ ℕ ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) = ( Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) + Σ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ) )
210 194 197 209 3brtr4d ⊢ ( 𝑁 ∈ ℕ → Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ≤ Σ 𝑗 ∈ ℕ ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) )
211 1zzd ⊢ ( ⊤ → 1 ∈ ℤ )
212 139 adantl ⊢ ( ( ⊤ ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) = ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) )
213 175 adantl ⊢ ( ( ⊤ ∧ 𝑗 ∈ ℕ ) → ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ∈ ℂ )
214 153 a1i ⊢ ( ⊤ → seq 1 ( + , 𝐹 ) ⇝ 1 )
215 173 211 212 213 214 isumclim ⊢ ( ⊤ → Σ 𝑗 ∈ ℕ ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) = 1 )
216 215 mptru ⊢ Σ 𝑗 ∈ ℕ ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) = 1
217 210 216 breqtrdi ⊢ ( 𝑁 ∈ ℕ → Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ≤ 1 )
218 111 112 31 120 217 lemul2ad ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / 4 ) · Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ) ≤ ( ( 1 / 4 ) · 1 ) )
219 4cn ⊢ 4 ∈ ℂ
220 219 a1i ⊢ ( 𝑁 ∈ ℕ → 4 ∈ ℂ )
221 113 a1i ⊢ ( 𝑁 ∈ ℕ → 0 < 4 )
222 221 gt0ne0d ⊢ ( 𝑁 ∈ ℕ → 4 ≠ 0 )
223 220 222 reccld ⊢ ( 𝑁 ∈ ℕ → ( 1 / 4 ) ∈ ℂ )
224 103 recnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ∈ ℂ )
225 62 223 224 fsummulc2 ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / 4 ) · Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ) = Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 1 / 4 ) · ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ) )
226 223 mulid1d ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / 4 ) · 1 ) = ( 1 / 4 ) )
227 218 225 226 3brtr3d ⊢ ( 𝑁 ∈ ℕ → Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 1 / 4 ) · ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ) ≤ ( 1 / 4 ) )
228 89 105 31 110 227 letrd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ ( 𝑗 + 1 ) ) ) ≤ ( 1 / 4 ) )
229 61 228 eqbrtrd ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐵 ‘ 1 ) − ( 𝐵 ‘ 𝑁 ) ) ≤ ( 1 / 4 ) )
230 18 27 31 229 subled ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐵 ‘ 1 ) − ( 1 / 4 ) ) ≤ ( 𝐵 ‘ 𝑁 ) )