Metamath Proof Explorer

Theorem stirlinglem10

Description: A bound for any B(N)-B(N + 1) that will allow to find a lower bound for the whole B sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem10.1 ⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
stirlinglem10.2 ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) )
stirlinglem10.4 ⊢ 𝐾 = ( 𝑘 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) )
stirlinglem10.5 ⊢ 𝐿 = ( 𝑘 ∈ ℕ ↦ ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑘 ) )
Assertion stirlinglem10 ( 𝑁 ∈ ℕ → ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) ≤ ( ( 1 / 4 ) · ( 1 / ( 𝑁 · ( 𝑁 + 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 stirlinglem10.1 ⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
2 stirlinglem10.2 ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) )
3 stirlinglem10.4 ⊢ 𝐾 = ( 𝑘 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) )
4 stirlinglem10.5 ⊢ 𝐿 = ( 𝑘 ∈ ℕ ↦ ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑘 ) )
5 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
6 1zzd ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℤ )
7 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( ( 1 + ( 2 · 𝑛 ) ) / 2 ) · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − 1 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( ( 1 + ( 2 · 𝑛 ) ) / 2 ) · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − 1 ) )
8 1 2 7 3 stirlinglem9 ⊢ ( 𝑁 ∈ ℕ → seq 1 ( + , 𝐾 ) ⇝ ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) )
9 2cnd ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
10 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
11 9 10 mulcld ⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) ∈ ℂ )
12 1cnd ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
13 11 12 addcld ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ )
14 13 sqcld ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ∈ ℂ )
15 0red ⊢ ( 𝑁 ∈ ℕ → 0 ∈ ℝ )
16 1red ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℝ )
17 2re ⊢ 2 ∈ ℝ
18 17 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ )
19 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
20 18 19 remulcld ⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) ∈ ℝ )
21 20 16 readdcld ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ )
22 0lt1 ⊢ 0 < 1
23 22 a1i ⊢ ( 𝑁 ∈ ℕ → 0 < 1 )
24 2rp ⊢ 2 ∈ ℝ+
25 24 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ+ )
26 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
27 25 26 rpmulcld ⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) ∈ ℝ+ )
28 16 27 ltaddrp2d ⊢ ( 𝑁 ∈ ℕ → 1 < ( ( 2 · 𝑁 ) + 1 ) )
29 15 16 21 23 28 lttrd ⊢ ( 𝑁 ∈ ℕ → 0 < ( ( 2 · 𝑁 ) + 1 ) )
30 29 gt0ne0d ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) + 1 ) ≠ 0 )
31 2z ⊢ 2 ∈ ℤ
32 31 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℤ )
33 13 30 32 expne0d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ≠ 0 )
34 14 33 reccld ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ∈ ℂ )
35 16 renegcld ⊢ ( 𝑁 ∈ ℕ → - 1 ∈ ℝ )
36 21 resqcld ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ∈ ℝ )
37 36 33 rereccld ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ∈ ℝ )
38 1re ⊢ 1 ∈ ℝ
39 lt0neg2 ⊢ ( 1 ∈ ℝ → ( 0 < 1 ↔ - 1 < 0 ) )
40 38 39 ax-mp ⊢ ( 0 < 1 ↔ - 1 < 0 )
41 23 40 sylib ⊢ ( 𝑁 ∈ ℕ → - 1 < 0 )
42 21 30 sqgt0d ⊢ ( 𝑁 ∈ ℕ → 0 < ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) )
43 36 42 recgt0d ⊢ ( 𝑁 ∈ ℕ → 0 < ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) )
44 35 15 37 41 43 lttrd ⊢ ( 𝑁 ∈ ℕ → - 1 < ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) )
45 2nn ⊢ 2 ∈ ℕ
46 45 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℕ )
47 expgt1 ⊢ ( ( ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ ∧ 2 ∈ ℕ ∧ 1 < ( ( 2 · 𝑁 ) + 1 ) ) → 1 < ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) )
48 21 46 28 47 syl3anc ⊢ ( 𝑁 ∈ ℕ → 1 < ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) )
49 36 42 elrpd ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ∈ ℝ+ )
50 49 recgt1d ⊢ ( 𝑁 ∈ ℕ → ( 1 < ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ↔ ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) < 1 ) )
51 48 50 mpbid ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) < 1 )
52 37 16 absltd ⊢ ( 𝑁 ∈ ℕ → ( ( abs ‘ ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ) < 1 ↔ ( - 1 < ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ∧ ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) < 1 ) ) )
53 44 51 52 mpbir2and ⊢ ( 𝑁 ∈ ℕ → ( abs ‘ ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ) < 1 )
54 1nn0 ⊢ 1 ∈ ℕ0
55 54 a1i ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℕ0 )
56 4 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 1 ) ) → 𝐿 = ( 𝑘 ∈ ℕ ↦ ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑘 ) ) )
57 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑘 = 𝑗 ) → 𝑘 = 𝑗 )
58 57 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑘 = 𝑗 ) → ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑘 ) = ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑗 ) )
59 elnnuz ⊢ ( 𝑗 ∈ ℕ ↔ 𝑗 ∈ ( ℤ≥ ‘ 1 ) )
60 59 biimpri ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 1 ) → 𝑗 ∈ ℕ )
61 60 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 1 ) ) → 𝑗 ∈ ℕ )
62 34 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 1 ) ) → ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ∈ ℂ )
63 61 nnnn0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 1 ) ) → 𝑗 ∈ ℕ0 )
64 62 63 expcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 1 ) ) → ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑗 ) ∈ ℂ )
65 56 58 61 64 fvmptd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 1 ) ) → ( 𝐿 ‘ 𝑗 ) = ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑗 ) )
66 34 53 55 65 geolim2 ⊢ ( 𝑁 ∈ ℕ → seq 1 ( + , 𝐿 ) ⇝ ( ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 1 ) / ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ) ) )
67 34 exp1d ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 1 ) = ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) )
68 14 33 dividd ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) = 1 )
69 68 eqcomd ⊢ ( 𝑁 ∈ ℕ → 1 = ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) )
70 69 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ) = ( ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) − ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ) )
71 49 rpcnne0d ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ∈ ℂ ∧ ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ≠ 0 ) )
72 divsubdir ⊢ ( ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ∈ ℂ ∧ ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ≠ 0 ) ) → ( ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) − 1 ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) = ( ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) − ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ) )
73 14 12 71 72 syl3anc ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) − 1 ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) = ( ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) − ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ) )
74 ax-1cn ⊢ 1 ∈ ℂ
75 binom2 ⊢ ( ( ( 2 · 𝑁 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) = ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( ( 2 · 𝑁 ) · 1 ) ) ) + ( 1 ↑ 2 ) ) )
76 11 74 75 sylancl ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) = ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( ( 2 · 𝑁 ) · 1 ) ) ) + ( 1 ↑ 2 ) ) )
77 76 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) − 1 ) = ( ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( ( 2 · 𝑁 ) · 1 ) ) ) + ( 1 ↑ 2 ) ) − 1 ) )
78 9 10 sqmuld ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( 𝑁 ↑ 2 ) ) )
79 sq2 ⊢ ( 2 ↑ 2 ) = 4
80 79 a1i ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ 2 ) = 4 )
81 80 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 2 ↑ 2 ) · ( 𝑁 ↑ 2 ) ) = ( 4 · ( 𝑁 ↑ 2 ) ) )
82 78 81 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) ↑ 2 ) = ( 4 · ( 𝑁 ↑ 2 ) ) )
83 11 mulridd ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) · 1 ) = ( 2 · 𝑁 ) )
84 83 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( 2 · ( ( 2 · 𝑁 ) · 1 ) ) = ( 2 · ( 2 · 𝑁 ) ) )
85 9 9 10 mulassd ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 2 ) · 𝑁 ) = ( 2 · ( 2 · 𝑁 ) ) )
86 2t2e4 ⊢ ( 2 · 2 ) = 4
87 86 a1i ⊢ ( 𝑁 ∈ ℕ → ( 2 · 2 ) = 4 )
88 87 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 2 ) · 𝑁 ) = ( 4 · 𝑁 ) )
89 84 85 88 3eqtr2d ⊢ ( 𝑁 ∈ ℕ → ( 2 · ( ( 2 · 𝑁 ) · 1 ) ) = ( 4 · 𝑁 ) )
90 82 89 oveq12d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( ( 2 · 𝑁 ) · 1 ) ) ) = ( ( 4 · ( 𝑁 ↑ 2 ) ) + ( 4 · 𝑁 ) ) )
91 4cn ⊢ 4 ∈ ℂ
92 91 a1i ⊢ ( 𝑁 ∈ ℕ → 4 ∈ ℂ )
93 10 sqcld ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ↑ 2 ) ∈ ℂ )
94 92 93 10 adddid ⊢ ( 𝑁 ∈ ℕ → ( 4 · ( ( 𝑁 ↑ 2 ) + 𝑁 ) ) = ( ( 4 · ( 𝑁 ↑ 2 ) ) + ( 4 · 𝑁 ) ) )
95 10 sqvald ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ↑ 2 ) = ( 𝑁 · 𝑁 ) )
96 10 mulridd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 · 1 ) = 𝑁 )
97 96 eqcomd ⊢ ( 𝑁 ∈ ℕ → 𝑁 = ( 𝑁 · 1 ) )
98 95 97 oveq12d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 ↑ 2 ) + 𝑁 ) = ( ( 𝑁 · 𝑁 ) + ( 𝑁 · 1 ) ) )
99 10 10 12 adddid ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 · ( 𝑁 + 1 ) ) = ( ( 𝑁 · 𝑁 ) + ( 𝑁 · 1 ) ) )
100 98 99 eqtr4d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 ↑ 2 ) + 𝑁 ) = ( 𝑁 · ( 𝑁 + 1 ) ) )
101 100 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( 4 · ( ( 𝑁 ↑ 2 ) + 𝑁 ) ) = ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) )
102 90 94 101 3eqtr2d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( ( 2 · 𝑁 ) · 1 ) ) ) = ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) )
103 sq1 ⊢ ( 1 ↑ 2 ) = 1
104 103 a1i ⊢ ( 𝑁 ∈ ℕ → ( 1 ↑ 2 ) = 1 )
105 102 104 oveq12d ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( ( 2 · 𝑁 ) · 1 ) ) ) + ( 1 ↑ 2 ) ) = ( ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) + 1 ) )
106 105 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( ( 2 · 𝑁 ) · 1 ) ) ) + ( 1 ↑ 2 ) ) − 1 ) = ( ( ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) + 1 ) − 1 ) )
107 10 12 addcld ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℂ )
108 10 107 mulcld ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 · ( 𝑁 + 1 ) ) ∈ ℂ )
109 92 108 mulcld ⊢ ( 𝑁 ∈ ℕ → ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) ∈ ℂ )
110 109 12 pncand ⊢ ( 𝑁 ∈ ℕ → ( ( ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) + 1 ) − 1 ) = ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) )
111 77 106 110 3eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) − 1 ) = ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) )
112 111 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) − 1 ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) = ( ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) )
113 70 73 112 3eqtr2d ⊢ ( 𝑁 ∈ ℕ → ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ) = ( ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) )
114 67 113 oveq12d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 1 ) / ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ) ) = ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) / ( ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ) )
115 4pos ⊢ 0 < 4
116 115 a1i ⊢ ( 𝑁 ∈ ℕ → 0 < 4 )
117 116 gt0ne0d ⊢ ( 𝑁 ∈ ℕ → 4 ≠ 0 )
118 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
119 19 16 readdcld ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℝ )
120 nngt0 ⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
121 19 ltp1d ⊢ ( 𝑁 ∈ ℕ → 𝑁 < ( 𝑁 + 1 ) )
122 15 19 119 120 121 lttrd ⊢ ( 𝑁 ∈ ℕ → 0 < ( 𝑁 + 1 ) )
123 122 gt0ne0d ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ≠ 0 )
124 10 107 118 123 mulne0d ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 · ( 𝑁 + 1 ) ) ≠ 0 )
125 92 108 117 124 mulne0d ⊢ ( 𝑁 ∈ ℕ → ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) ≠ 0 )
126 12 14 109 14 33 33 125 divdivdivd ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) / ( ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ) = ( ( 1 · ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) / ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) · ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) ) ) )
127 12 14 mulcomd ⊢ ( 𝑁 ∈ ℕ → ( 1 · ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) · 1 ) )
128 127 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 1 · ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) / ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) · ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) ) ) = ( ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) · 1 ) / ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) · ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) ) ) )
129 12 mulridd ⊢ ( 𝑁 ∈ ℕ → ( 1 · 1 ) = 1 )
130 129 eqcomd ⊢ ( 𝑁 ∈ ℕ → 1 = ( 1 · 1 ) )
131 130 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) ) = ( ( 1 · 1 ) / ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) ) )
132 12 92 12 108 117 124 divmuldivd ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / 4 ) · ( 1 / ( 𝑁 · ( 𝑁 + 1 ) ) ) ) = ( ( 1 · 1 ) / ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) ) )
133 131 132 eqtr4d ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) ) = ( ( 1 / 4 ) · ( 1 / ( 𝑁 · ( 𝑁 + 1 ) ) ) ) )
134 68 133 oveq12d ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) · ( 1 / ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) ) ) = ( 1 · ( ( 1 / 4 ) · ( 1 / ( 𝑁 · ( 𝑁 + 1 ) ) ) ) ) )
135 14 14 12 109 33 125 divmuldivd ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) · ( 1 / ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) ) ) = ( ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) · 1 ) / ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) · ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) ) ) )
136 92 117 reccld ⊢ ( 𝑁 ∈ ℕ → ( 1 / 4 ) ∈ ℂ )
137 108 124 reccld ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( 𝑁 · ( 𝑁 + 1 ) ) ) ∈ ℂ )
138 136 137 mulcld ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / 4 ) · ( 1 / ( 𝑁 · ( 𝑁 + 1 ) ) ) ) ∈ ℂ )
139 138 mullidd ⊢ ( 𝑁 ∈ ℕ → ( 1 · ( ( 1 / 4 ) · ( 1 / ( 𝑁 · ( 𝑁 + 1 ) ) ) ) ) = ( ( 1 / 4 ) · ( 1 / ( 𝑁 · ( 𝑁 + 1 ) ) ) ) )
140 134 135 139 3eqtr3d ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) · 1 ) / ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) · ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) ) ) = ( ( 1 / 4 ) · ( 1 / ( 𝑁 · ( 𝑁 + 1 ) ) ) ) )
141 126 128 140 3eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) / ( ( 4 · ( 𝑁 · ( 𝑁 + 1 ) ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ) = ( ( 1 / 4 ) · ( 1 / ( 𝑁 · ( 𝑁 + 1 ) ) ) ) )
142 114 141 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 1 ) / ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ) ) = ( ( 1 / 4 ) · ( 1 / ( 𝑁 · ( 𝑁 + 1 ) ) ) ) )
143 66 142 breqtrd ⊢ ( 𝑁 ∈ ℕ → seq 1 ( + , 𝐿 ) ⇝ ( ( 1 / 4 ) · ( 1 / ( 𝑁 · ( 𝑁 + 1 ) ) ) ) )
144 59 biimpi ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ( ℤ≥ ‘ 1 ) )
145 144 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ( ℤ≥ ‘ 1 ) )
146 oveq2 ⊢ ( 𝑘 = 𝑛 → ( 2 · 𝑘 ) = ( 2 · 𝑛 ) )
147 146 oveq1d ⊢ ( 𝑘 = 𝑛 → ( ( 2 · 𝑘 ) + 1 ) = ( ( 2 · 𝑛 ) + 1 ) )
148 147 oveq2d ⊢ ( 𝑘 = 𝑛 → ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) = ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) )
149 146 oveq2d ⊢ ( 𝑘 = 𝑛 → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) = ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) )
150 148 149 oveq12d ⊢ ( 𝑘 = 𝑛 → ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ) )
151 elfznn ⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → 𝑛 ∈ ℕ )
152 151 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 𝑛 ∈ ℕ )
153 2cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 2 ∈ ℂ )
154 152 nncnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 𝑛 ∈ ℂ )
155 153 154 mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 2 · 𝑛 ) ∈ ℂ )
156 1cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 1 ∈ ℂ )
157 155 156 addcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℂ )
158 0red ⊢ ( 𝑛 ∈ ℕ → 0 ∈ ℝ )
159 1red ⊢ ( 𝑛 ∈ ℕ → 1 ∈ ℝ )
160 17 a1i ⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℝ )
161 nnre ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
162 160 161 remulcld ⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℝ )
163 162 159 readdcld ⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) + 1 ) ∈ ℝ )
164 22 a1i ⊢ ( 𝑛 ∈ ℕ → 0 < 1 )
165 24 a1i ⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℝ+ )
166 nnrp ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
167 165 166 rpmulcld ⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℝ+ )
168 159 167 ltaddrp2d ⊢ ( 𝑛 ∈ ℕ → 1 < ( ( 2 · 𝑛 ) + 1 ) )
169 158 159 163 164 168 lttrd ⊢ ( 𝑛 ∈ ℕ → 0 < ( ( 2 · 𝑛 ) + 1 ) )
170 151 169 syl ⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → 0 < ( ( 2 · 𝑛 ) + 1 ) )
171 170 gt0ne0d ⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → ( ( 2 · 𝑛 ) + 1 ) ≠ 0 )
172 171 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 2 · 𝑛 ) + 1 ) ≠ 0 )
173 157 172 reccld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℂ )
174 10 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 𝑁 ∈ ℂ )
175 153 174 mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 2 · 𝑁 ) ∈ ℂ )
176 175 156 addcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ )
177 30 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 2 · 𝑁 ) + 1 ) ≠ 0 )
178 176 177 reccld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℂ )
179 2nn0 ⊢ 2 ∈ ℕ0
180 179 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 2 ∈ ℕ0 )
181 152 nnnn0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 𝑛 ∈ ℕ0 )
182 180 181 nn0mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 2 · 𝑛 ) ∈ ℕ0 )
183 178 182 expcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ∈ ℂ )
184 173 183 mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ) ∈ ℂ )
185 3 150 152 184 fvmptd3 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 𝐾 ‘ 𝑛 ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ) )
186 185 adantlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 𝐾 ‘ 𝑛 ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ) )
187 169 gt0ne0d ⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) + 1 ) ≠ 0 )
188 163 187 rereccld ⊢ ( 𝑛 ∈ ℕ → ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℝ )
189 151 188 syl ⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℝ )
190 189 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℝ )
191 21 30 rereccld ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℝ )
192 191 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℝ )
193 192 182 reexpcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ∈ ℝ )
194 193 adantlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ∈ ℝ )
195 190 194 remulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ) ∈ ℝ )
196 186 195 eqeltrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 𝐾 ‘ 𝑛 ) ∈ ℝ )
197 readdcl ⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑖 ∈ ℝ ) → ( 𝑛 + 𝑖 ) ∈ ℝ )
198 197 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑖 ∈ ℝ ) ) → ( 𝑛 + 𝑖 ) ∈ ℝ )
199 145 196 198 seqcl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐾 ) ‘ 𝑗 ) ∈ ℝ )
200 oveq2 ⊢ ( 𝑘 = 𝑛 → ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑘 ) = ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑛 ) )
201 34 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ∈ ℂ )
202 201 181 expcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑛 ) ∈ ℂ )
203 4 200 152 202 fvmptd3 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 𝐿 ‘ 𝑛 ) = ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑛 ) )
204 37 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ∈ ℝ )
205 204 181 reexpcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑛 ) ∈ ℝ )
206 203 205 eqeltrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 𝐿 ‘ 𝑛 ) ∈ ℝ )
207 206 adantlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 𝐿 ‘ 𝑛 ) ∈ ℝ )
208 145 207 198 seqcl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐿 ) ‘ 𝑗 ) ∈ ℝ )
209 31 a1i ⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → 2 ∈ ℤ )
210 elfzelz ⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → 𝑛 ∈ ℤ )
211 209 210 zmulcld ⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → ( 2 · 𝑛 ) ∈ ℤ )
212 1exp ⊢ ( ( 2 · 𝑛 ) ∈ ℤ → ( 1 ↑ ( 2 · 𝑛 ) ) = 1 )
213 211 212 syl ⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → ( 1 ↑ ( 2 · 𝑛 ) ) = 1 )
214 1exp ⊢ ( 𝑛 ∈ ℤ → ( 1 ↑ 𝑛 ) = 1 )
215 210 214 syl ⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → ( 1 ↑ 𝑛 ) = 1 )
216 213 215 eqtr4d ⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → ( 1 ↑ ( 2 · 𝑛 ) ) = ( 1 ↑ 𝑛 ) )
217 216 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 ↑ ( 2 · 𝑛 ) ) = ( 1 ↑ 𝑛 ) )
218 176 181 180 expmuld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ↑ 𝑛 ) )
219 217 218 oveq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 ↑ ( 2 · 𝑛 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) = ( ( 1 ↑ 𝑛 ) / ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ↑ 𝑛 ) ) )
220 156 176 177 182 expdivd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) = ( ( 1 ↑ ( 2 · 𝑛 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) )
221 176 sqcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ∈ ℂ )
222 31 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 2 ∈ ℤ )
223 176 177 222 expne0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ≠ 0 )
224 156 221 223 181 expdivd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑛 ) = ( ( 1 ↑ 𝑛 ) / ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ↑ 𝑛 ) ) )
225 219 220 224 3eqtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) = ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑛 ) )
226 225 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑛 ) ) )
227 1rp ⊢ 1 ∈ ℝ+
228 227 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 1 ∈ ℝ+ )
229 17 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 2 ∈ ℝ )
230 152 nnred ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 𝑛 ∈ ℝ )
231 229 230 remulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 2 · 𝑛 ) ∈ ℝ )
232 180 nn0ge0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 0 ≤ 2 )
233 181 nn0ge0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 0 ≤ 𝑛 )
234 229 230 232 233 mulge0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 0 ≤ ( 2 · 𝑛 ) )
235 231 234 ge0p1rpd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℝ+ )
236 1red ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 1 ∈ ℝ )
237 228 rpge0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 0 ≤ 1 )
238 159 163 168 ltled ⊢ ( 𝑛 ∈ ℕ → 1 ≤ ( ( 2 · 𝑛 ) + 1 ) )
239 151 238 syl ⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → 1 ≤ ( ( 2 · 𝑛 ) + 1 ) )
240 239 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 1 ≤ ( ( 2 · 𝑛 ) + 1 ) )
241 228 235 236 237 240 lediv2ad ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ≤ ( 1 / 1 ) )
242 156 div1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 / 1 ) = 1 )
243 241 242 breqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ≤ 1 )
244 152 188 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℝ )
245 19 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 𝑁 ∈ ℝ )
246 229 245 remulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 2 · 𝑁 ) ∈ ℝ )
247 15 19 120 ltled ⊢ ( 𝑁 ∈ ℕ → 0 ≤ 𝑁 )
248 247 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 0 ≤ 𝑁 )
249 229 245 232 248 mulge0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 0 ≤ ( 2 · 𝑁 ) )
250 246 249 ge0p1rpd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ+ )
251 250 222 rpexpcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ∈ ℝ+ )
252 251 rpreccld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ∈ ℝ+ )
253 210 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 𝑛 ∈ ℤ )
254 252 253 rpexpcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑛 ) ∈ ℝ+ )
255 244 236 254 lemul1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ≤ 1 ↔ ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑛 ) ) ≤ ( 1 · ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑛 ) ) ) )
256 243 255 mpbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑛 ) ) ≤ ( 1 · ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑛 ) ) )
257 202 mullidd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 · ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑛 ) ) = ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑛 ) )
258 256 257 breqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑛 ) ) ≤ ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑛 ) )
259 226 258 eqbrtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ) ≤ ( ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) ) ↑ 𝑛 ) )
260 259 185 203 3brtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 𝐾 ‘ 𝑛 ) ≤ ( 𝐿 ‘ 𝑛 ) )
261 260 adantlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 𝐾 ‘ 𝑛 ) ≤ ( 𝐿 ‘ 𝑛 ) )
262 145 196 207 261 serle ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐾 ) ‘ 𝑗 ) ≤ ( seq 1 ( + , 𝐿 ) ‘ 𝑗 ) )
263 5 6 8 143 199 208 262 climle ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) ≤ ( ( 1 / 4 ) · ( 1 / ( 𝑁 · ( 𝑁 + 1 ) ) ) ) )