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