Theorem stirlinglem11

Description: B is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	stirlinglem11.1	⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
	stirlinglem11.2	⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) )
	stirlinglem11.3	⊢ 𝐾 = ( 𝑘 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) )
Assertion	stirlinglem11	⊢ ( 𝑁 ∈ ℕ → ( 𝐵 ‘ ( 𝑁 + 1 ) ) < ( 𝐵 ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		stirlinglem11.1	⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
2		stirlinglem11.2	⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) )
3		stirlinglem11.3	⊢ 𝐾 = ( 𝑘 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) )
4		0red	⊢ ( 𝑁 ∈ ℕ → 0 ∈ ℝ )
5	3	a1i	⊢ ( 𝑁 ∈ ℕ → 𝐾 = ( 𝑘 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) ) )
6		simpr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 = 1 ) → 𝑘 = 1 )
7	6	oveq2d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 = 1 ) → ( 2 · 𝑘 ) = ( 2 · 1 ) )
8	7	oveq1d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 = 1 ) → ( ( 2 · 𝑘 ) + 1 ) = ( ( 2 · 1 ) + 1 ) )
9	8	oveq2d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 = 1 ) → ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) = ( 1 / ( ( 2 · 1 ) + 1 ) ) )
10	7	oveq2d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 = 1 ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) = ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 1 ) ) )
11	9 10	oveq12d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 = 1 ) → ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) = ( ( 1 / ( ( 2 · 1 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 1 ) ) ) )
12		1nn	⊢ 1 ∈ ℕ
13	12	a1i	⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℕ )
14		2cnd	⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
15		1cnd	⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
16	14 15	mulcld	⊢ ( 𝑁 ∈ ℕ → ( 2 · 1 ) ∈ ℂ )
17	16 15	addcld	⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 1 ) + 1 ) ∈ ℂ )
18		2t1e2	⊢ ( 2 · 1 ) = 2
19	18	oveq1i	⊢ ( ( 2 · 1 ) + 1 ) = ( 2 + 1 )
20		2p1e3	⊢ ( 2 + 1 ) = 3
21	19 20	eqtri	⊢ ( ( 2 · 1 ) + 1 ) = 3
22		3ne0	⊢ 3 ≠ 0
23	21 22	eqnetri	⊢ ( ( 2 · 1 ) + 1 ) ≠ 0
24	23	a1i	⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 1 ) + 1 ) ≠ 0 )
25	17 24	reccld	⊢ ( 𝑁 ∈ ℕ → ( 1 / ( ( 2 · 1 ) + 1 ) ) ∈ ℂ )
26		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
27	14 26	mulcld	⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) ∈ ℂ )
28	27 15	addcld	⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ )
29		1red	⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℝ )
30		2re	⊢ 2 ∈ ℝ
31	30	a1i	⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ )
32		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
33	31 32	remulcld	⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) ∈ ℝ )
34	33 29	readdcld	⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ )
35		0lt1	⊢ 0 < 1
36	35	a1i	⊢ ( 𝑁 ∈ ℕ → 0 < 1 )
37		2rp	⊢ 2 ∈ ℝ+
38	37	a1i	⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ+ )
39		nnrp	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
40	38 39	rpmulcld	⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) ∈ ℝ+ )
41	29 40	ltaddrp2d	⊢ ( 𝑁 ∈ ℕ → 1 < ( ( 2 · 𝑁 ) + 1 ) )
42	4 29 34 36 41	lttrd	⊢ ( 𝑁 ∈ ℕ → 0 < ( ( 2 · 𝑁 ) + 1 ) )
43	42	gt0ne0d	⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) + 1 ) ≠ 0 )
44	28 43	reccld	⊢ ( 𝑁 ∈ ℕ → ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℂ )
45		2nn0	⊢ 2 ∈ ℕ0
46	45	a1i	⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℕ0 )
47		1nn0	⊢ 1 ∈ ℕ0
48	47	a1i	⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℕ0 )
49	46 48	nn0mulcld	⊢ ( 𝑁 ∈ ℕ → ( 2 · 1 ) ∈ ℕ0 )
50	44 49	expcld	⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 1 ) ) ∈ ℂ )
51	25 50	mulcld	⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( 2 · 1 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 1 ) ) ) ∈ ℂ )
52	5 11 13 51	fvmptd	⊢ ( 𝑁 ∈ ℕ → ( 𝐾 ‘ 1 ) = ( ( 1 / ( ( 2 · 1 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 1 ) ) ) )
53		1re	⊢ 1 ∈ ℝ
54	30 53	remulcli	⊢ ( 2 · 1 ) ∈ ℝ
55	54 53	readdcli	⊢ ( ( 2 · 1 ) + 1 ) ∈ ℝ
56	55 23	rereccli	⊢ ( 1 / ( ( 2 · 1 ) + 1 ) ) ∈ ℝ
57	56	a1i	⊢ ( 𝑁 ∈ ℕ → ( 1 / ( ( 2 · 1 ) + 1 ) ) ∈ ℝ )
58	34 43	rereccld	⊢ ( 𝑁 ∈ ℕ → ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℝ )
59	58 49	reexpcld	⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 1 ) ) ∈ ℝ )
60	57 59	remulcld	⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( 2 · 1 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 1 ) ) ) ∈ ℝ )
61	52 60	eqeltrd	⊢ ( 𝑁 ∈ ℕ → ( 𝐾 ‘ 1 ) ∈ ℝ )
62	1	stirlinglem2	⊢ ( 𝑁 ∈ ℕ → ( 𝐴 ‘ 𝑁 ) ∈ ℝ+ )
63	62	relogcld	⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( 𝐴 ‘ 𝑁 ) ) ∈ ℝ )
64		nfcv	⊢ Ⅎ 𝑛 𝑁
65		nfcv	⊢ Ⅎ 𝑛 log
66		nfmpt1	⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
67	1 66	nfcxfr	⊢ Ⅎ 𝑛 𝐴
68	67 64	nffv	⊢ Ⅎ 𝑛 ( 𝐴 ‘ 𝑁 )
69	65 68	nffv	⊢ Ⅎ 𝑛 ( log ‘ ( 𝐴 ‘ 𝑁 ) )
70		2fveq3	⊢ ( 𝑛 = 𝑁 → ( log ‘ ( 𝐴 ‘ 𝑛 ) ) = ( log ‘ ( 𝐴 ‘ 𝑁 ) ) )
71	64 69 70 2	fvmptf	⊢ ( ( 𝑁 ∈ ℕ ∧ ( log ‘ ( 𝐴 ‘ 𝑁 ) ) ∈ ℝ ) → ( 𝐵 ‘ 𝑁 ) = ( log ‘ ( 𝐴 ‘ 𝑁 ) ) )
72	63 71	mpdan	⊢ ( 𝑁 ∈ ℕ → ( 𝐵 ‘ 𝑁 ) = ( log ‘ ( 𝐴 ‘ 𝑁 ) ) )
73	72 63	eqeltrd	⊢ ( 𝑁 ∈ ℕ → ( 𝐵 ‘ 𝑁 ) ∈ ℝ )
74		peano2nn	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ )
75	1	stirlinglem2	⊢ ( ( 𝑁 + 1 ) ∈ ℕ → ( 𝐴 ‘ ( 𝑁 + 1 ) ) ∈ ℝ+ )
76	74 75	syl	⊢ ( 𝑁 ∈ ℕ → ( 𝐴 ‘ ( 𝑁 + 1 ) ) ∈ ℝ+ )
77	76	relogcld	⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( 𝐴 ‘ ( 𝑁 + 1 ) ) ) ∈ ℝ )
78		nfcv	⊢ Ⅎ 𝑛 ( 𝑁 + 1 )
79	67 78	nffv	⊢ Ⅎ 𝑛 ( 𝐴 ‘ ( 𝑁 + 1 ) )
80	65 79	nffv	⊢ Ⅎ 𝑛 ( log ‘ ( 𝐴 ‘ ( 𝑁 + 1 ) ) )
81		2fveq3	⊢ ( 𝑛 = ( 𝑁 + 1 ) → ( log ‘ ( 𝐴 ‘ 𝑛 ) ) = ( log ‘ ( 𝐴 ‘ ( 𝑁 + 1 ) ) ) )
82	78 80 81 2	fvmptf	⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ ∧ ( log ‘ ( 𝐴 ‘ ( 𝑁 + 1 ) ) ) ∈ ℝ ) → ( 𝐵 ‘ ( 𝑁 + 1 ) ) = ( log ‘ ( 𝐴 ‘ ( 𝑁 + 1 ) ) ) )
83	74 77 82	syl2anc	⊢ ( 𝑁 ∈ ℕ → ( 𝐵 ‘ ( 𝑁 + 1 ) ) = ( log ‘ ( 𝐴 ‘ ( 𝑁 + 1 ) ) ) )
84	83 77	eqeltrd	⊢ ( 𝑁 ∈ ℕ → ( 𝐵 ‘ ( 𝑁 + 1 ) ) ∈ ℝ )
85	73 84	resubcld	⊢ ( 𝑁 ∈ ℕ → ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) ∈ ℝ )
86	31 29	remulcld	⊢ ( 𝑁 ∈ ℕ → ( 2 · 1 ) ∈ ℝ )
87		0le2	⊢ 0 ≤ 2
88	87	a1i	⊢ ( 𝑁 ∈ ℕ → 0 ≤ 2 )
89		0le1	⊢ 0 ≤ 1
90	89	a1i	⊢ ( 𝑁 ∈ ℕ → 0 ≤ 1 )
91	31 29 88 90	mulge0d	⊢ ( 𝑁 ∈ ℕ → 0 ≤ ( 2 · 1 ) )
92	86 91	ge0p1rpd	⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 1 ) + 1 ) ∈ ℝ+ )
93	92	rpreccld	⊢ ( 𝑁 ∈ ℕ → ( 1 / ( ( 2 · 1 ) + 1 ) ) ∈ ℝ+ )
94	39	rpge0d	⊢ ( 𝑁 ∈ ℕ → 0 ≤ 𝑁 )
95	31 32 88 94	mulge0d	⊢ ( 𝑁 ∈ ℕ → 0 ≤ ( 2 · 𝑁 ) )
96	33 95	ge0p1rpd	⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ+ )
97	96	rpreccld	⊢ ( 𝑁 ∈ ℕ → ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℝ+ )
98		2z	⊢ 2 ∈ ℤ
99	98	a1i	⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℤ )
100		1z	⊢ 1 ∈ ℤ
101	100	a1i	⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℤ )
102	99 101	zmulcld	⊢ ( 𝑁 ∈ ℕ → ( 2 · 1 ) ∈ ℤ )
103	97 102	rpexpcld	⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 1 ) ) ∈ ℝ+ )
104	93 103	rpmulcld	⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( 2 · 1 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 1 ) ) ) ∈ ℝ+ )
105	52 104	eqeltrd	⊢ ( 𝑁 ∈ ℕ → ( 𝐾 ‘ 1 ) ∈ ℝ+ )
106	105	rpgt0d	⊢ ( 𝑁 ∈ ℕ → 0 < ( 𝐾 ‘ 1 ) )
107	85 61	resubcld	⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) − ( 𝐾 ‘ 1 ) ) ∈ ℝ )
108		eqid	⊢ ( ℤ≥ ‘ ( 1 + 1 ) ) = ( ℤ≥ ‘ ( 1 + 1 ) )
109	101	peano2zd	⊢ ( 𝑁 ∈ ℕ → ( 1 + 1 ) ∈ ℤ )
110		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
111	3	a1i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 𝐾 = ( 𝑘 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) ) )
112		oveq2	⊢ ( 𝑘 = 𝑗 → ( 2 · 𝑘 ) = ( 2 · 𝑗 ) )
113	112	oveq1d	⊢ ( 𝑘 = 𝑗 → ( ( 2 · 𝑘 ) + 1 ) = ( ( 2 · 𝑗 ) + 1 ) )
114	113	oveq2d	⊢ ( 𝑘 = 𝑗 → ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) = ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) )
115	112	oveq2d	⊢ ( 𝑘 = 𝑗 → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) = ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) )
116	114 115	oveq12d	⊢ ( 𝑘 = 𝑗 → ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) = ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) ) )
117	116	adantl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 = 𝑗 ) → ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) = ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) ) )
118		simpr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
119		2cnd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 2 ∈ ℂ )
120		nncn	⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℂ )
121	120	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℂ )
122	119 121	mulcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 2 · 𝑗 ) ∈ ℂ )
123		1cnd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 1 ∈ ℂ )
124	122 123	addcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 2 · 𝑗 ) + 1 ) ∈ ℂ )
125		0red	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 0 ∈ ℝ )
126		1red	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 1 ∈ ℝ )
127	30	a1i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 2 ∈ ℝ )
128		nnre	⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℝ )
129	128	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℝ )
130	127 129	remulcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 2 · 𝑗 ) ∈ ℝ )
131	130 126	readdcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 2 · 𝑗 ) + 1 ) ∈ ℝ )
132	35	a1i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 0 < 1 )
133	37	a1i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 2 ∈ ℝ+ )
134		nnrp	⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℝ+ )
135	134	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℝ+ )
136	133 135	rpmulcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 2 · 𝑗 ) ∈ ℝ+ )
137	126 136	ltaddrp2d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 1 < ( ( 2 · 𝑗 ) + 1 ) )
138	125 126 131 132 137	lttrd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 0 < ( ( 2 · 𝑗 ) + 1 ) )
139	138	gt0ne0d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 2 · 𝑗 ) + 1 ) ≠ 0 )
140	124 139	reccld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) ∈ ℂ )
141	26	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 𝑁 ∈ ℂ )
142	119 141	mulcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 2 · 𝑁 ) ∈ ℂ )
143	142 123	addcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ )
144	43	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 2 · 𝑁 ) + 1 ) ≠ 0 )
145	143 144	reccld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℂ )
146	45	a1i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 2 ∈ ℕ0 )
147		nnnn0	⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℕ0 )
148	147	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ0 )
149	146 148	nn0mulcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 2 · 𝑗 ) ∈ ℕ0 )
150	145 149	expcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) ∈ ℂ )
151	140 150	mulcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) ) ∈ ℂ )
152	111 117 118 151	fvmptd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 𝐾 ‘ 𝑗 ) = ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) ) )
153		0red	⊢ ( 𝑗 ∈ ℕ → 0 ∈ ℝ )
154		1red	⊢ ( 𝑗 ∈ ℕ → 1 ∈ ℝ )
155	30	a1i	⊢ ( 𝑗 ∈ ℕ → 2 ∈ ℝ )
156	155 128	remulcld	⊢ ( 𝑗 ∈ ℕ → ( 2 · 𝑗 ) ∈ ℝ )
157	156 154	readdcld	⊢ ( 𝑗 ∈ ℕ → ( ( 2 · 𝑗 ) + 1 ) ∈ ℝ )
158	35	a1i	⊢ ( 𝑗 ∈ ℕ → 0 < 1 )
159	37	a1i	⊢ ( 𝑗 ∈ ℕ → 2 ∈ ℝ+ )
160	159 134	rpmulcld	⊢ ( 𝑗 ∈ ℕ → ( 2 · 𝑗 ) ∈ ℝ+ )
161	154 160	ltaddrp2d	⊢ ( 𝑗 ∈ ℕ → 1 < ( ( 2 · 𝑗 ) + 1 ) )
162	153 154 157 158 161	lttrd	⊢ ( 𝑗 ∈ ℕ → 0 < ( ( 2 · 𝑗 ) + 1 ) )
163	162	gt0ne0d	⊢ ( 𝑗 ∈ ℕ → ( ( 2 · 𝑗 ) + 1 ) ≠ 0 )
164	163	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 2 · 𝑗 ) + 1 ) ≠ 0 )
165	124 164	reccld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) ∈ ℂ )
166	165 150	mulcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) ) ∈ ℂ )
167	152 166	eqeltrd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 𝐾 ‘ 𝑗 ) ∈ ℂ )
168		eqid	⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( ( 1 + ( 2 · 𝑛 ) ) / 2 ) · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − 1 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( ( 1 + ( 2 · 𝑛 ) ) / 2 ) · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − 1 ) )
169	1 2 168 3	stirlinglem9	⊢ ( 𝑁 ∈ ℕ → seq 1 ( + , 𝐾 ) ⇝ ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) )
170	110 13 167 169	clim2ser	⊢ ( 𝑁 ∈ ℕ → seq ( 1 + 1 ) ( + , 𝐾 ) ⇝ ( ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) − ( seq 1 ( + , 𝐾 ) ‘ 1 ) ) )
171		peano2nn	⊢ ( 1 ∈ ℕ → ( 1 + 1 ) ∈ ℕ )
172		uznnssnn	⊢ ( ( 1 + 1 ) ∈ ℕ → ( ℤ≥ ‘ ( 1 + 1 ) ) ⊆ ℕ )
173	12 171 172	mp2b	⊢ ( ℤ≥ ‘ ( 1 + 1 ) ) ⊆ ℕ
174	173	a1i	⊢ ( 𝑁 ∈ ℕ → ( ℤ≥ ‘ ( 1 + 1 ) ) ⊆ ℕ )
175	174	sseld	⊢ ( 𝑁 ∈ ℕ → ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → 𝑗 ∈ ℕ ) )
176	175	imdistani	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) )
177	176 152	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( 𝐾 ‘ 𝑗 ) = ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) ) )
178	30	a1i	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → 2 ∈ ℝ )
179		eluzelre	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → 𝑗 ∈ ℝ )
180	178 179	remulcld	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → ( 2 · 𝑗 ) ∈ ℝ )
181		1red	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → 1 ∈ ℝ )
182	180 181	readdcld	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → ( ( 2 · 𝑗 ) + 1 ) ∈ ℝ )
183	173	sseli	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → 𝑗 ∈ ℕ )
184	183 163	syl	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → ( ( 2 · 𝑗 ) + 1 ) ≠ 0 )
185	182 184	rereccld	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) ∈ ℝ )
186	185	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) ∈ ℝ )
187	34	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ )
188	43	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( ( 2 · 𝑁 ) + 1 ) ≠ 0 )
189	187 188	rereccld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℝ )
190	176 149	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( 2 · 𝑗 ) ∈ ℕ0 )
191	189 190	reexpcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) ∈ ℝ )
192	186 191	remulcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) ) ∈ ℝ )
193	177 192	eqeltrd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( 𝐾 ‘ 𝑗 ) ∈ ℝ )
194		1red	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 1 ∈ ℝ )
195	30	a1i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 2 ∈ ℝ )
196	176 129	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 𝑗 ∈ ℝ )
197	195 196	remulcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( 2 · 𝑗 ) ∈ ℝ )
198	87	a1i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ 2 )
199		0red	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → 0 ∈ ℝ )
200	87	a1i	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → 0 ≤ 2 )
201		1p1e2	⊢ ( 1 + 1 ) = 2
202		eluzle	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → ( 1 + 1 ) ≤ 𝑗 )
203	201 202	eqbrtrrid	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → 2 ≤ 𝑗 )
204	199 178 179 200 203	letrd	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → 0 ≤ 𝑗 )
205	204	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ 𝑗 )
206	195 196 198 205	mulge0d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ ( 2 · 𝑗 ) )
207	197 206	ge0p1rpd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( ( 2 · 𝑗 ) + 1 ) ∈ ℝ+ )
208	89	a1i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ 1 )
209	194 207 208	divge0d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) )
210	32	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 𝑁 ∈ ℝ )
211	195 210	remulcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( 2 · 𝑁 ) ∈ ℝ )
212	94	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ 𝑁 )
213	195 210 198 212	mulge0d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ ( 2 · 𝑁 ) )
214	211 213	ge0p1rpd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ+ )
215	194 214 208	divge0d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) )
216	189 190 215	expge0d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) )
217	186 191 209 216	mulge0d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) ) )
218	217 177	breqtrrd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ ( 𝐾 ‘ 𝑗 ) )
219	108 109 170 193 218	iserge0	⊢ ( 𝑁 ∈ ℕ → 0 ≤ ( ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) − ( seq 1 ( + , 𝐾 ) ‘ 1 ) ) )
220		seq1	⊢ ( 1 ∈ ℤ → ( seq 1 ( + , 𝐾 ) ‘ 1 ) = ( 𝐾 ‘ 1 ) )
221	100 220	mp1i	⊢ ( 𝑁 ∈ ℕ → ( seq 1 ( + , 𝐾 ) ‘ 1 ) = ( 𝐾 ‘ 1 ) )
222	221	oveq2d	⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) − ( seq 1 ( + , 𝐾 ) ‘ 1 ) ) = ( ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) − ( 𝐾 ‘ 1 ) ) )
223	219 222	breqtrd	⊢ ( 𝑁 ∈ ℕ → 0 ≤ ( ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) − ( 𝐾 ‘ 1 ) ) )
224	4 107 61 223	leadd1dd	⊢ ( 𝑁 ∈ ℕ → ( 0 + ( 𝐾 ‘ 1 ) ) ≤ ( ( ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) − ( 𝐾 ‘ 1 ) ) + ( 𝐾 ‘ 1 ) ) )
225	52 51	eqeltrd	⊢ ( 𝑁 ∈ ℕ → ( 𝐾 ‘ 1 ) ∈ ℂ )
226	225	addlidd	⊢ ( 𝑁 ∈ ℕ → ( 0 + ( 𝐾 ‘ 1 ) ) = ( 𝐾 ‘ 1 ) )
227	73	recnd	⊢ ( 𝑁 ∈ ℕ → ( 𝐵 ‘ 𝑁 ) ∈ ℂ )
228	84	recnd	⊢ ( 𝑁 ∈ ℕ → ( 𝐵 ‘ ( 𝑁 + 1 ) ) ∈ ℂ )
229	227 228	subcld	⊢ ( 𝑁 ∈ ℕ → ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) ∈ ℂ )
230	229 225	npcand	⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) − ( 𝐾 ‘ 1 ) ) + ( 𝐾 ‘ 1 ) ) = ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) )
231	224 226 230	3brtr3d	⊢ ( 𝑁 ∈ ℕ → ( 𝐾 ‘ 1 ) ≤ ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) )
232	4 61 85 106 231	ltletrd	⊢ ( 𝑁 ∈ ℕ → 0 < ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) )
233	84 73	posdifd	⊢ ( 𝑁 ∈ ℕ → ( ( 𝐵 ‘ ( 𝑁 + 1 ) ) < ( 𝐵 ‘ 𝑁 ) ↔ 0 < ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) ) )
234	232 233	mpbird	⊢ ( 𝑁 ∈ ℕ → ( 𝐵 ‘ ( 𝑁 + 1 ) ) < ( 𝐵 ‘ 𝑁 ) )